A congruence relation for restructuring classical terms

Abstract

We present a congruence relation on sequent-style classical proofs which identi es proofs up to trivial rule permutation. The study is performed in the framework of X calculus which provides a CurryHoward 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 classifying proofs (terms) which are syntactically di erent 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.

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 con uent 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 di erent 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 ].

Related work

The rst 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 capturing 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 substitution, 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 formalized in the sequent calculus with explicit structural rules weakening and contraction. Terms are built from names. This concept di ers essentially from the one applied in -calculus, where variable is the basic notion. The di erence 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 de ned 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.

De nition 1. The syntax of X -calculus3 is presented in Fig. 1, where x; y; z::: range over an in nite set of in-names and ; ; ::: range over an in nite set of out-names.

P; Q ::= hx: i j xb P b : j P b [x] yb Q j P b y xbQ j x P j P j z< xybhP ]

b j [P ibb > capsule exporter importer cut left-eraser right-eraser left-duplicator right-duplicator

(axiom rule) (ritht arrow-introduction) (left arrow-introduction)

(cut) (left weakening) (right weakening) (left contraction) (right contraction)

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.

De nition 2. We de ne free names and principal names of a term R, written f n(R) and pn(R), respectively, in the following way:

R hx: i x P b : b P b [x] yb Q P b y xbQ x P P

f n(R) x; f n(P )nfx; g [ f n(P ) [ f n(Q)nf ; yg [ x f n(P ) [ f n(Q)nf ; xg f n(P ) [ x f n(P ) [ pn(R) x;

x none x x< xxc12hP ] f n(P )nfx1; x2g [ x x

c [P icc21 > f n(P )nf 1; 2g [

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 operation, 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 de nition of linear terms, see [ 18 ] on page 43. We will specify the notions of context, subterm and immediate subterm in order to e ciently work with the structure of terms.

De nition 3. The contexts are formally de ned as follows:

Cf g ::= j j j j j f g f g b [x] yb Q f gb y xbQ x f g z< xybbhf g] CfCf gg j j j j j xb f g b : P b [x] yb f g P b y xbf g f g [f gibb >

Informally, a context is a term with a hole which can accept another term. Therefore CfP g denotes placing the term P in the context Cf g. De nition 4. A term Q is a subterm of a term P , denoted as Q 4 P if there is a context Cf g such that P = CfQg (the symbol = stands for syntactic equality.). It is easy to show that the subterm relation is re exive, antisymmetric and transitive (i.e., is an order).

De nition 5. A term Q is an immediate subterm of P if P = CfQg and Cf g =6 C0fC00f gg; Cf g =6 f g. 4

The type assignment system

Given a set T of basic types, a type is given by A; B ::= A 2 T j 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 innames and out-names of P , respectively4. Comma in the expression ; 0 stands for the set union.

De nition 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. (R!) ` A; ; 0; A ! B ` 0; B `

0 A ` A (ax) ` ; A ` ; A; A ` ; A ` (weak-L) (cont-L) (L!) ` A; ; 0 `

Reduction rules are numerous as they capture the richness and complexity of classical cut elimination, and very ne-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 represented 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 ].

hx: i : x :A ` :A (ax) P : `

:A; P b [x] yb Q :

Q : 0; y :B `

0 ; 0; x :A ! B ` (L!)

P : x P b : : b ; x :A `

:B; ` :A ! B; (R!) P : ` ; x :A ` P :

P : x P :

; x :A; y :A ` z< xybhP ] : b ; z :A ` `

:A; P b y xbQ : (weak-L) (cont-L)

Q : ; 0 ` 0; x :A ` :A; :A; : A; `

:A; is a re exive, symmetric and transitive relation closed under any context. These rules de ne explicitly and in an intuitive way which syntactically di erent terms should be considered the same. The key property of this congruence relation is that, given a cut term, it o ers 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) x P γβ I

y Q E α

z ei1 : xb (P b [z] y Q) b :

b ei2 : xb (P b [z] yb Q) b : (x P b : ) b [z] yb Q

Pbb [z] yb (xb Q b : ) exporter-cut (1)

γ x P β

E α y Q (2)

P γ z I yx Q β

E

α with x; with x; 2 f n(P ) 2 f n(Q) (2)

P γ yx Q β

E α ec1 : xb (P b y ybQ) b : ec2 : xb (P b y ybQ) b : importer-importer (1)

β P α I y Q x z

I t R cut-cut (1)

β P α

x Q cc1 : (P b y xbQ) b y ybR cc2 : (P b y xbQ) b y ybR cc3 : P b y xb(Q b y ybR) cut-importer

β P α I y Q

x (1) (3) ii1 : (P b [x] ybQ) b [z] btR (P b [z] btR) b [x] ybQ ii2 : (P b [x] ybQ) b [z] btR P b [x] yb(Q b [z] btR) ii3 : (Q b [z] btR) Q b [z] bt(P b [x] ybR) ci3 : P b y xb(Q b [y] zbR) ci4 : P b y xb(Q b [y] zbR) (P b y xbQ) b [y] zbR

Q b [y] zb(P b y xbR) z R y (2) (2) ci1 : (P b [x] y Q) b y zbR

b ci2 : (P b [x] ybQ) b y zbR (P b y zbR) b [x] ybQ

P b [x] yb(Q b y zbR) P α x Q β I z R (4)

P α (x P b : )b y ybQ b P b y yb(xb Q b : )

P α I y Q β I t R x

z y R

P α x Q β y R

P α (P b y ybR)b y xbQ P b y xb(Q b y ybR) Q b y yb(P b y xbR) (3) (3) with x; 2 f n(P ) with x; 2 f n(Q) P α I

y

Q β I t R x

z with ; 2 f n(P ) with y; 2 f n(Q) with y; t 2 f n(R)

Q β x y R with ; 2 f n(P ) with x; 2 f n(Q) with x; y 2 f n(R) with ; 2 f n(P ) with y; 2 f n(Q)

x Q β I z R

y with x; 2 f n(Q) with x; z 2 f n(R) (2)

P α I y Q β

z R x x1 x2 P α

y Q α1 P βα2 α

y Q (1)

x (3) (1) (2) (4)

P α x x1 xy2 Q with x1; x2 2 f n(P ) with x1; x2 2 f n(Q); y 6= x

P β y

α1 Q α2

α (2)

C

P

α x 2= f n(CfP g) 2= f n(CfP g) cct1 : x< xxc12hP b y ybQ]

c cct2 : x< xxc21hP b y ybQ] c (x< xxc21hP ])b y ybQ

c P b y yb(x< xxc12hQ])

c cct3 : [P b y ybQi c21 >

c cct4 : [P b y ybQi c21 >

c weak-general x

C

P wg1 : x (CfP g) wg2 : (CfP g)

Cfx CfP

P g

g ([P i c21 > ) b y ybQ

c P b y yb([Qi c21 > ) c with 1; 2 2 f n(P );

6= with 1; 2 2 f n(Q) 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 nitely many terms, and thus nitely 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 preservation 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 restructuring 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: 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 de ned in the previous section6 - to:

CfP

b y xbQxg 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 y xbQ), which allows us to continue the computation at the top level.

In what follows we rst formulate two lemmas which focus on a single cutname (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 y xbQ, there exists a context C and a term P , where is a principal name for P and P 4 P , such that

P b y xbQ

CfP 6 For the cases we prove here the set of congruence rules presented is su cient. Presenting a complete proof would require to use all congruence rules. 7 Due to a limited space.

ec1

y (M b y xbQ) b : i:h: b y (C0fM b , CfM

b y xbQg) b : b y xbQg; with Cf g = yb (C0f g) b : , CfM

b y xbQg; , CfM

b y xbQg; cc1 i:h:

(C0fM , CfM (M b [y] zb N )b y xbQ ci1 (M b y xbQ) b [y] zb N i:h: (M b [y] zb N )b y xbQ ci2 (M b y xbQ) b [y] zb N i:h: (M b y ybN )b y xbQ

(M b y xbQ) b y ybN 2: (a) Case (b) Case exists a context C and a term Qx, whose principal name is x and Qbxy4xbQQ,, tshuecrhe Lemma 2 (Right-restructuring). For every term of the form P that

P b y xbQ

CfP b y xbQxg

Proof. Similarly as previous lemma, by induction on the structure of Q and case analysis.

The following theorem con rms 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 propagation 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).

Theorem 1. For every term of the form P b y xbQ there exists a context C and terms P and Qx whose principal names are ; x respectively, and P 4 P ,

P b y xbQ

CfP b y xbQxg

Proof. By using the two previous lemmas, we construct the proof as follows: , 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 de ned by can be seen as proof-transformation.

Theorem 2 (Free names preservation). If P; Q are X -terms, then the following 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 ; Then the following holds: If S : and S S0, then S0 : ` ` contexts.

Proof. The proof goes by checking that the property holds for equations inducing . We rst 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 rst rule of exporter-importer group of rules: xb (P b [z] yb Q) b : the one hand we have: ei1 (xb P b : ) b [z] yb Q, with x; 2 f n(P ); x 6= z. On xb (P b [z] ybQ) b : : ; 0; z : C ! D ` The proof goes similarly for the other cases. 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 di erent 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 de ning a system with only the essential reduction rules, where reducing is reducing modulo 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 de ne 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 { P1 !D P2 then then

D(P1) = D(P2)

D(P1) !D D(P2) where P1 and P2 are X -terms, and where !D 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. 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, computation 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 , CONCOUR 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 SIGPLAN Int. Conf. on Functional Programming (ICFP'00) . ACM, 2000 , pp. 233 { 243 .

5. Gentzen , G. , Untersuchungen uber das logische Schlie en . Math. 39 , ( 1935 ) 176 { 210 .

6. Ghilezan , S. , Lescanne , P , and Zunic , 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 dualite, Universite Paris XI ( Habilitation a 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 classical 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. thesis) , 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 University Press, 1925 .

18. Zunic , 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