Hostname: page-component-745bb68f8f-f46jp Total loading time: 0 Render date: 2025-02-06T04:05:25.954Z Has data issue: false hasContentIssue false

Full abstraction, totality and PCF

Published online by Cambridge University Press:  01 February 1999

GORDON PLOTKIN
Affiliation:
Department of Computer Science, University of Edinburgh, King's Buildings, Edinburgh EH9 3JZ, UK. E-mail: gdp@dcs.ed.ac.uk.
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Inspired by a question of Riecke, we consider the interaction of totality and full abstraction, asking whether full abstraction holds for Scott's model of cpos and continuous functions if one restricts to total programs and total observations. The answer is negative, as there are distinct operational and denotational notions of totality. However, when two terms are each total in both senses, they are totally equivalent operationally iff they are totally equivalent in the Scott model. Analysing further, we consider sequential and parallel versions of PCF and several models: Scott's model of continuous functions, Milner's fully abstract model of PCF and their effective submodels. We investigate how totality differs between these models. Some apparently rather difficult open problems arise that essentially concern whether the sequential and parallel versions of PCF have the same expressive power, in the sense of total equivalence.

Type
Research Article
Copyright
1999 Cambridge University Press