The Geometry of Sequential Computation I: A Simplicial Geometry of Interaction

We formulate a geometrical representation of the normalization of proofs in the multiplicative-exponential fragment of linear logic. In particular, our representation conserves the local nature of the normalization process --- a concern salient to the Geometry of Interaction paradigm of Girard et al. Our approach is based on the representation of linear proofs as certain kinds of higher-dimensional automata, modeled as Simplicial sets in an affine geometry. This representation draws significantly upon the ideas of Eric Goubault, Vaughan Pratt and others, using geometric simplices for modeling higher-dimensional automata. The novelty in our approach is using this essentially concurrent structure to anchor a second-level sequential representation --- that of the global history of the (development) of the proof-objects, encoded as a certain kind of homological data correlated with the simplicial structure. In the process-theoretic metaphor, these could be viewed as set of sequential traces of these automata, along with a minimal synchronization structure. The main motivation behind our approach is to develop extensional fully-abstract models of higher-type functional sequential computation, by using the (local) geometrical structure of Simplicial sets to enrich the (global) topological space of denotations. Additionally, it opens up a new way of looking at linear proofs as geometrically structured processes, along with the possibility of importing notions like equivalence and causal dependence from traditional process theory into the study of proofs.     «

We formulate a geometrical representation of the normalization of proofs in the multiplicative-exponential fragment of linear logic. In particular, our representation conserves the local nature of the normalization process --- a concern salient to the Geometry of Interaction paradigm of Girard et al. Our approach is based on the representation of linear proofs as certain kinds of higher-dimensional automata, modeled as Simplicial sets in an affine geometry. This representation draws significantl...     »