Proof-nets and the Hilbert space
Vincent Danos, Laurent Régnier · Cambridge University Press eBooks · 1995
Girard's execution formula (given in [Gir88a]) is a decomposition of usual β-reduction (or cut-elimination) in reversible, local and asynchronous elementary moves. It can easily be presented, when applied to a λ-term or a net, as the sum of maximal paths on the λ-term/net that are not cancelled by the algebra L* (as was done in [Dan90, Reg92]). It is then natural to ask for a characterization of those paths, that would be only of geometric nature. We prove here that they are exactly those paths that have residuals in any reduct of the λ-term/net. Remarkably, the proof puts to use for the first time the interpretation of λ-terms/nets as operators on the Hilbert space. Presentation λ-Calculus is simple but not completely convincing as a real machine-language. Real machine instructions have a fixed run-time; a β-reduction step does not. Some implementations do map-reductions into sequences of real elementary steps (as in environment machines for example) but they use a global time to achieve this. The “geometry of interaction” (GOI) is an attempt to find a low-level combinatorial code within which β-reduction could be implemented and such that: elementary reduction steps are local; parallelism shows up and global time disappears; some mathematics dealing with syntax is uncovered. — Goal and organization of this paper. A persistent path is a path on a λ-term which survives the action of any reduction (defined in [Reg92]). A regular path is a path which is not cancelled by Girard's algebraic device L* (defined in [Gir88a]).