The Geometry of Sequential Computation II: Full abstraction for PCF

In this study, our earlier work on the representation of linear (MELL) proofs using affine simplices is used to develop an approach to a certain version of the problem of full abstraction for a denotational semantics for PCF. We stay as far as possible, within the classical ideas of Scott, Berry and others, by conceiving our denotational space essentially as a certain kind of topological space (specifically, a consistently complete, algebraic cpo); the generalization we use, is to look at this space not just as a set of points as in traditional topology, but as a variable set, with its domain of variation structured by the geometry of simplicial sets. The geometry used to enrich our points is then used to control the size of the function spaces by cutting them down to consist of only those kinds of continuous maps, which satisfy a criterion akin to the Kahn-Plotkin notion of sequential functions, but framed purely in terms of our underlying geometry. Thus we show that global topological continuity based upon local geometric structure is a good way to represent sequential computation.     «

In this study, our earlier work on the representation of linear (MELL) proofs using affine simplices is used to develop an approach to a certain version of the problem of full abstraction for a denotational semantics for PCF. We stay as far as possible, within the classical ideas of Scott, Berry and others, by conceiving our denotational space essentially as a certain kind of topological space (specifically, a consistently complete, algebraic cpo); the generalization we use, is to look at this...     »