A congruence relation for restructuring classical terms Dragiša Žunić1 and Pierre Lescanne2 1 Carnegie Mellon University in Qatar 2 Laboratoire de l’Informatique du Parallélisme, LIP Ecole Normale Supérieure de Lyon, France Abstract. We present a congruence relation on sequent-style classical proofs which identifies proofs up to trivial rule permutation. The study is performed in the framework of ∗X calculus which provides a Curry- Howard correspondence for classical logic (with explicit structural rules) ensuring that proofs can be seen as terms and proof transformation as computation. Congruence equations provide an explicit account for clas- sifying proofs (terms) which are syntactically different but essentially the same. We are able to prove that there is always a representative of a congruence class which enables computation at the top level. 1 Introduction For a long time it was considered not possible to give constructive semantics to classical logic, but only to intuitionistic and linear logic. Recent works have shown that this is actually possible if one gives up on the principle that the computational semantics is a confluent rewrite system. In this work we study the essence of classical proofs by means of specifying its unessential content. Namely we present a list of congruence rules specifying which syntactically different proofs/terms should be considered the same. Moreover, this congruence relation enables us to pick a representative of a congruence class so that the cut elimination can continue at the top level. This is done in the framework of ∗X calculus - a higher order rewrite system designed to provide a Curry-Howard correspondence with the sequent system G1 [13] for classical logic (presented in Fig. 2). This system is characterized by the presence of structural rules weakening and contraction and it is very close to the original formulation by Gentzen [5]. 2 Related work The first computational interpretation of classical logic relying on sequents was presented by Curien and Herbelin in [4] and in [8], while a direct correspondence with a standard sequent formulation of classical logic, with the intent of captur- ing its computational content in full richness (although with implicit structural rules), was presented by Urban in [14] and by Bierman and Urban in [15]. This research further lead to the formulation of X calculus [11, 2] which was a base to introduce explicit control over erasure and duplication by featuring explicit structural rules weakening and contraction, yielding the ∗X calculus [18, 6]. This kind of conservative calculus extension had been studied in the intuitionistic framework by Kesner and Lengrand [9]. Indeed there is a certain analogy in going from λx [1] (featuring explicit substitution) towards λlxr [9] (explicit sub- stitution, erasure and duplication) in the natural deduction setting, and going from X to ∗X in the classical sequent calculus setting. 3 The calculus ∗X Intuitively when we speak about ∗X -terms we speak about classical proofs for- malized in the sequent calculus with explicit structural rules weakening and contraction. Terms are built from names. This concept differs essentially from the one applied in λ-calculus, where variable is the basic notion. The difference lies in the fact that a variable can be substituted by an arbitrary term, while a name can be only renamed (that is, substituted by another name). In our calculus the renaming is explicit, which means that it is expressed within the language itself and is not defined in the meta-theory. The notation of using hats over names has been borrowed from Principia Mathematica [17] and is used to denote the binding of a name. Definition 1. The syntax of ∗X -calculus3 is presented in Fig. 1, where x, y, z... range over an infinite set of in-names and α, β, γ... range over an infinite set of out-names. P, Q ::= hx.αi capsule (axiom rule) b P βb . α | x exporter (ritht arrow-introduction) | Pα b [x] yb Q importer (left arrow-introduction) | Pα b †x bQ cut (cut) | x P left-eraser (left weakening) | P α right-eraser (right weakening) | z < xybbhP ] left-duplicator (left contraction) α | [P iβb >γ right-duplicator (right contraction) b Fig. 1. The syntax of ∗X Although we distinguish two categories of names (in-names and out-names) they will usually be referred to simply as names. There are eight constructors introduced in the syntax, whose names suggest their computational role. 3 We consider only the implicational fragment here. Definition 2. We define free names and principal names of a term R, written f n(R) and pn(R), respectively, in the following way: R f n(R) pn(R) hx.αi x, α x, α xb P βb . α f n(P )\{x, β} ∪ α α Pα b [x] yb Q f n(P ) ∪ f n(Q)\{α, y} ∪ x x Pα b †x bQ f n(P ) ∪ f n(Q)\{α, x} none x P f n(P ) ∪ x x P α f n(P ) ∪ α α x< xxc c 1 2 hP ] f n(P )\{x1 , x2 } ∪ x x α [P iαc2 >α c1 f n(P )\{α1 , α2 } ∪ α α A name which is not free is called a bound name. The notion of a principal name describes a free name that appears at the top level in the structure of term. We will use P α and Qx to emphasize that P and Q have α and x as principal names, respectively. Our consideration of principal names is motivated by the nature of cut oper- ation, which always refers to a pair of free names (an out-name and an in-name) - one in each corresponding term - and binds them. If these names are at the top level (accessible) then the cut elimination proceeds in one of its essential steps. However this research is concerned by static aspects only (dealing with proof structure), but it most certainly attempts to lay the foundation for revealing the computational essence as well. In the ∗X calculus we consider only linear terms. We say that a term is linear if every name has at most one free occurrence and every binder does bind an actual occurrence of a name (and therefore only one). We use the standard definition of linear terms, see [18] on page 43. We will specify the notions of context, subterm and immediate subterm in order to efficiently work with the structure of terms. Definition 3. The contexts are formally defined as follows: C{ } ::= {} | b { } βb . α x | { }α b [x] yb Q | Pα b [x] yb { } | { }b α†x bQ | Pαb †x b{ } | x {} | {} α α | z < xybbh{ }] | [{ }iβb >γ b | C{C{ }} Informally, a context is a term with a hole which can accept another term. Therefore C{P } denotes placing the term P in the context C{ }. Definition 4. A term Q is a subterm of a term P , denoted as Q 4 P if there is a context C{ } such that P = C{Q} (the symbol = stands for syntactic equality.). It is easy to show that the subterm relation is reflexive, antisymmetric and transitive (i.e., is an order). Definition 5. A term Q is an immediate subterm of P if P = C{Q} and 6 C 0 {C 00 { }}, C{ } = C{ } = 6 { }. 4 The type assignment system Given a set T of basic types, a type is given by A, B ::= A ∈ T | A → B. Expressions of the form P : · Γ ` ∆ are used to present the type assignment, where P is an ∗X term and Γ, ∆ are contexts whose domains consist of free in- names and out-names of P , respectively4 . Comma in the expression Γ, Γ 0 stands for the set union. Definition 6. We say that a term P is typable if there exist contexts Γ and ∆ such that P : · Γ ` ∆ is derivable in the system of rules given by Fig. 3. Γ ` A, ∆ Γ 0 , B ` ∆0 Γ, A ` B, ∆ (L→) (R→) 0 0 Γ, Γ , A → B ` ∆, ∆ Γ ` A → B, ∆ Γ ` A, ∆ Γ 0 , A ` ∆0 (ax) (cut) A`A Γ, Γ 0 ` ∆, ∆0 Γ `∆ Γ `∆ (weak-L) (weak-R) Γ, A ` ∆ Γ ` A, ∆ Γ, A, A ` ∆ Γ ` A, A, ∆ (cont-L) (cont-R) Γ, A ` ∆ Γ ` A, ∆ Fig. 2. Sequent system G1 for classical logic Reduction rules are numerous as they capture the richness and complexity of classical cut elimination, and very fine-grained due to the presence of explicit terms for erasure and duplication. For details see [18]. 5 The congruence relation This section presents a congruence relation on terms, denoted ≡, which is rep- resented by a list of equations5 . The congruence relation induced by these rules 4 Technically contexts are sets of pairs (name, formula); if we forget about labels and consider only type, we are going back to Gentzen’s classical system G1 (Fig. 2), where contexts are multisets of formulas. 5 The list is partial due to limited space. A complete list of congruence rules can be found in [18]. (ax) hx.αi : · x :A ` α :A P : · Γ ` α :A, ∆ Q : · Γ 0 , y :B ` ∆0 P : · Γ, x :A ` α :B, ∆ (L→) (R→) 0 0 b [x] yb Q : · Γ, Γ , x :A → B ` ∆, ∆ Pα x b . β : · Γ ` β :A → B, ∆ bP α P : · Γ ` α :A, ∆ Q : · Γ 0 , x :A ` ∆0 (cut) bQ : · Γ, Γ 0 ` ∆, ∆0 b †x Pα P :· Γ ` ∆ P :· Γ ` ∆ (weak-L) (weak-R) x P : · Γ, x :A ` ∆ P α : · Γ ` α :A, ∆ P : · Γ, x :A, y :A ` ∆ P : · Γ ` α :A, β : A, ∆ (cont-L) α (cont-R) z < xybbhP ] : · Γ, z :A ` ∆ [P iβb >γ : · Γ ` γ :A, ∆ b Fig. 3. The type system for ∗X is a reflexive, symmetric and transitive relation closed under any context. These rules define explicitly and in an intuitive way which syntactically different terms should be considered the same. The key property of this congruence relation is that, given a cut term, it offers a representative of a congruence class so that the computation (cut elimination) continues at the top level (see Theorem 1). The diagrammatic representation is assigned to every congruence rule to strengthen the reader’s intuition (a formal study of the diagrammatic calculus, which can be derived from the term calculus presented here, is in the domain of future work). A label is assigned to every congruence rule, and thus each rule is declared as: name : P ≡ Q. exporter-importer (1) γ y (2) γ y x P β I Q P I x Q β E E α z z α ei1 : xb (P γb [z] yb Q) βb . α ≡ (b x P βb . α) γ b [z] yb Q with x, β ∈ f n(P ) . ei2 : xb (P γb [z] yb Q) β α ≡ P γb [z] yb (b b x Q βb . α) with x, β ∈ f n(Q) exporter-cut (1) γ y (2) γ y x P β Q P x Q β E E α α ec1 : xb (P γb † ybQ) βb . α ≡ (b x P βb . α)b γ † ybQ with x, β ∈ f n(P ) . ec2 : xb (P γb † ybQ) β α ≡ P γb † yb(b b x Q βb . α) with x, β ∈ f n(Q) importer-importer (1) (2) (3) t α R α y Q β t P β I P I I R I y P α y Q Q β t R I I x z x x z z ii1 : (P α t R ≡ (P βb [z] b b [x] yb Q) βb [z] b t R) αb [x] yb Q with α, β ∈ f n(P ) ii2 : (P αb [x] yb Q) β [z] b b tR ≡ P α b [x] yb (Q βb [z] b t R) with y, β ∈ f n(Q) ii3 : (Q βb [z] b t R) ≡ Q βb [z] b t (P α b [x] yb R) with y, t ∈ f n(R) cut-cut (1) (2) (3) y α β R P α x Q β y R P x P α x Q Q β y R cc1 : (P α b †xbQ)βb † ybR ≡ (P βb † ybR)b α †x bQ with α, β ∈ f n(P ) cc2 : (P α b †xbQ)βb † ybR ≡ P α b †x b(Qβb † ybR) with x, β ∈ f n(Q) cc3 : P α b †xb(Qβb † ybR) ≡ Qβb † yb(P α b †xbR) with x, y ∈ f n(R) cut-importer (1) (2) β z R P α I y Q β z R α y P I Q x x ci1 : b [x] yb Q)βb † zbR ≡ (P βb † zbR) α (P α b [x] yb Q with α, β ∈ f n(P ) ci2 : b [x] yb Q)βb † zbR ≡ P α (P α b [x] yb (Qβb † zbR) with y, β ∈ f n(Q) (3) (4) α x β z α P Q I R P x β z Q I R y y ci3 : P α b †x b(Q βb [y] zb R) ≡ (P α b †x bQ) βb [y] zb R with x, β ∈ f n(Q) ci4 : P α b(Q βb [y] zb R) ≡ Q βb [y] zb (P α b †x b †x bR) with x, z ∈ f n(R) cut-contraction (1) (2) x1 x1 x x x2 x2 P α y Q P α y Q cct 1 : x< xxc c2 b † ybQ] ≡ (x< xxc 1 hP α c 1 hP ])b 2 α † ybQ with x1 , x2 ∈ f n(P ) x cct 2 : x< xc2 hP α c1 b † yb(x< xxc b † ybQ] ≡ P α c 1 2 hQ]) with x1 , x2 ∈ f n(Q), y 6= x (3) (4) α1 α1 α α α2 P β y Q P β y Q α2 cct 3 : [P βb † ybQiααc1 c2 α >α ≡ ([P i 1 >α)β c α c2 b † ybQ with α1 , α2 ∈ f n(P ), α 6= β cct 4 : [P βb † ybQiαc12 >α ≡ P βb † yb([Qiααc αc c2 >α) 1 with α1 , α2 ∈ f n(Q) weak-general (1) (2) x C P C P α wg1 : x (C{P }) ≡ C{x P } x∈ / f n(C{P }) wg2 : (C{P }) α ≡ C{P α} α∈ / f n(C{P }) The relation ≡ induces congruence classes on terms. We use cl(P ) to denote the congruence class of a term P with respect to the relation ≡. Notice that each congruence class has finitely many terms, and thus finitely many possibilities to select a representative of a class. Congruence rules satisfy some standard properties such as preservation of free names (interface preservation, as in Lafont’s interaction nets [10]) and preserva- tion of types. It has been argued in [12] that two sequent proofs induce the same proof net if and only if one can be obtained from the other by a sequence of transpositions of independent rules, without giving details about these operations. We proceed further as we have presented explicitly how this transposition is done at the static level. This detailed study, presented here in the framework of ∗X calculus, will enable the search for the essence of computational aspect as well, by considering reduction as reducing modulo congruence relation. In what follows we show that the congruence rules allow us to perform restruc- turing of ∗X -terms (i.e. sequent proofs), so that the cut-names (names bound by a cut operation) are brought to the top level. Take for example an arbitrary ∗ X -term of the form: Pαb †x bQ The name α might not be directly accessible (that is, α is maybe not principal name for P ). Furthermore, this might hold for both names involved in the cut, α and x, which are possibly deep inside the structure of their corresponding terms. We prove that it is possible to transform the above term using congruence rules defined in the previous section6 - to: C{P α α bQx } b †x where C is a context, and α and x are principal names of P α 4 P and Qx 4 Q, respectively. In other words we can always pick at least one representative of a congruence class cl(P αb †xbQ), which allows us to continue the computation at the top level. In what follows we first formulate two lemmas which focus on a single cut- name (either x or α) at a time, followed by the main theorem which addresses both cut-names. In proving the results we will use the transitivity of 4 relation: If P 4 Q and Q 4 R then P 4 R. Lemma 1 (Left-restructuring). For every term of the form P α b †xbQ, there exists a context C and a term P α , where α is a principal name for P α and P α 4 P , such that Pα bQ ≡ C{P α α b †x b †x bQ} Proof. By induction on the structure of P and case analysis. • The base case is when α is a principal name for P . Then we have P α = P and C = { }. • Assume that the property holds for the immediate subterms of P . The pos- sible cases for P are 1. P = yb M βb . γ, γ 6= α 2. P = M βb [y] zb N 3. P = M βb † ybN β P = x< xxc 1 c 4.&5. c 1 2 hM ] and P = [M iβc2 >β, β 6= α 6.&7. P = x M and P = M α, β 6= α We analyze the first 3 cases7 : 6 For the cases we prove here the set of congruence rules presented is sufficient. Pre- senting a complete proof would require to use all congruence rules. 7 Due to a limited space. ec1 y M βb . γ)b 1. (b α†x bQ ≡ yb (M α bQ) βb . γ b †x i.h. ≡ yb (C 0 {M α α bQ}) βb . γ b †x α , C{M α b †xbQ}, with C{ } = yb (C 0 { }) βb . γ 2. (a) Case α ∈ M. ci1 i.h. α†x (M βb [y] zb N )b bQ ≡ (M α bQ) βb [y] zb N ≡ (C 0 {M α α b †x b †x bQ}) βb [y] zb N , C{M α α b †x bQ}, with C{ } = (C 0 { }) βb [y] zb N (b) Case α ∈ N. ci2 i.h. α†x (M βb [y] zb N )b bQ ≡ (M α bQ) βb [y] zb N ≡ (C 0 {M α α b †x b †x bQ}) βb [y] zb N , C{M α α b †x bQ}, with C{ } = M βb [y] zb (C 0 { }) 3. (a) Case α ∈ M. cc1 (M βb † ybN )b α†x bQ ≡ (M α b †x bQ)βb † ybN i.h. ≡ (C 0 {M α α b †x bQ})βb † ybN α , C{M α b †xbQ}, with C{ } = (C 0 { })βb † ybN (b) Case α ∈ N. cc2 (M βb † ybN )b α†x bQ ≡ M βb † yb(N α b †x bQ) i.h. ≡ M βb † yb(C 0 {N α α b †x bQ}) , C{N α αb †x bQ}, with C{ } = M βb † yb(C 0 { }) The proof goes similarly for other cases. Lemma 2 (Right-restructuring). For every term of the form P α b†xbQ, there exists a context C and a term Qx , whose principal name is x and Qx 4 Q, such that b †x Pα bQ ≡ C{P α b †x bQx } Proof. Similarly as previous lemma, by induction on the structure of Q and case analysis. The following theorem confirms that the top level cut evaluation is complete, in a sense that there always exists a representative of a congruence class which enables cut evaluation at the top level relative to its cut-names. It also shows that in the presence of congruence rules we do not need prop- agation rules. Propagation rules in the ∗X calculus can be seen as means to perform restructuring of terms. However their existence blurs the core part of classical computation, and at the same time don’t enable restructuring of normal forms (terms that do not contain cuts). b†x Theorem 1. For every term of the form P α bQ there exists a context C and terms P α and Qx whose principal names are α, x respectively, and P α 4 P , Qx 4 Q, such that bQ ≡ C{P α α b †x Pα bQx } b †x Proof. By using the two previous lemmas, we construct the proof as follows: Lem. 1 b †x Pα bQ ≡ C1 {P α α b †x bQ} Lem. 2 ≡ C1 {C2 {P α α bQx }} b †x , C 0 {P α α bQx }, b †x with C 0 { } = C1 {C2 { }} And thus we are done. 6 Basic properties of ≡ The congruence relation describes the way to perform restructuring of terms and thus an important property is preservation of free names. Second important property is type preservation, which ensures that term-restructuring defined by ≡ can be seen as proof-transformation. Theorem 2 (Free names preservation). If P, Q are ∗X -terms, then the fol- lowing holds: If P ≡ Q then f n(P ) = f n(Q) Proof. The property can be checked by treating carefully each rule. Theorem 3 (Type preservation). Let S be an ∗X -term and Γ, ∆ contexts. Then the following holds: If S : · Γ ` ∆ and S ≡ S 0 , then S 0 : · Γ ` ∆ Proof. The proof goes by checking that the property holds for equations induc- ing ≡. We first write the typing derivation for the term on the left-hand side, and then for the term on the right-hand side of the equation. We prove several non-trivial cases. • Observe the first rule of exporter-importer group of rules: ei1 x b [z] yb Q) βb . α ≡ (b b (P γ x P βb . α) γ b [z] yb Q, with x, β ∈ f n(P ), x 6= z. On the one hand we have: P : · Γ, x : A ` β : B, γ : C, ∆ Q : · Γ 0 , y : D ` ∆0 (→ L) Pγ b [z] yb Q : · Γ, Γ 0 , x : A, z : C → D ` β : B, ∆, ∆0 (→ R) 0 0 x b [z] yb Q) βb . α b (P γ : · Γ, Γ , z : C → D ` α : A → B, ∆, ∆ On the other hand, P : · Γ, x : A ` β : B, γ : C, ∆ (→ R) b P βb . α x : · Γ ` α : A → B, γ : C, ∆ Q : · Γ 0 , y : D ` ∆0 (→ L) x P βb . α) γ (b b [z] yb Q : · Γ, Γ 0 , z : C → D ` α : A → B, ∆, ∆0 The proof goes similarly for the other cases. 7 Conclusion and future work We presented a detailed account of a possible step forward, towards the unveiling of the essential content of sequent classical proofs. This is done by declaring which syntactically different terms should be considered the same, i.e., by means of congruence rules which induce a congruence relation on terms. The framework for this is classical logic formalized in a standard sequent system with explicit structural rules, namely weakening and contraction. Indeed it was necessary to have all the details, structural as well as logical, to be able to state what are the unessential aspects and thus extract the essence in a systematic way. Clearly this is a base for studying the operational semantics towards defining a system with only the essential reduction rules, where reducing is reducing mod- ulo congruence relation. The congruence relation is proved to satisfy the minimal requirement of free names preservation, as well as that of type preservation. It is also possible to define a translation, call it D, from terms to diagrams in a natural way, inductively on the structure of terms (basic study is given in [18]). A similar approach was taken in [9], when interpreting intuitionistic λlxr-terms (featuring explicit weakening and contraction) into proof-nets [7]. It is reasonable to expect the translation D to satisfy – P1 ≡ P2 then D(P1 ) = D(P2 ) D D – P1 → P2 then D(P1 ) → D(P2 ) D where P1 and P2 are ∗X -terms, and where → is a suitable reduction relation on diagrams. However this should be carefully studied and belongs in the domain of future work. Moreover, in terms of future work, this computational model may be relevant in relation to process session types and concurrency, as recent studies have shown that both linear intuitionistic [3] and linear classical logic [16], have a natural interpretation as protocols for concurrent process communication. Acknowledgments This paper was made possible by NPRP 7-988-1-178 from the Qatar National Research Fund (a member of Qatar Foundation). The statements made herein are solely the responsibility of the authors. References 1. Barbanera, F., Berardi, S.: A Symmetric Lambda Calculus for ”Classical” Program Extraction, TACS, pp. 495-515, 1994. 2. van Bakel, S., Lengrand, S. and Lescanne, P.: The language X : circuits, computa- tion and Classical Logic, Proc. 9th Italian Conf. on Theoretical Computer Science, vol. 3701, pp. 81-96, 2005. 3. Caires, L., Pfenning, F.: Session Types as Intuitionistic Linear Propositions, CON- COUR 2010, Lecture Notes in Computer Science, 6269 (2010), pp. 222–236. 4. Curien P.-L., Herbelin, H.: The duality of computation. In: Proc. 5 th ACM SIG- PLAN Int. Conf. on Functional Programming (ICFP’00). ACM, 2000, pp. 233–243. 5. Gentzen, G., Untersuchungen über das logische Schließen. Math. 39, (1935) 176– 210. 6. Ghilezan, S., Lescanne, P, and Žunić, D.: Computational interpretation of classical logic with explicit structural rules, draft. 7. Girard, J.-Y.: A new constructive logic: classical logic, Mathematical Structures in Computer Science, 1-3 (1991), pp. 255–296. 8. Herbelin, H.: C’est maintenant qu’on calcule, au cœur de la dualité, Université Paris XI ( Habilitation à diriger les recherches), 2005. 9. Kesner, D., Lengrand, S.: Resource operators for lambda-calculus, Information and Computation, vol. 205, pp. 419-473, 2007. 10. Lafont, Y.: Interaction nets. Proceedings of the 17th ACM symposium on Principles of programming languages, POPL, ACM Press, pp. 99–108, 1990. 11. Lengrand, S.: Call-by-value, call-by-name, and strong normalization for the clas- sical sequent calculus, Electronic Notes in Theoretical Computer Science, 86-4 (2003), pp. 714–730. 12. Robinson, E.: Proof Nets for Classical Logic, Journal of Logic and Computation, 13-5 (2003), pp. 777–797. 13. Troelstra, A. S., Schwichtenberg, H.: Basic Proof Theory, Cambridge University Press, 1996. 14. Urban, C.: Classical Logic and Computation, University of Cambridge (Ph.D. the- sis), 2000. 15. Urban, C., Bierman, G. M.: Strong normalisation of cut-elimination in classical logic. Fundamenta Informaticae 45 (1-2) (2001), 123–155, (appeared also at TLCA in 1999). 16. Wadler, P.: Propositions as Sessions, Proceedings of the 17th ACM SIGPLAN international conference on Functional programming, ACM SIGPLAN Notices, 47-9 (2012), pp. 273–286. 17. Whitehead, A. N., Russell, B.: Principia Mathematica 2nd Ed., Cambridge Uni- versity Press, 1925. 18. Žunić, D.: Computing With Sequent and Diagrams in Classical Logic - Calculi *X , c X and dX , Ph.D. thesis, ENS Lyon, France, 2007. URL: https://tel. archives-ouvertes.fr/tel-00265549