Coherent models of proof nets (Q1325054): Difference between revisions

The first goal of the paper is to construct a model of the set PN of pure proof nets of \textit{V. Danos} and \textit{L. Regnier} [\(\Lambda\) et \(\Lambda^*\): une alternative à la réduction des \(\lambda\)-termes. Preprint, Univ. Paris 7 (1989); see also \textit{V. Damos}, La logique linéaire appliquée à l'étude de divers processus de normalisation (principalement du \(\lambda\)-calcul). Thèse de doctorat, Univ. Paris 7 (1990)]. The set PN is to the linear logic of \textit{J.-Y. Girard} [Theor. Comput. Sci. 50, 1-102 (1987; Zbl 0625.03037)] what untyped \(\lambda\)- calculus (or \(\lambda\)-calculus, for short), is to typed \(\lambda\)- calculus, or to intuitionistic logic via the isomorphism of Curry-Howard; moreover, the set PN contains a translation of the elements of \(\lambda\)- calculus. A coherent space, named \(C\), is the domain of the interpretation of the pure proof nets (Theorem 2.7); Theorem 2.9 establishes that \(C\) is model of PN. A first property is the equality of the interpretation in \(C\) of the \(\lambda\)-terms and their translated proof nets (Theorem 3.3). The second goal, Part 3.2, which is a consequence of the modelization, is the introduction of another syntax of PN, called intermediate syntax. The set of proof nets with this syntax (Definition 3.6, Theorem 3.10) is defined starting from a quotient of PN by an equivalence relation. The equivalence relation defined in Definition 3.4 satisfies that two equivalent proof nets have the same interpretation (Lemma 3.5). The intermediate syntax is a step in the definition of the pure proof nets as graphs like the multiplicative proof nets are (proof nets of the multiplicative linear logic, whose set is named \(\text{PN}_ 0)\). Indeed, we have the notion of name (of exponential box) or index in the syntax and the original correctness criterion (which is inductive on the indices (of boxes), the correctness graphs are acyclic and connected). To forget the notion of an index and the induction in the syntax of pure proof nets, we get the so-called new syntax [the authors, Proof nets of PN as graphs, Arch. Math. Logic (submitted)], which will not be the object of the present paper . The objects defined in the new syntax are graphs, and the question is then which ones are pure proof nets. A partial answer happens to be in the above paper: it concerns graphs without exponential cut link; the so defined set is closed by (multiplicative) cut elimination and in the general case is still open. The intermediate syntax is also a step in the direction of the work of \textit{G. Gonthier}, \textit{M. Abadi} and \textit{J. J. Lévy} [``The geometry of optimal lambda reduction'', Proc. 19th ACM Symp. Principles of Programming Languages, 15-26 (1992)], since an index corresponds to a crossing box link.