Logical Full Abstraction and PCF
John Longley and Gordon PlotkinAbstract:
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.
ECS-LFCS-97-353.This report is available in the following formats:
- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts
- LaTeX DVI file
- Gzipped LaTeX DVI file