Formalizing a Named Explicit Substitutions Calculus in Coq

Abstract

Explicit Substitutions (ES) calculi are extensions of the calculus that internalize the substitution operation, which is a metaoperation, by taking it as an ordinary operation belonging to the grammar of the ES calculus. As a formal system, ES are closer to implementations of functional languages and proof assistants, and are useful for studying properties of such systems. Nevertheless, several ES calculi do not satisfy important properties related with the simulation of the -calculus, such as con uence on open terms, simulation of one step reduction, full composition and the preservation of strong normalization (PSN). The latter, which states that -terms without in nite reduction sequences can only be nitely reduced in the ES calculus, is easily lost in such extensions. In a recent work, D. Kesner developed the ex-calculus, which is the rst ES calculus that satis es all the good properties expected for an ES calculus. In this work we present a formalization of the ex-calculus in the Coq Proof Assistant, which is fully available at http://www.cic.unb.br/ flavio/publications.html.

-

An Explicit Substitutions (ES) calculus is an extension of the -calculus that internalizes the substitution operation by extending its grammar such as: t; u ::= x j x:t j t u j t[x=u] (1) where, beside the variable x, abstraction x:t and application t u, there is a term t[x=u] denoting an explicit substitution, i.e., a pending substitution that needs to wait to be performed [ 4 ]. The free occurrences of the variable x in t are bound in both x:t and t[x=u], as usual. As a formal system, an ES calculus is composed by a set of rewriting rules with two parts whose aim is to simulate the -calculus. The rst part is composed by a rule that starts the simulation of the -reduction, and the second part is used to explicitly perform the substitution operation. For instance, the x-calculus [ 18,19,24,5 ] is de ned by the following ? Corresponding author partially supported by FEMAT. rewriting system: ( x:t)u ! t[x=u] x[x=u] ! u y[x=u] ! y (t1 t2)[x=u] ! t1[x=u] t2[x=u] ( y:v)[x=u] ! y:v[x=u] (x 6= y) (x 6= y) where the rst rule starts the simulation of the -reduction and the other rules are responsible for executing, by propagating through the term's structure, the pending substitution operation. In this way, the -step ( x:(x y)) z ! z y can be simulated by ( x:(x y)) z ! (x y)[x=z] ! x[x=z] y[x=z] ! z y[x=z] ! z y.

Most of the de ned calculi follow one of two approaches: the rst one uses names for declaring variables as presented in (1). The advantage of this approach is that its terms are more readable, but -equivalence, i.e. the class of terms modulo renaming of bound variables, needs to be carefully manipulated. Therefore, implementations of such calculi are not straightforward. Calculi in this family include the x-, ex- [ 16 ], lxr- [ 17 ], sub- [21] and es-calculi [ 16 ]. The second approach uses de Bruijn indexes [ 8 ] to represent variables in such a way that each term has a unique representation and hence -equivalence is no longer necessary. For instance the -term ( x:(x y)) z is represented by ( (0 1))1, where the 1 inside the denotes the position of the variable y in a xed context, and the 1 outside the denotes the second variable in this context. Note also that the 0 is bound by the while the 1 inside it represents the same variable as 0 outside thus ( (0 1)) 0 represents ( x:(x y)) y. Therefore, -equivalence is not a problem in this approach, but an algebraic manipulation of indexes is necessary while performing substitutions. A simple example of calculus in this approach is given by the s-calculus [ 13 ] whose grammar, rules and an update function upik(b) are given by:

a; b ::= n j a j a b j a[n=b] ( a)b ! a[0=b] 8 n 1 if n > i < n[i=b] ! upi0(b) if n = i

: n if n < i (a1 a2)[i=b] ! a1[i=b] a2[i=b] ( a)[i=b] a[i + 1=b] ! upik( a) ! (upik+1(a))

n + i if n > k upik(n) ! n if n k upik(a1 a2) ! upik(a1) upik(a2)

