zbMATH — the first resource for mathematics

Proof-nets and the Hilbert space. (English) Zbl 0854.03011
Girard, Jean-Yves (ed.) et al., Advances in linear logic. Based on the linear logic workshop held June 14-18, 1993 at the Mathematical Sciences Institute, Cornell University, Ithaca, New York, USA. Cambridge: Cambridge University Press. Lond. Math. Soc. Lect. Note Ser. 222, 307-328 (1995).
Proof-nets play in Girard’s Linear Logic the rôle proof-trees play in intuitionistic logic. The properties of paths through these nets have been studied in detail and they are known to provide information about logical correctness as well as about termination of reduction.
The authors of the present paper have been at the heart of these achievements from the beginning. Their present work gives a new proof of an equivalence between two notions: persistent paths and regular paths. Persistent paths are paths which do not disappear along any reduction of the net. Regular paths are paths of weight 0, when a weight in Girard’s algebra \(L^*\) has been associated to each path.
The authors recall these different notions in a short but clear way; then the equivalence is proven, with a new method which is the first use of the linear structure of the Hilbert space in Geometry of Interaction.
For the entire collection see [Zbl 0816.00018].

03B40 Combinatory logic and lambda calculus
03F07 Structure of proofs
03F05 Cut-elimination and normal-form theorems