Logical Full Abstraction and PCF

John Longley and Gordon Plotkin


We introduce the concept of logical full abstraction, generalising the usual equational notion. We consider the language PCF and two extensions with ``parallel'' operations. The main result is that, for standard interpretations, logical full abstraction is equivalent to equational full abstraction together with universality; the proof involves constructing enumeration operators. We also consider restrictions on logical complexity and on the level of types.


This report is available in the following formats:

Previous | Index | Next