In this calculus, the previous example can be simulated as follows: ( (0 1))1 ! (0 1)[0=1] ! 0[0=1] 1[0=1] ! up00(1) 0 ! 1 0. Examples of calculi with de Bruijn indexes are C [ 9 ], [ 1 ], se [ 14 ], susp [22] and ws [ 7 ].

The formalization presented in this work takes advantages of both approaches: it uses de Bruijn indexes to represent bound variables, while free variables are represented by named variables. This framework, called the locally nameless representation, is already available in Coq and a more detailed explanation of its advantages can be found in [ 6 ].

Formalizing Explicit Substitutions Calculi In this section we present the basic notions that will be used in our formalization of the ex-calculus1, an ES calculus with names, in the Coq proof assistant. The notion of terms is general and could be used for any calculus having the syntax as in (1). In fact, the notion of terms given below is an extension of the formalization of the -calculus presented in [ 6 ]. Terms are de ned over a signature of preterms whose set of variables is formed by the bound variables (pterm bvar), indexed by natural numbers, and named free variables (pterm fvar). Applications (pterm app), abstractions (pterm abs) and explicit substitutions (pterm sub) have the standard signature.

Inductive pterm : Set := j pterm bvar : nat ! pterm j pterm fvar : var ! pterm j pterm app : pterm ! pterm ! pterm j pterm abs : pterm ! pterm j pterm sub : pterm ! pterm ! pterm.

Notation t1 [t2 ] := (pterm sub t u).

Terms of the ex-calculus are de ned by an unary predicate over pre-terms. The intuition is that a term is a pre-term without dangling de Bruijn indexes. We extended the predicate term to pre-terms with explicit substitution as follows: Inductive term : pterm ! Prop := j term var : 8 x,

term (pterm fvar x ) j term app : 8 t1 t2,

term t1 ! term t2 ! term (pterm app t1 t2 ) j term abs : 8 L t1,

(8 x, x \notin L ! term (t1 ^ x )) ! term (pterm abs t1 ) j term sub : 8 L t1 t2,

(8 x, x \notin L ! term (t1 ^ x )) ! term t2 ! term (t1 [t2 ]). where term sub is the constructor that de nes the conditions for (t1 [t2 ]) to be a term. In this de nition, the expression (t1 ^ x ) represents the term obtained from t1 after replacing all the occurrences of the ith de Bruijn index that is in the scope of i binders for x, i.e., all the occurrences of 0 that is not in the scope of a binder, of 1 that is in the scope of one binder, of 2 that is in the scope of two binders, and so on, are replaced for x in t1 . The condition x \notin L avoids the capture of free variables by the substitution operation2. Therefore, if (t1 ^ x ) and t2 are terms then (t1 [t2 ]) is also a term. 2.1

The ex-calculus The ex-calculus [ 15 ] was the rst ES calculus that simultaneously satis es all the desired properties for an ES calculus: termination, con uence on open terms, 1 The full formalization is available at www.cic.unb.br/ flavio/publications.html 2 The details can be found in [ 6 ] simulation of one step -reduction, full composition and preservation of strong normalization (PSN). It is de ned by the following rewriting system ( x:t) u

!B t[x=u] x[x=u] !Var u t[x=u] !Gc t; if x 2= fv(t) (t v)[x=u] !App t[x=u] v[x=u] ( y:t)[x=u] !Lamb y:t[x=u] (t[y=v])[x=u] !Comp t[x=u][y=v[x=u]]; x 2 fv(v) and an equation for permutation of independent substitutions (2) (3) (4) t[y=v][x=u] =C t[x=u][y=v]; if x 2= fv(v) and y 2= fv(u) where the rewriting relation generated by the rules in (2) is denoted by Bx, and by x if one considers all the rules but B. The equivalence relation generated by the conversions and C is denoted by e, and the reduction relation generated by each rewriting relation modulo e speci es rewriting of e-equivalence classes as follows: t !ex t0 i t ! ex t0 i 9s; s0 such that t =e s !x s0 =e t0 9s; s0 such that t =e s !Bx s0 =e t0

