We present a new realisability model based on othogonality for Linear Logic in the context of nets untyped proof structures with generalized axiom. We show that it adequately models second order multiplicative linear logic. As usual, not all realizers are representations of a proof, but we identify specific types (sets of nets closed under bi-othogonality) that capture exactly the proofs of a given sequent. Furthermore these types are orthogonal's of finite sets; this ensures the existence of a correctnesss criterion that runs in ifnite time. In particular, in the well known case of multiplicative linear logic, the types capturing the proofs are generated by the tests of Danos-Regnier, we provide - to our knowledge - the first proof of the folklore result which states "test of a formula are proofs of its negation".
For instance, whenever the computational model is a freely–generated language equipped with a binary relation capturing program execution, correct programs correspond to well–formed terms.
A theorem of adequacy or soundness usually follows, e.g. each proof of corresponds to a realizer of . However, not all realizers are correct programs thus not all realizers represent a proof. In fact, it was revealed by realisability models based on orthogonality that the presence of incorrect programs is crucial to give a computational status to correctness.
When introduced by Kleene, realisability was only considered for intuistionnistic logics due to their ‘constructive’ nature, and it is only in 2005 that Jean-Louis Krivine introduced classical realisability [3] aiming at extending realisability techniques to classical logic, proposing a model based on orthogonality. Krivine’s construction is based on an extension of the untyped lambda calculus, but, in order to capture a given context (stack) to potentially restore it later, the syntax is not only extended with the call/cc operator but also with a countably infinite set of stack constants. As a consequence, (as in Kleene’s realisability) only some of the programs represent a classical proof, namely those not containing stack constants. This introduction of "incorrect" terms is essential, as it introduces in the syntax semantic information [4] that can be used to test correct (and incorrect) terms. This concept of testing is captured by the definition of an orthogonality relation (here between terms and stacks), which is used to define the interpretation of types (as the set of terms passing a given set of tests).
In parallel with the work of Krivine, similar realisability constructions have been introduced by Jean-Yves Girard in order to interpret Linear Logic. While the orthogonality construction was clearly put forth in Ludics, the ideas and first occurrences can be traced back to the first model of geometry of interaction (GoI) [5], which is restricted to multiplicative linear logic, and interprets proofs as permutations. Later GoI construction took several diverse forms, generalising permutations by operators in a C*-algebra (goi1 [6], goi2 [7]), first-order prefix rewriting (goi3) [8], or von Neumann Algebras (goi5) [9].
In a series of recent papers [10, 11, 12], Thomas Seiller proposed a combinatorial approach to the Geometry of Interaction, interaction graphs, which specialises to all the previous ‘geometries’ of interaction proposed by Girard. It is crucial to note that this work on goi constructs the types of Linear Logic via a realisabilty method, involving orthogonality within the computational model of interaction graphs. However, proofs are interpreted in these models as abstract objects (generalisations of dynamical systems) which remain far from the general intuition of what a proof is.
This is where our work starts: we extend the use of realizability techniques to Linear Logic in an untyped variant of the well known and ‘canonical’ context of proof nets; first to the multiplicative fragment of Linear Logic, and secondly to second order multiplicative Linear Logic. We obtain the results of soundness (e.g. adequacy) and completeness both for MLL and MLL✠ – with furthermore assumptions on the interpretation basis. Soundness is also true at the second–order for MLL2 proofs. Moreover we show that the types constructed by induction for both the multiplicative and second–order preserve the finite testability 2. In particular this is true for the types capturing the proofs of the multiplicative fragment: this is done by encoding the Danos Regnier criterion [13] in MLL✠ proofs, we provide, to our knowledge, the first proper 2A type A is finitely testable if there exists a finite set such that A = ⊥. proof of the folklore result which states that ’tests of are proofs of its negation’. We are still investigating how to capture the proofs of the second order multiplicative fragment while remaining finitely testable. We believe this will lead to a novel correctness criterion for second order multiplicative proof structures.
As a computational model we chose the model of nets, a modern formulation – as hypergraphs – of the model of proof structures introduced by Jean Yves Girard in his seminal paper [14]. Informally speaking the nets are hypergraphs constructed by composing the hyperedges, called links, of the figure 1 such that a vertex is the target (resp. source) of at most one link. The conclusion of a net is a vertex that is the source of no link and our hypergraphs are equipped with an order on their conclusion. Nets that have conclusions can interact by placing cut links in between their conclusions. Given two nets and their interaction is denoted :: .
Furhtermore, the nets come with a notion of computation which corresponds to cut elimination illustrated in figure 2. Contrary to the original multiplicative proof structures introduced in 1987 by Jean Yves Girard, this rewriting is non–deterministic and not confluent.
The computation gives rise to the notion of orthogonality; two nets and are orthogonal whenever their interaction :: has at least one way to reduce to the net ✠ the daimon link with no output – we then denote ⊥ .
Definition 1 (Types). The orthogonal ⊥ of a set of multiplicative nets is defined by { | ∀ ∈ , ⊥ }. A type A is a set of multiplicative nets such that A⊥⊥ = A, or equivalently such that A = ⊥ for some set .
Given a net with its conclusion ordered as 1 < · · · < for an integer 1 ≤ ≤ we denote () the conclusion of . Furthermore, we let Pos() denote its set of vertices. Given two nets and their sum + corresponds to the union of their graphs in which the set of links is assumed to be disjoint.
Definition 2 (Construction on types). Given A and B two types we define several constructions: • Their parallel sum A ‖ B = { + | ∈ A, ∈ B, Pos() ∩ Pos() = ∅}⊥⊥. • Their functional composition A · B = { | for any ∈ A⊥, :: ∈ B}⊥⊥ . • The tensor product of two types, A⊗ B = {++⟨(1), (1) ▷⊗ ⟩ | Pos()∩Pos() = ∅, ∈ A, ∈ B}⊥⊥.
• The `–product of two types, A ` B = (A⊥ ⊗ B⊥)⊥.
Definition 3 (Interpretation Basis). An interpretation basis ℬ is a function that associates to each atomic proposition a type JKℬ, the interpretation of , such that • Each net in JKℬ has one conclusion.
• For any atomic proposition we have J⊥Kℬ = JKℬ⊥.
Definition 4 (Realizer of a formula). Given an interpretation basis ℬ, the interpretation of a formula is lifted from atomic formulas to any formula and sequents of MLL by induction; ✠ 1 2 . . .
cut cut cut
✠ 3 ` 6 4 ✠ cut 5 11
21 cut cut → 0 ✠ 21 +1 . . . 4
5 ` 6 1 2 3
4 ` 5 cut ✠ ⊗ 6 ✠ cut 4 ⊗ 6 5
cut 1 . . . → 4 11
1 . . . 5 cut ✠ 1 . . . → 4 ✠ 2 . . . If there is no ambiguity we relax the notation JΓKℬ to JΓK. We denote ⊩ ℬ 1, . . . , whenever ∈ JΓKℬ.
Interpretation basis may come with several properties to ensure adequacy or completeness for the logical system considered, namely MLL, MLL✠ or MLL2. A basis is: • self dual whenever it maps atomic variables to self dual types A ⊆ • approximable whenever it maps atomic variables to types containing the net made of one daimon link with one conclusion.
Theorem 5 (Adequacy). Let be a multiplicative net and Γ be a sequent, • For any basis ℬ; ⊢MLL Γ ⇒ ⊩ ℬ Γ.
• For any approximable basis ℬ; ⊢MLL✠ Γ ⇒ ⊩ ℬ Γ.
MLL✠.
Theorem 6 (MLL✠ completeness). Given some sequent Γ and a cut–free net and ℬ a self dual and approximable interpretation basis, if belongs to JΓKℬ then represents a proof of Γ from Definition 7 (Intersection and union type). Let ℬ be an interpretation basis, and Ω be a set of types with one output. Given a Γ a sequent of MLL formulas and a propositional variable the intersection type and union type on Ω of Γ in w.r.t. to ℬ are defined as follow; ∈Ω
∈Ω J ⋂︁ ΓKℬ ≜ ⋂︁ JΓKℬ{↦→}
J ∈Ω ⋃︁ ΓKℬ ≜ ︃( ∈Ω ⋃︁ JΓKℬ{↦→} )︃⊥⊥ . in MLL. interpretation basis. If symmetrically realizes ⋂︀ Theorem 8 (MLL completeness). Given a proof like and cut–free net and ℬ some approximable ∈ J⋂︀∈Ω ΓKℬ then is the image of a proof Definition 9 (realizers of MLL2). Let ℬ be an approximable interpretation basis and Ω denote the set of types with one output. Given a formula of MLL2 its set of realizers is given by the following induction:
J J ⊗ K ≜ JK ⊗ JK ` K ≜ JK ` JK
J∀ K ≜ { + ⟨(1) ▷∀ ⟩ | ∈ J J∃ K ≜ { + ⟨(1) ▷∃ ⟩ | ∈ J⋃︀∈Ω K}⊥⊥ ⋂︀∈Ω K} Theorem 10 (Soundness for MLL2). Let ℬ be an approximable interpretation basis. Given a proof–like multiplicative second order net. If represents a proof of the sequent Γ then belongs to JΓKℬ
. [1] A. Miquel, De la formalisation des preuves à l’extraction de programmes, Habilitation at
Université Paris Diderot (2009). URL: https://www.fing.edu.uy/~amiquel/publis/hdr.pdf. [2] S. C. Kleene, On the interpretation of intuitionistic number theory, The Journal of Symbolic
URL: https://hal.science/hal-00154500. [3] J.-L. Krivine, Realizability in classical logic, Panoramas et synthèses 27 (2009) 197–229. [4] A. Naibo, M. Petrolo, T. Seiller, On the Computational Meaning of Axioms, Springer International Publishing, Cham, 2016, pp. 141–184. URL: https://doi.org/10.1007/ 978-3-319-26506-3_5. doi:10.1007/978-3-319-26506-3_5. [5] J. Girard, Multiplicatives, in: G. Lolli (Ed.), Logic and Computer Science: New Trends and
Applications, Rosenberg & Sellier, 1987, pp. 11–34. [6] J.-Y. Girard, Geometry of interaction 1: Interpretation of system f, in: R. Ferro, C. Bonotto, S. Valentini, A. Zanardo (Eds.), Logic Colloquium ’88, volume 127 of Studies in Logic and the Foundations of Mathematics, Elsevier, 1989, pp. 221–260. URL: https:// www.sciencedirect.com/science/article/pii/S0049237X08702714. doi:https://doi.org/ 10.1016/S0049-237X(08)70271-4. [7] J. Girard, Geometry of interaction 2: deadlock-free algorithms, in: P. Martin-Löf, G. Mints (Eds.), COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings, volume 417 of Lecture Notes in Computer Science, Springer, 1988, pp. 76– 93. URL: https://doi.org/10.1007/3-540-52335-9_49. doi:10.1007/3-540-52335-9\_49. [8] J.-Y. Girard, Geometry of interaction III: accommodating the additives, London Mathematical Society Lecture Note Series, Cambridge University Press, 1995, p. 329–389. doi:10.1017/CBO9780511629150.017. [9] J. Girard, Geometry of interaction V: logic in the hyperfinite factor, Theor. Comput. Sci. 412 (2011) 1860–1883. URL: https://doi.org/10.1016/j.tcs.2010.12.016. doi:10.1016/j.tcs. 2010.12.016. [10] T. Seiller, Interaction graphs: Graphings, Annals of Pure and Applied Logic 168 (2017) 278–320. doi:10.1016/j.apal.2016.10.007. [11] T. Seiller, Interaction graphs: Exponentials, Log. Methods Comput. Sci. 15 (2013). [12] T. Seiller, Interaction graphs: Full linear logic, CoRR abs/1504.04152 (2015). URL: http: //arxiv.org/abs/1504.04152. arXiv:1504.04152. [13] V. Danos, L. Regnier, The structure of multiplicatives, Archive for Mathematical Logic 28 (1989) 181–203. URL: https://doi.org/10.1007/BF01622878. doi:10.1007/BF01622878. [14] J.-Y. Girard, Linear logic, Theoretical Computer Science 50 (1987) 1 – 101. URL: http: //www.sciencedirect.com/science/article/pii/0304397587900454. doi:https://doi.org/ 10.1016/0304-3975(87)90045-4.