The formalization of -equivalence is unnecessary due to the locally nameless representation, as explained in the introduction. Nevertheless, the formalization of the equivalence of terms modulo the equation (3) is not straightforward and constitutes an important contribution of this work. The reduction relations in (4) allow a, possible empty, permutation of substitutions before and/or after the rewriting step, and its formalization is done in several steps as explained below. First, we inductively de ne the permutation of independent substitutions: Inductive eqc : pterm ! pterm ! Prop := j eqc rf: 8 u, eqc u u j eqc rx: 8 t u v, term u ! term v ! eqc (t[u][v ]) ((& t)[v ][u]) . The constructor eqc rf de nes the re exivity of eqc, i.e., of equation (3), and eqc rx permutes two independent substitutions. The independence of the substitutions [u] and [v ] in t[u][v ] is assured by the conditions (term u) and (term v ) because no dangling bound variable is allowed to occur in terms. As a consequence, we have that eqc is also symmetric and transitive, and hence eqc de nes an equivalence relation. The permutation of independent substitutions done by the constructor eqc rx requires an adjustment of the indexes of the term t that is replaced by (& t := bswap rec 0 t), which is obtained from t after replacing each occurrence of the index bound to the substitution [u] by the one bound to the substitution [v ] and vice-versa. This swap of indexes is formally de ned by the idempotent recursive function bswap rec.

The parallel contextual closure of eqc is denoted by the permutation of independent substitutions in any position of a term. The parallel contextual closure generalizes the standard contextual closure by allowing applications of a reduction in parallel positions: (8 x, x \notin L ! p contextual closure eqc (t ^x ) (t' ^x )) ! p contextual closure eqc u u' ! p contextual closure eqc (t [u]) (t' [u' ])

So, in order to take advantage of rewriting facilities of Coq, we need to show the compatibility of ex-contexts w.r.t. the equivalence relation eqc. This means, for example, that two term applications that are eqc equivalent result in corresponding arguments are eqc equivalent. The same happens to abstractions and explicit substitutions eqc equivalent terms. In this way, one can directly replace equivalent ex-terms using the rewrite tactic of Coq [26]. For this purpose, and since (p contextual closure eqc) is no longer transitive, we de ned the transitive parallel contextual closure of eqc, denoted by =e.

Finally, the reduction relation in (4) is parametrized by a relation R as follows: 9 t' u' , (t =e t' )/\(contextual closure R t' u' )/\(u' =e u), where R will be instantiated either with ex or lex.

The rewriting rules in (2) are formalized via binary predicates over the set of pre-terms. Therefore, the rule B, here called rule b, has type pterm ! pterm ! Prop, where the rst argument corresponds to the left hand side of the rule, and the second argument corresponds to its right hand side: Inductive rule b : pterm ! pterm ! Prop := reg rule b : 8 (t u:pterm), body t ! term u !

rule b (pterm app(pterm abs t ) u) (t [u]).

Notation "t ! B u" := (rule b t u).

The system x, called sys x, is given by the remaining rules in (2). The rules Lamb and Comp need to take into account the correct manipulation of bound variables in t while propagating the substitution over a binder operator. In particular, the conditions body (t [u]) and :term u in reg rule comp assure that the substitutions [u] and [v ] are not independent.

Inductive sys x : pterm ! pterm ! Prop := j reg rule var : 8 t, term t ! sys x (pterm bvar 0 [t ]) t j reg rule gc : 8 t u, term t ! term u ! sys x (t [u]) t j reg rule app : 8 t1 t2 u, body t1 ! body t2 ! term u !

sys x ((pterm app t1 t2 )[u]) (pterm app (t1 [u]) (t2 [u])) j reg rule lamb : 8 t u, body (pterm abs t ) ! term u !

sys x ((pterm abs t )[u]) (pterm abs ((& t )[u])) j reg rule comp : 8 t u v, body (t [u]) ! : term u ! term v ! sys x (t [u][v ]) (((& t )[v ])[ u[ v ] ]).

Notation "t ! x u" := (sys x t u).

The result of the (implicit) substitution, replacing all occurrences of index 0 (at the root level), of term t by a term u is written (t ^^ u).

The rst non-trivial property that is proved is called full composition: it states that the explicit substitution simulates the implicit substitution of the -calculus and nothing else:

Lemma full comp: 8 t u, body t ! term u ! t [u] -->ex+ (t ^^ u). Proof. The proof is done by induction on t as in [ 15 ], but the induction principle need to be adapted to the locally nameless notation because t is not a term in this notation. In fact, t is a body, and hence the induction is on the body structure. Apart from this, everything else runs as in the original proof.

The simulation of one step -reduction is another important property of ES calculi. It states that one step -reduction in the -calculus can be simulated in the ES calculus in a nite number of steps:

Lemma sim beta reduction : 8 t t', (t -->Beta t' ) ! (t -->lex* t' ). Proof. The proof is done by induction on t -->Beta t' . For the base case one has to show that pterm app (pterm abs t) u -->lex* (t ^^ u), which after an application of rule b reduces to t [u] -->ex+ (t ^^ u), and we conclude by lemma full comp. The inductive cases are straightforward.

The strategy above can be simulated in the ex-calculus as stated by the following lemma. And so we proved that it is deterministic, fact that is only stated in [ 15 ]. Both proofs are done by induction followed by inversion on the strategy

:

Lemma perp proposition : 8 t t', term t ! (t

t' ) ! (t -->lex+ t' ).

Lemma det many step : 8 t u v, term t ! ((t

u) ^ (t v ) ! u = v ).

The PSN proof for the ex-calculus relies on the fact that strong normalization can be inductively de ned. The so called IE property establishes the conditions for a term to be strongly normalizing in the ex-calculus. A term is strongly normalizing (SN) if every reduction sequence starting from it is nite. Therefore, the SN predicate inductively characterizes when a term t is strongly normalizing w.r.t. a reduction relation R by assuring the existence of a natural number n that bounds the maximum size of any reduction from t. Inductive SN ind (n : nat) (R : pterm ! pterm ! Prop) (t : pterm) : Prop := j SN intro : (8 t', R t t' ! 9 k , k < n ^ SN ind k R t' ) ! SN ind n R t. Definition SN R t := 9 n, SN ind n R t.

The PSN property for the ex-calculus is proved under the hypothesis that IE holds. We are currently working on the formalization of the IE property, but it is not straightforward, as shown in [ 15 ].

Hypothesis IE property : 8 t u lv, body t ! term u ! SN lex u ! SN lex ((t ^^ u) // lv ) ! SN lex ((t[u]) // lv ).

A perpetual strategy gives either an in nity reduction sequence of a term when it exists, or a reduction sequence leading to some normal form. The theorem perpetuality states that the many step strategy is perpetual by relating it with the SN predicate.

Theorem perpetuality : 8 t t', term t ! (t t' ) ! SN lex t' ! SN lex t.

Proof. The proof is by induction on the strategy many step. The IE property is used in the base case for the rule p subst1.

An inductive characterization of strongly normalizing terms is very convenient because it simpli es proofs. The predicate ISN characterizes the set of strongly normalizing terms in the ex-calculus. This claim is proved by the lemma ISN prop which states the equivalence between ISN and SN lex . Inductive ISN : pterm ! Prop := j isn var : 8 (x : var) (lu : list pterm),

(8 u, (In u lu) ! ISN u) ! ISN ((pterm fvar x ) // lu) j isn NF : 8 (u : pterm),

NF lex u ! ISN u j isn app : 8 (u v : pterm) (lu : list pterm),

ISN (u[v ] // lu) ! ISN ((pterm app (pterm abs u) v ) // lu) j isn subs : 8 (u v : pterm) (lu : list pterm),

ISN ((u ^^ v ) // lu) ! ISN v ! ISN (u[v ] // lu) j isn abs : 8 L (u : pterm), (8 x, x \notin L ! ISN (u ^ x )) ! ISN (pterm abs u) .

The preservation of strong normalization for the ex-calculus is proved by showing that every -term without in nite reduction sequences do not have in nite reduction sequences in the ex-calculus, i.e., if a -term t is strongly normalizing then it is also strongly normalizing in the ex-calculus.

Lemma ISN prop : 8 t, term t ! (ISN t $ SN lex t ).

Theorem PSN : 8 t, Lterm t ! SN Beta t ! SN lex t.

Proof. The proof is done by induction on SN Beta t, de ned as follows [27]: Inductive SN Beta : pterm ! Prop := j sn beta var : 8 (x : var) (lu : list pterm),

(8 u, (In u lu) ! SN Beta u) ! SN Beta ((pterm fvar x ) // lu) j sn beta abs : 8 L (u : pterm),

(8 x, x \notin L ! SN Beta (u ^ x )) ! SN Beta (pterm abs u) j sn beta meta sub : 8 (t u : pterm) (lv : list pterm),

SN Beta u ! SN Beta ((t ^^ u) // lv ) ! SN Beta ((pterm app (pterm abs t ) u) // lv ).

The full formalization follows [ 15 ] and is divided in 5 Coq les that sum up about 4000 lines of code, excluding the framework provided by [ 6 ]. Related work There is a formalization of the -calculus proving its con uence [25]. In [ 12 ], termination of both the - and s-calculus are formalized in ALF [ 11 ]. Nevertheless, both the - and the s-calculus uses de Bruijn indexes and do not have equations, and hence its formalization do not need a framework for dealing with equivalence classes of terms.

The framework in [ 6 ] was used in the formalization of the full composition property for the untyped structural -calculus [23]. 3

Conclusion and Future Work Formalization of ES calculi are important because they form the theoretical basis for the implementation of functional languages and proof assistants. In this way, ES calculi allow, as a formal framework, not only the study of properties and further improvements of the implemented systems, but also the study of the -calculus itself [ 3 ].

In this work, we presented a formalization of the ex-calculus in Coq using a framework based on locally nameless representation [ 6 ]. In this formalization we proved that the ex-calculus satis es a number of interesting properties such as full composition, simulation of one step -reduction and that the many step strategy, which can be simulated in the ex-calculus, is used to characterize strongly normalizing terms. Assuming the IE property, we proved that the excalculus enjoys the PSN property.

As future work, we will formalize the IE property and metacon uence, i.e., con uence on open terms for the ex-calculus. This will provide a complete formalization of the ex-calculus. We will investigate whether our formalization could be adapted to formalize other calculi that uses names instead of de Bruijn indexes, such as the family of ES calculi that acts at a distance [ 21,2 ]. 18. R. Lins. A new formula for the execution of categorical combinators. 8th Conference on Automated Deduction (CADE), volume 230 of LNCS:89{98, 1986. 19. R. Lins. Partial categorical multi-combinators and church rosser theorems. Technical Report 7/92, Computing Laboratory, University Kent at Canterbury, May 1992. 20. P.-A. Mellies. Typed -calculi with explicit substitutions may not terminate. In

Proceedings of TLCA'95, volume 902 of LNCS. Springer-Verlag, 1995. 21. R. Milner. Local bigraphs and con uence: Two conjectures: (extended abstract).

ENTCS, 175(3):65{73, 2007. 22. G. Nadathur and D. S. Wilson. A Notation for Lambda Terms: A Generalization of Environments. TCS, 198:49{98, 1998. 23. Fabien Renaud. Les ressources explicites vues par la theorie de la reecriture. PhD thesis, 2011. 24. K. Rose. Explicit cyclic substitutions. In Michael Rusinowitch and Jean-Luc Remy, editors, 3rd International Workshop on Conditional Term Rewriting Systems (CTRS), volume 656, pages 36{50. Springer-Verlag, 1992. 25. A. Sabi. Formalization of a lambda-Calculus with Explicit Substitutions in Coq. In TYPES '94: Selected papers from the International Workshop on Types for Proofs and Programs, pages 183{202, London, UK, 1995. Springer-Verlag. 26. M. Sozeau. A new look at generalized rewriting in type theory. J. Formalized

Reasoning, 2(1):41{62, 2009. 27. F. van Raamsdonk. Con uence and Normalization for Higher-Order Rewriting.

PhD thesis, Amsterdam University, Netherlands, 1996.

References

1. M. Abadi , L. Cardelli , P.-L. Curien , and J.-J. Levy. Explicit Substitutions . Journal of Functional Programming , 1 ( 4 ): 375 { 416 , 1991 .

2. B. Accattoli and D. Kesner . The structural lambda-calculus . In 19th EACSL Annual Conference on Computer Science and Logic (CSL) , volume 6247 of LNCS , pages 381 { 395 . Springer-Verlag, 2010 .

3. B. Accattoli and D. Kesner . The permutative lambda calculus . In Nikolaj Bj rner and Andrei Voronkov , editors, LPAR , volume 7180 of Lecture Notes in Computer Science, pages 23 { 36 . Springer, 2012 .

4. M. Bezem , J. W. Klop , and R. de Vrijer, editors. Term Rewriting Seminar { Terese . Cambridge University Press, 2003 .

5. R. Bloo and K. Rose . Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection . In CSN-95: COMPUTER SCIENCE IN THE NETHERLANDS , pages 62 { 72 , 1995 .

6. A. Chargueraud . The Locally Nameless Representation . Journal of Automated Reasoning , pages 1 { 46 , 2011 .

7. R. David and B. Guillaume . A lambda-calculus with explicit weakening and explicit substitution . Mathematical Structures in Computer Science , 11 ( 1 ): 169 { 206 , 2001 .

8. N. G. de Bruijn. Lambda-Calculus Notation with Namefree Formulas Involving Symbols that Represent Reference Transforming Mappings . Indag. Mat., 40 : 348 { 356 , 1978 .

9. N. G. de Bruijn . A namefree lambda calculus with facilities for internal de nition of expressions and segments . Technical Report T.H.-Report 78-WSK-03 , Technische Hogeschool Eindhoven, Nederland, 1978 .

10. B. Guillaume . The s e-calculus Does Not Preserve Strong Normalization . J. of Func. Programming , 10 ( 4 ): 321 { 325 , 2000 .

11. M. Hanus . The alf system . In PLILP , pages 423 { 424 , 1991 .

12. F. Kamareddine and H. Qiao . Formalizing strong normalization proofs of explicit substitution calculi in alf . Journal of Automated Reasoning , 30 ( 1 ): 59 { 98 , 2003 .

13. F. Kamareddine and A. R os. A -calculus a la de Bruijn with Explicit Substitutions . In Proc. of PLILP'95 , volume 982 of LNCS , pages 45 { 62 . Springer, 1995 .

14. F. Kamareddine and A. R os. Extending a -calculus with Explicit Substitution which Preserves Strong Normalisation into a Con uent Calculus on Open Terms . Journal of Functional Programming , 7 : 395 { 420 , 1997 .

15. D. Kesner . Perpetuality for full and safe composition (in a constructive setting) . In Luca Aceto , Ivan Damgard, Leslie Ann Goldberg, Magnus M. Halldorsson , Anna Ingolfsdottir, and Igor Walukiewicz, editors, ICALP (2) , volume 5126 of Lecture Notes in Computer Science, pages 311 { 322 . Springer, 2008 .

16. D. Kesner . A Theory of Explicit Substitutions with Safe and Full Composition . Logical Methods in Computer Science , 5 ( 3 :1):1{ 29 , 2009 .

17. D. Kesner and S. Lengrand . Resource operators for the -calculus . Information and Computation , 205 : 419 { 473 , April 2007 .