Rewriting with Extensional Polymorphic λ-calculus

Roberto Di Cosmo^{1} and Delia Kesner^{2}

1 LIENS (CNRS) - DMI Ecole Normale Supérieure 45, Rue d’Ulm 75005 Paris - France, E-mail: roberto@dicosmo.org 2 CNRS and LRI Bât 490, Université de Paris-Sud 91405 ORSAY Cedex, France, E-mail: kesner@lri.lri.fr

Abstract. We provide a confluent and strongly normalizing rewriting system, based on expansion rules, for the extensional second order typed lambda calculus with product and unit types: this system corresponds to the Intuitionistic Positive Calculus with implication, conjunction, quantification over proposition and the constant T rue. This result is an important step towards a new theory of reduction based on expansion rules, and gives a natural interpretation to the notion of second order η-long normal forms used in higher order resolution and unification, that are here just the normal forms of our reduction system.

1 Introduction

Typed lambda calculus provides a convenient framework for studying functional programming and offers a natural formalism to deal with proofs in intuitionistic logic. It comes traditionally equipped with a fundamental computational mechanism, which is the β equality (λx.M)N = M[N/x], and with a minimal tool for reasoning about programs, which is the η extensional equality λx.Mx = M. This basic calculus can then be extended by adding further types, like products, unit and second order types, each coming with its own computational mechanism and/or its extensional equalities.

This work provides a confluent and stronlgy normalizing rewriting system for second order lambda calculus equipped with extensionality axioms for the products and for the arrow type, no longer oriented as contractive rules, but, according to the now growing practice [Aka93, Dou93, DCK94b, Cub92, DCK94a, DCP95, JG92], as expansive rewriting rules.

Using expansive rewrite rules, in a controlled fashion, allows us to obtain a simple canonical system that can be used to decide equality, has the second order Huet’s βη-long normal forms as normal forms and is naturally compatible with rules that break confluence when added to systems with contractive rules for extensional equalities. This is the case, for example, of the special unit type T and the rule M : T ⟶ ∗ : T that one needs to define the extensional first order lambda calculus associated to Cartesian Closed Categories. Another example is the extensional first order lambda calculus enriched with a confluent algebraic rewriting system, where confluence is also broken by contractive rules [DCK94a].

As has been noticed before, the expansive interpretation of extensional rules is not new, but has been neglected for a long time, so that the theory of lambda calculus with expansion rules is far from being fully developed: even for ηcontraction, that has been extensively studied for a long time, a satisfactory treatment has been provided only recently [Geu92].

A first positive result for polymorphic systems is presented in [DCP95], but just for the first order expansive η rule: unfortunately, the proof technique used there, which is based essentially on η postponement, does not extend to polymorphic η expansion nor to expansive surjective pairing.

Here we provide a proof of confluence and normalization for the full polymorphic system with the extensionality of arrow, product and universal types turned into expansive rules. Since the rewriting relation with controlled expansive rules is not a congruence and is not stable by substitution, we cannot use the traditional reducibility proofs, that strongly rely on these properties.

Our proof is based on a modification of Girard’s reducibility candidates, as first suggested for the first order calculus in [Jay92], that requires some careful reordering of the traditional lemmas in Girard’s proof, but works homogeneously for products as well as arrow and polymorphic types. A related approach has been independently taken in [Gha95] for the fragment without products and terminal object: there a different modification of reducibility is introduced, which seems very promising.

It is worth noting that the expansive interpretation of extensional equalities does not fit the various higher order schemes proposed for example in [Klo80, JO91, Nip90], as those schemes do not allow the left hand side of the reduction rules to be a single higher-order variable.

We also present a simple argument that allows to add in a fully modular way the special rule for the unit type to any rewriting system, preserving normalization.

Overall, this provides us with first canonical rewriting system for the full polymorphic extension of the first order lambda calculus associated to Cartesian Closed Categories, an important step towards a full theory of expansive extensionality.

1.1 Brief Survey

Several proof techniques have been developed to tackle the expansionary interpretation of the extensional equalities, and show that it yields a confluent and normalizing system in the first order case. One idea is to try to separate the expansion rules from the rest of the reduction, and then try to show some kind of modularity of the reduction systems. In [Aka93] this is done by means of the following property:

Lemma 1. Let S and R be confluent and strongly normalizing reductions, s.t.

∀M, N (M ⟹^{R} N) implies (M^{S}⟹^{R}+N^{S})

where M^{S} is the S normal form of M, then S ∪ R is also confluent and strongly normalizing.

The lemma applies to S taken as the expansions and R the usual reductions. In [DCK94b], we reduced confluence and strong normalization of the full expansionary system to that of the traditional one without expansions using another modular technique based on a translation.

A different non-modular approach is taken in [JG92] and [Dou93], where the proofs of strong normalization are based on an extension of the traditional techniques of reducibility and allow to handle also the peculiarity of the expansion rules. But that is not all, since one is left to prove weak confluence separately, which is not an easy task in the presence of expansion rules, as the rewrite relation is not a congruence (see [DCK94b] for details).

An even different technique is used in [Cub92], where confluence is shown by a careful study of the residuals in the reduction.

Finally, in [DCP95], one finds a simple general lemma, that appears also in [Ges90], and that is today the most satisfactory tool to handle the addition of expansion rules to first order systems, since it is fully modular and extremely easy to apply.

Lemma 2. Let ⟨A, R, S⟩ be an Abstract Reduction System, where R-reduction is strongly normalizing. Let the following commutation hold

∀a, b, c, d ∈ A [figure: \begin{matrix}a & c \\ b & d \end{matrix}; R; S; S; +; R]

Then S^{∗} and R^{+} commute, so, in particular, S^{∗} and R^{∗} commute.

Since the union of two confluent reductions that commute is confluent, this lemma gives an easy way of proving confluence modularly: in particular, if we take expansive η and SP as S, and the rest of the system as R, all first order systems cited above satisfy the lemma, so confluence comes up immediately from the separate confluence of the expansions alone and of the non expansive subsystems.

As for normalization, if R preserves S normal forms, and S and R are both confluent and normalizing, it is easy to see that commutation also entails the hypothesis of Akama’s lemma, so also normalization comes up modularly. This is the case in all first order systems: since the type of any subterm do not evolve during reduction, expansive normal forms are preserved, so one gets immediately strong normalization for the full system.

For these reasons, we can consider that the treatment of expansive rules in first order systems is nowadays fully satisfactroy. Unfortunately, in the presence of second order quantification, the type of a subterm can evolve during evaluation, and this fact allows us to build very simple examples suggesting that the modular approaches [Aka93, DCK94b, DCP95] cannot be satisfactorily extended to the second order case, and we have to go back and have a better look at reducibility candidates.

Expansions and polymorphism are not modular The following simple example shows that we cannot use the modular techniques developed up to now to separate the complexities introduced by expansion rules and polymorphic typing.

Example 1. Let M = (ΛX.(x[X → X])(λy : X.y))[A × B] where x : ∀Z.(Z → A) and A and B are base types. Then, the term M is a normal form w.r.t expansion rules, but its immediate β^{2} reduct is not:

M′ = (x[A × B → A × B])(λy : A × B.y)

In fact, M′ reduces to the term

M′′ = (x[A × B → A × B])(λy : A × B.⟨π_{1}(y), π_{2}(y)⟩)

Now, there is no way to reduce M to M′′ without using expansions, so the hypothesis of lemma 1 are not satisfied, and then also lemma 2 is no good, since it relies on Akama’s lemma for normalization.

This same example can be used to show how the use of expansor terms of [DCK94b] is neither viable.

Our approach Since the modular techniques are not viable, we focused on the reducibility predicates defined in [JG92] for the first order calculi with expansion rules, and we adapt the strong normalization proof to handle both second order quantification and expansion rules, by a careful reorganisation of the traditional arguments.

One fundamental difference between the proof for the simply typed and the proof for polymorphic lambda calculus is that one does not work with just one reducibility candidate, but with all reducibility candidates at once. This requires to deal with many subtle points in the second order case that do not appear in the first order case.

We define the calculus in section 2 and we show weak confluence of the full reduction system in section 3. We then give the proof of strong normalization in section 4, add the Top type in section 5 and we finally conclude with some ideas for further work.

2 The Calculus

We consider a denumerable set of atomic types and a denumerable set of type variables. The set of types of our calculus can be defined by the following grammar:

A ::= ι | X | A × A | A → A | ∀X.A

where ι ranges over the set of atomic types and X over the set of type variables.

Variables are typed by the following axiom:

x_{1} : A_{1}, …, x_{n} : A_{n} ⊢ x_{i} : A_{i} (1 ≤ i ≤ n)

where the x_{j}’s are pairwise distinct.

And terms are typed by the following rules:

\frac{Γ, x : A ⊢ M : B}{Γ ⊢ λx : A.M : A → B} \frac{Γ ⊢ M : A → B Γ ⊢ N : A}{Γ ⊢ (MN) : B}

\frac{Γ ⊢ M_{1} : A_{1} Γ ⊢ M_{2} : A_{2}}{Γ ⊢ ⟨M_{1}, M_{2}⟩ : A_{1} × A_{2}} \frac{Γ ⊢ M : B_{1} × B_{2}}{Γ ⊢ π_{1}(M) : B_{1}} \frac{Γ ⊢ M : B_{1} × B_{2}}{Γ ⊢ π_{2}(M) : B_{2}}

\frac{Γ ⊢ M : A X not free in the type of any x ∈ F V (M)}{Γ ⊢ ΛX.M : ∀X.A}

\frac{Γ ⊢ M : ∀X.A}{Γ ⊢ M[B] : A[B/X]}

We write M : A is M has type A under some context Γ. The set of free variables of a term M, denoted F V (M) is defined as usual. If M is a term and θ a substitution, Mθ is the term M where each x ∈ F V (M) is replaced by θ(x). Substitutions are typed, in the sense that the substituted variable and term must have the same type.

We identify terms up to α-conversion, i.e. renaming of bound variables. The reduction rules are the following (we refer the interested reader to [DCK94b] for a discussion of the restrictions on the expansion rules):

(β) (λx : A.M)N ⟶^{β} M[N/x]
(β^{2}) (ΛX.M)[A] ⟶^{β^{2}} M[A/X]
(π_{i}) π_{i}⟨M_{1}, M_{2}⟩ ⟶^{π_{i}} M_{i}, for i = 1, 2
(δ) M ⟶^{δ} ⟨π_{1}(M), π_{2}(M)⟩, if \{ \begin{matrix}M : A × B \\ M is not a pair \end{matrix}

(η) M ⟶^{η} λx : A.Mx, if \{ \begin{matrix}x ∉ F V (M) \\ M : A → C \\ M is not a λ − abstraction \end{matrix}

(η^{2}) M ⟶^{η^{2}} ΛX.M[X], if \{ \begin{matrix}X is not free in M \\ X is not free in the type of any free variable of M \\ M : ∀Y.A \\ M is not a Λ − abstraction \end{matrix}

The one-step reduction relation between terms, denoted ⟹ , is defined as the closure of the reduction rules β, β^{2}, η, η^{2}, π_{1}, π_{2}, δ for all the contexts except in the application and projection cases, i.e:

– If M ⟹ M′, then MN ⟹ M′N except in the case M ⟶^{η} M′

– If M ⟹ M′, then M[A] ⟹ M′[A] except in the case M ⟶^{η^{2}} M′

– If M ⟹ M′, then π_{i}(M) ⟹ π_{i}(M′) except in the case M ⟶^{δ} M′

Notation 3 The transitive and the reflexive transitive closure of ⟹ are noted ⟹+ and ⟹∗ respectively.

We will use some standard notions from the theory of rewriting system, such as redex, normal form, confluence, weak confluence and strong normalization. See [Bar84] for references.

3 Weak Confluence

Since we already know that the first order fragment of the calculus is confluent [Aka93, DCK94b, JG92, Dou93, Cub92], this task is greatly simplified: we are left to examine only the critical pairs that arise from the use of the second order rules β^{2} and η^{2}.

We first prove a substitution lemma for types:

Lemma 4. If Q ⟹ Q′, then Q[A/X] ⟹ Q′[A/X]

Proof. By a simple case analysis.

Then, we can proceed to prove the following

Lemma 5 Critical Pairs. If M ⟶ M_{1} and M ⟹ M_{2}, there is M_{3} such that M_{1} ⟹∗ M_{3} and M_{2} ⟹∗ M_{3}.

Proof. We analyse only the cases where M ⟶ M_{1} is an ⟶^{η^{2}} or ⟹^{β^{2}} , all the other cases can be found in [DCK94b].

1.

(ΛX.Q)[A] = = = = =\begin{matrix}= \\ = \\ = \\ = \\ ⇒ \end{matrix} (ΛX.Q′)[A]

β^{2}∨  β^{2}∨

Q[A/X] = = = = = = by lemma 4 \begin{matrix}= \\ = \\ = \\ = \\ = \\ ⇒ \end{matrix} Q′[A/X]

2.

(ΛX.Q)[A] \overline{η} \overline{>} λy : B.((ΛX.Q)[A])y

β^{2}∨  β^{2}∨

Q[A/X]  λy : B.(Q[A/X])y

If Q[A/X] is not a λ-abstraction, then Q[A/X] ⟶^{η} λy : B.(Q[A/X])y, otherwise Q[A/X] = λz.N and we have

λy : B.(λz.N)y ⟶^{β} λy : B.(N[y/z]) =_{α} λz.N = Q[A/X]

3.

(ΛX.Q)[A] \overline{δ} \overline{>} ⟨π_{1}((ΛX.Q)[A]), π_{2}((ΛX.Q)[A])⟩

β^{2}∨  β^{2}∨

⟨π_{1}(Q[A/X]), π_{2}((ΛX.Q)[A])⟩

β^{2}∨

Q[A/X]  ⟨π_{1}(Q[A/X]), π_{2}(Q[A/X])⟩

If Q[A/X] is not a pair, then Q[A/X] ⟶^{δ} ⟨π_{1}(Q[A/X]), π_{2}(Q[A/X])⟩, otherwise Q[A/X] = ⟨N_{1}, N_{2}⟩ and we have

⟨π_{1}(⟨N_{1}, N_{2}⟩), π_{2}(⟨N_{1}, N_{2}⟩)⟩ ⟶^{π_{1}} ⟨N_{1}, π_{2}(⟨N_{1}, N_{2}⟩)⟩ ⟶^{π_{2}} ⟨N_{1}, N_{2}⟩ = Q[A/X]

(ΛX.Q)[A] \overline{η^{2}}\overline{>} ΛY.((ΛX.Q)[A])[Y]

β^{2}∨  β^{2}∨

Q[A/X]  ΛY.(Q[A/X])[Y]

If Q[A/X] is not a Λ-abstraction, then Q[A/X] ⟶^{η^{2}} ΛY.(Q[A/X])[Y], otherwise Q[A/X] = ΛZ.N and we have

ΛY.(ΛZ.N)y ⟶^{β^{2}} ΛY.(N[Y/Z]) =_{α} ΛZ.N = Q[A/X]

5.

Q = = = =\begin{matrix}= \\ = \\ = \\ ⇒ \end{matrix} Q′

η^{2}∨  η^{2}∨

ΛY.Q[Y] = ⇒ ΛY.Q[Y]

This is because if Q ⟹ Q′ is an internal reduction, it is not a root expansion and then Q[Y] ⟹ Q′[Y] which implies also ΛY.Q[Y] ⟹ ΛY.Q′[Y]

6.

(λy.M)N  \overline{β} \overline{>} M[N/y]

η^{2}∨

ΛY.((λy.M)N)[Y]

If M[N/y] is not a Λ-abstraction, then M[N/y] ⟶^{η^{2}} ΛY.(M[N/y])[Y], otherwise M[N/y] = ΛZ.L and we have:

ΛY.(ΛZ.L)[Y] ⟶^{β^{2}} ΛY.L[Y/Z] =_{α} ΛZ.L = M[N/y]

Finally, the proof of the weak confluence for the calculus proceeds exactly as in Theorem 4.11 of [DCK94b].

4 Strong normalization

In this section we prove strong normalization for the full system by means of a notion of reducibility modified as in [JG92].

4.1 Definitions

Definition 6 (neutral terms) A term t:U is neutral if it is not a λ-abstraction, a type abstraction or a pair.

Definition 7 (longest reduction path for a term, or rank) Let u be a term, then ν(u) denotes the length of the longest reduction path starting from u. Notice that, by König’s Lemma, if u is strongly normalisable then ν(u) is finite.

Definition 8 A reducibility candidate of type U is a set R of terms of type U with the following properties.

CR1 if t ∈ R, then t is strongly normalisable. CR2 if t ∈ R and t ⟶ t’, then t’ ∈ R. CR3 if t is neutral and for all t’ s.t. t ⟶ t’ other than a basic expansion we

have that t’ ∈ R, then t ∈ R.

The modification written in bold in CR3 was first suggested in [Jay92] to adapt Girard’s reducibility proof for the simply typed λ-calculus with expansion rules.

To discuss its implications, let us recall here the steps that one follows in a traditional reducibility proof for second order calculi. First, one defines the notion of reducibility candidate, remarks that the set of stronlgy normalizing terms is a reducibility candidate, defines the notion of product and function space for reducibility candidates, and shows that the product and function spaces of any given reducibility candidate is still a reducibility candidate. Then one defines a notion of reducible candidate with parameters RED [\overrightarrow{R}/\overrightarrow{X}]for all types T and one shows by induction on the types that all reducible candidate with parameters is a reducible candidate. Finally, using a bunch of technical lemmas, one shows by structural induction on the terms that every instance of a term t (and in particular t itself) is reducible, hence strongly normalizable.

In the presence of expansions, we have to alter the order of several lemmas, and it is not evident that the set of strongly normalizing terms form a reducibility candidate in general, while this is trivial with Girard’s formulation of CR3.

Fortunately, it will be enough to show that the set of strongly normalizing terms of base or variable types only are a reducibility candidate.

Proposition 9. The set of strongly normalizable terms of basic type or variable type are a reducibility candidate.

Proof. Just notice that on terms of basic type or variable type the modified (CR3) condition is equal to Girard’s original (CR3) condition, because no root expansion is possible, so the proof goes through as in the usual case without expansions.

Remark. A reducibility candidate R, if it exists, is never empty as CR3 implies that it always contains the variables of type U, because they are neutral and there is no reduction other than basic expansions leaving them.

Lemma 10 normalization lemma.

(i) If t : A × B is a term such that p_{1}t : A and p_{2}t are s. n. then so is t. (ii) If t : A → B is a term and x : A is a variable not free in t such that tx : B

is s. n. then t is s. n.. (iii) If t : ∀Y.A is a term and X is a type variable not free in t such that t[X] :

A[X/Y] is s. n. then t is s. n.. (iv) If t : A is a s. n. term, then λx.t and ΛX.t are s. n. too.

Proof. By induction on the maximal reduction lengths of the strongly normalizing terms.

If R and S are reducibility candidates of types U and V, we can define the following sets:

t ∈ R × S⟺ π_{1}(t) ∈ U and π_{2}(t) ∈ V t ∈ R → S⟺ for all u ∈ R, tu ∈ S

Lemma 11 Pairing. Let R_{1} and R_{2} be reducibility candidates of types A_{1} and A_{2} and let u : A_{1} ∈ R_{1} and v : A_{2} ∈ R_{2} . Then p_{i}⟨u, v⟩ : A_{i} ∈ R_{i}.

Proof. By induction on the normalization lengths of u and v, using (CR3), as usual.

Theorem 12. If R_{1} and R_{2} are reducibility candidates of types U_{1} and U_{2}, then R_{1} × R_{2} is a reducibility candidate of type U_{1} × U_{2}.

Proof. The proof is still done by induction on the type. It is rather different from the usual one, so we show it in full in the Appendix.

4.2 Reducibility with parameters

Let T be a type, and \overrightarrow{X} be a set of type variables that contains at least all the free type variables of T. For \overrightarrow{U} a sequence of types of the same length, let T[\overrightarrow{U}/\overrightarrow{X}] be the type obtained by simultaneous substitution of the X’s with the

U’s, and \overrightarrow{R} a sequence of reducibility candidates of corresponding types.

Definition 13 The set RED_{T} [\overrightarrow{R}/\overrightarrow{X}] of reducible terms of type T is defined by

induction on the type T as follows (where the \overrightarrow{R} are reducibility candidates of

type \overrightarrow{U}).

– if T is atomic, RED_{T} [\overrightarrow{R}/\overrightarrow{X}] is the set of s. n. terms of type T

– if T is X_{i}, RED_{T} [\overrightarrow{R}/\overrightarrow{X}] is R_{i}

– if T is U × V then RED_{T} [\overrightarrow{R}/\overrightarrow{X}] is RED_{U}[\overrightarrow{R}/\overrightarrow{X}] × RED_{V} [\overrightarrow{R}/\overrightarrow{X}]

– if T is U → V then RED_{T} [\overrightarrow{R}/\overrightarrow{X}] is RED_{U}[\overrightarrow{R}/\overrightarrow{X}] → RED_{V} [\overrightarrow{R}/\overrightarrow{X}] – if T is ∀Y.W then RED_{T} [\overrightarrow{R}/\overrightarrow{X}] is the set of terms t of type T[\overrightarrow{U}/\overrightarrow{X}]

such that, for every type V and reducibility candidate S of this type, t[V] ∈ RED_{W} [\overrightarrow{R}/\overrightarrow{U}, S/Y]

Lemma 14 Universal abstraction. If for every type V and candidate S, RED_{W} [\overrightarrow{R}/\overrightarrow{X}, S/Y] is a reducibility candidate and v[V/Y] ∈ RED_{W} [\overrightarrow{R}/\overrightarrow{X}, S/Y], then ΛY.v ∈ RED_{∀Y.W} [\overrightarrow{R}/\overrightarrow{X}]

Proof. We need to show that (ΛY.v)[V] ∈ RED_{W} [\overrightarrow{R}/\overrightarrow{X}, S/Y] for every type V and candidate S of type V. We can argue by induction on ν(v), because v is strongly normalizable as v = v[Y/Y] is in RED_{W} [\overrightarrow{R}/\overrightarrow{X}, SN_{Y} /Y], which is a reducibility candidate by hypothesis. Since (ΛY.v)[V] is neutral, we will use CR3 for RED_{W} [\overrightarrow{R}/\overrightarrow{X}, S/Y].

Converting a redex of (ΛY.v)[V] without using basic expansions can yield:

– v[V/Y], which is in RED_{W} [\overrightarrow{R}/\overrightarrow{X}, S/Y] by hypothesis

– (ΛY.v’)[V] with v’ one step from v; now, v[V/Y] reduces to v’[V/Y]^{3}, so we can apply induction on ν(v) and get (ΛY.v’)[V] ∈ RED_{W} [\overrightarrow{R}/\overrightarrow{X}, S/Y]

The results follows then by CR3 for RED_{W} [\overrightarrow{R}/\overrightarrow{X}].

In the following lemma we will talk about subtypes of a given type, where the subtypes of A → B are given by A → B itself together with the subtypes of A and B, and similarly for A × B, while the subtypes of ∀X.A are given by ∀X.A itself together with the subtypes of A. This notion also provide a natural order over types.

Lemma 15 Abstraction. Let x:U and v:V, and suppose that RED_{W} [\overrightarrow{R}/\overrightarrow{X}] is a reducibility candidate for all W subtypes of U or V (inclusive). If for all u ∈ RED_{U}[\overrightarrow{R}/\overrightarrow{X}] we have v[u/x] ∈ RED_{V} [\overrightarrow{R}/\overrightarrow{X}], then λx.v ∈ RED_{U→V} [\overrightarrow{R}/\overrightarrow{X}]

Proof. Assume the property is true for all types strictly smaller than U → V.

To show that λx.v ∈ RED_{U→V} [\overrightarrow{R}/\overrightarrow{X}], we need to show that (λx.v)u ∈ RED_{V} [\overrightarrow{R}/\overrightarrow{X}] for all u ∈ RED_{U}[\overrightarrow{R}/\overrightarrow{X}], and we will do so by using CR3 for RED_{V} [\overrightarrow{R}/\overrightarrow{X}].

We know that x:U is in RED_{U}[\overrightarrow{R}/\overrightarrow{X}] (remark 4.1).

3 Since type substitution does not alter the structure of a term, we can perform on v[V/Y] all the reductions we could perform on v, or maybe more as new expansion redexes can arise, but surely not less.

So v = v[x/x] is in RED_{V} [\overrightarrow{R}/\overrightarrow{X}], hence strongly normalizable by CR1 and we can argue by induction on ν(u) + ν(v) to show that all terms one step from (λx.v) u are reducible.

The term (λx.v) u converts to

– v[u/x] that is in RED_{V} [\overrightarrow{R}/\overrightarrow{X}] by hypothesis.

– (λx.v’) u with v’ one step from v. To apply the induction hypothesis using

the fact that ν(v′) < ν(v), and get (λx.v’) u ∈ RED_{V} [\overrightarrow{R}/\overrightarrow{X}], we need to

show now that v’[u/x] is in RED_{V} [\overrightarrow{R}/\overrightarrow{X}]. If v’[u/x] is one step from v[u/x],

then this comes from CR2 for RED_{V} [\overrightarrow{R}/\overrightarrow{X}].

If v’[u/x] is not one step from v[u/x], then v’ is obtained from v by an expansion of an occurrence of x and u is either a pair, a λ-abstraction or a type abstraction. Notice now that if u is a pair, ⟨p_{1}u, p_{2}u⟩ is reducible by Lemma 11; if u is an abstraction of type U = C → D then by definition of u ∈ RED_{U}[\overrightarrow{R}/\overrightarrow{X}], ut ∈ RED_{D}[\overrightarrow{R}/\overrightarrow{X}] for all t ∈ RED_{C}[\overrightarrow{R}/\overrightarrow{X}], and by

induction hypothesis on the type we have that λy.uy ∈ RED_{C→D}[\overrightarrow{R}/\overrightarrow{X}]; finally, if u is a type abstraction of type U = ∀X.W, then by definition of u ∈ RED_{U}[\overrightarrow{R}/\overrightarrow{X}], for every type V and reducibility candidate S of this type,

u[X][V/X] = u[V] ∈ RED_{W} [\overrightarrow{R}/\overrightarrow{U}, S/Y], which is a reducibiblity candidate

by hypothesis, so we have that ΛX.u[X] ∈ RED_{∀X.D}[\overrightarrow{R}/\overrightarrow{X}] by lemma 14. Let us now use η(u) for either ⟨p_{1}u, p_{2}u⟩ with u a pair or λy.uy with u a λabstraction or ΛX.u[X] with u a type abstraction. What we have just shown

means that by hypothesis v[η(u)/x] ∈ RED_{V} [\overrightarrow{R}/\overrightarrow{X}], but it is straightforward to see that η(u)→→u, so we can build a reduction sequence v[η(u)/x]→→v′[u/x],

and then use repeatedly CR2 for RED_{V} [\overrightarrow{R}/\overrightarrow{X}] to deduce v’[u/x] ∈ RED_{V} [\overrightarrow{R}/\overrightarrow{X}], as neeeded.

– (λx.v)u’ with u’ one step from u. Then u’ ∈ RED_{U}[\overrightarrow{R}/\overrightarrow{X}] by CR2, ν(u′) <

ν(u) and v[u’/x] ∈ RED_{V} [\overrightarrow{R}/\overrightarrow{X}] by repeated applications of CR2, as it is some steps from v[u/x]. So we can apply again the induction hypothesis.

Since (λx.v)u is neutral and it converts to terms in RED_{V} [\overrightarrow{R}/\overrightarrow{X}] only, it is

in RED_{V} [\overrightarrow{R}/\overrightarrow{X}] too. Hence λx.v is in RED_{U→V} [\overrightarrow{R}/\overrightarrow{X}] by definition.

Theorem 16. RED_{T} [\overrightarrow{R}/\overrightarrow{X}] is a reducibility candidate of type T[\overrightarrow{U}/\overrightarrow{X}]

Proof. We proceed by structural induction on the type T. We show only the cases for the arrow and universal types, which are the ones that change with expansions.

Arrow types Let T be U_{1} → U_{2}. We know by induction hypothesis that RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}], RED_{U_{2}}[\overrightarrow{R}/\overrightarrow{X}] and in fact all RED_{W} [\overrightarrow{R}/\overrightarrow{X}] for W subtype of the U_{i}, are reducibility candidates, and we will now show that RED_{U_{1}→U_{2}}[\overrightarrow{R}/\overrightarrow{X}] = RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}] → RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}] is a reducibility candidate.

– (CR1) if t ∈ RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}] → RED_{U_{2}}[\overrightarrow{R}/\overrightarrow{X}], then let x be a variable of type U_{1}. Since x ∈ any reducibility candidate of type U_{1}, (remark 4.1), in

particular x ∈ RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}] and we get that (tx) ∈ RED_{U_{2}}[\overrightarrow{R}/\overrightarrow{X}] by

definition, hence (tx) is strongly normalisable by CR1 for RED_{U_{2}}[\overrightarrow{R}/\overrightarrow{X}], which is a reducibility candidate by induction hypothesis. This suffices to show that t is strongly normalisable, by Lemma 10.

– (CR2) if t ⟶ t’, we need to show (t’u) ∈ RED_{U_{2}}[\overrightarrow{R}/\overrightarrow{X}] for all u ∈

RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}]. Take then u ∈ RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}]; we have (tu) ∈ RED_{U_{2}}[\overrightarrow{R}/\overrightarrow{X}]

by definition of reducibility candidate. If (tu) ⟶ (t’u), then (t’u) ∈ RED_{U_{2}}[\overrightarrow{R}/\overrightarrow{X}]

by CR2 for RED_{U_{2}}[\overrightarrow{R}/\overrightarrow{X}], which is a reducibility candidate by induction hypothesis. Otherwise, t ⟶ λx : U_{1}.tx, but tu = (tx)[u/x] is in

RED_{U_{2}}[\overrightarrow{R}/\overrightarrow{X}] for any u ∈ RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}] by induction hypothesis, so we can conclude by applying lemma 15.

– (CR3) t is neutral and all t’ one step from t other than basic expansions are in

RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}] → RED_{U_{2}}[\overrightarrow{R}/\overrightarrow{X}]. In order to show t ∈ RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}] →

RED_{U_{2}}[\overrightarrow{R}/\overrightarrow{X}], we need to show (tu) ∈ RED_{U_{2}}[\overrightarrow{R}/\overrightarrow{X}] for all u ∈ RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}].

By induction hypothesis on RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}], we get u is strongly normalisable, so we can argue by induction on ν(u). In one step, and without performing basic expansions, (tu) converts to:

• (t’u) with t’ one step from t.

As t’ ∈ RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}] → RED_{U_{2}}[\overrightarrow{R}/\overrightarrow{X}], we get (t’u) ∈ RED_{U_{2}}[\overrightarrow{R}/\overrightarrow{X}] by definition.

• (tu’) with u’ one step from u.

By induction hypothesis on RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}], u’ ∈ RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}] and

ν(u′) < ν(u), so (tu’) ∈ RED_{U_{2}}[\overrightarrow{R}/\overrightarrow{X}] by the induction hypothesis on u.

Universal types Let T = ∀Y.W.

– (CR1) if t ∈ RED_{∀Y.W} [\overrightarrow{R}/\overrightarrow{X}], then let X be an arbitrary type variable and S be an arbitrary reducibility candidate of type X (for example, the strongly

normalizable terms of type X). Then t[X] ∈ RED_{W} [\overrightarrow{R}/\overrightarrow{X}, S/Y] by definition, so by induction hypothesis we know that t[X] is strongly normalizable. Then we can conclude by 10 that t is strongly normalisable.

– (CR2) let t ⟶ t’; for all types V and reducibility candidate S of this type, we have that t[V] ∈ RED_{W} [\overrightarrow{R}/\overrightarrow{X}, S/Y], so if t[V] ⟶ t’[V], then t’[V] ∈ RED_{W} [\overrightarrow{R}/\overrightarrow{X}, S/Y] by induction hypothesis on W. Otherwise t ⟶ ΛX.t[X]=t’: we know by inductive hypothesis that for all types V and reducibility candidate S of this type RED_{W} [\overrightarrow{R}/\overrightarrow{X}, S/Y] is a reducibility candidate and we know that t[Y][V/Y]=t[V] ∈ RED_{W} [\overrightarrow{R}/\overrightarrow{X}, S/Y], so we can apply lemma 14 and we get t’=ΛX.t[X] ∈ RED_{∀Y.W} [\overrightarrow{R}/\overrightarrow{X}], and finally we get t’[V] ∈ RED_{W} [\overrightarrow{R}/\overrightarrow{X}, S/Y] by definition. In any case, t’[V] ∈ RED_{W} [\overrightarrow{R}/\overrightarrow{X}], so by definition t’ ∈ RED_{∀Y.W} [\overrightarrow{R}/\overrightarrow{X}].

– (CR3) t is neutral and all t’ one step from t other than basic expansions are in RED_{T} [\overrightarrow{R}/\overrightarrow{X}]. Take V and S: if we apply a conversion other than a basic expansion to t[V], the only possible result is t′[V] (since t is neutral), and t’ cannot be a basic expansion of t (because t is applied). Now, this means that t’ is in RED_{T} [\overrightarrow{R}/\overrightarrow{X}], so by definition t′[V] is in RED_{W} [\overrightarrow{R}/\overrightarrow{X}, S/Y], and by (CR3) for W we get that t[V] is in RED_{W} [\overrightarrow{R}/\overrightarrow{X}, S/Y], so we can conclude that t ∈ RED_{T} [\overrightarrow{R}/\overrightarrow{X}].

Reducibility theorem We shall need now one more lemma to deduce reducibility of a term from reducibility of its subterms.

Lemma 17. RED_{T [V/Y]}[\overrightarrow{R}/\overrightarrow{X}] = RED_{T} [\overrightarrow{R}/\overrightarrow{X}, RED_{V} [\overrightarrow{R}/\overrightarrow{X}]/Y]

Proof. By induction on T.

Lemma 18 Universal application. If t ∈ RED_{∀Y.W} [\overrightarrow{R}/\overrightarrow{X}], then t[V] ∈ RED_{W [V/Y]}[\overrightarrow{R}/\overrightarrow{X}] for every type V.

Proof. By hypothesis, t[V] ∈ RED_{W} [\overrightarrow{R}/\overrightarrow{X}, S/Y] for every candidate S of type V. Taking S = RED_{V} [\overrightarrow{R}/\overrightarrow{X}], the result follows by Lemma 17.

The theorem As in [GLT90], we say here that a term t of type T is reducible if it is in RED_{T} [\overrightarrow{SN}/\overrightarrow{X}], where \overrightarrow{X} are the free type variables of T and SN_{i} is the set of strongly normalizable terms of type X_{i}. In the proof of the theorem, there is the need of a stronger induction hypothesis, from which the strong normalization follows by putting u_{i} = x_{i} and R_{i} = SN_{i}.

Proposition 19. Let t:T be any term, whose free variables are contained in x_{1} : U_{1}, …, x_{n} : U_{n}, and all the free variable of T, U_{1}, … U_{n} are among X_{1}, … X_{m}. If R_{1}, … R_{m} are reducibility candidates of types V_{1}, … V_{m}, and u_{1}, … u_{m} are terms of types U_{1}[\overrightarrow{V}/\overrightarrow{X}], … U_{m}[\overrightarrow{V}/\overrightarrow{X}]which are in RED_{U_{1}}[\overrightarrow{R}/\overrightarrow{X}],

… RED_{U_{n}}[\overrightarrow{R}/\overrightarrow{X}], then t[\overrightarrow{V}/\overrightarrow{X}][\overrightarrow{u}/\overrightarrow{x}] ∈ RED_{T} [\overrightarrow{R}/\overrightarrow{X}].

Proof. By induction on t as usual.

Theorem 20. ⟶^{β^{2}η^{2}π∗} is strongly normalizing.

Proof. Let t be any term, and U be its type. All its free variables are in any reducibility candidate by remark 4.1, so that t = t[\overrightarrow{X}/\overrightarrow{X}][x_{1}/x_{1}, …, x_{n}/x_{n}] ∈

RED_{U[\overrightarrow{X}/\overrightarrow{X}]}[\overrightarrow{SN}/\overrightarrow{X}] by the previous lemma. Then it is strongly normalizing

by CR1.

5 Adding the Top type modularly

It is possible to extend the previous reducibility proof to take into account also the special unit type T and the Top rule M : T ⟶ ∗ : T that one needs for various systems (see [CDC91], for a discussion of the motivation for the Top rule), but that would not be a wise approach to this rule: indeed, its great simplicity will allow to add it modularly to a given canonical system, without any need to go again through a long proof involving the rest of the calculus.

Without going into much formal details, we want to give here a very simple argument of general applicability that shows how Top preserves strong normalization, and hence also confluence under some additional assumptions.

Proposition 21 Preservation of Strong Normalization with Top. Given a strongly normalizing left-linear reduction relation R, generated by rules that do not contain the special term ∗ in their left hand side, then R + T op is still strongly normalizing.

Proof. The argument of the proof is indeed very simple: take any infinite reduction Π in R + T op, and notice that (since Top alone is clearly strongly normalizing) this reduction must contain infinite R steps. Now, one can easily build an infinite reduction in R alone by using the infinite number of R steps from the Π reduction: it suffices to remark that any Top reduction step followed by an R reduction step in Π C[M] ⟶^{T op} C[∗] ⟶^{R} M′ can be postponed as in C[M] ⟶^{R} M′′ ⟶^{T op}∗ M′, as the rules on R are left-linear and do not transform ∗ (basically, rules in R can only pass ∗ around untouched, or delete it).

Clearly, if R is also confluent, and Top does not break local confluence, then, as an easy corollary of Newman’s Lemma, R + T op is also confluent.

It is then quite immediate to derive the following

Corollary 22. The second order lambda calculus with expansive rules for products, arrow and universal types, and the Top rule is strongly normalizing and confluent.

Notice that the Top rule, whose l.h.s. is just a metavariable, does not fit into the general scheme of [JO91]: it would be interesting to see if the simple argument presented here allow to modify that scheme in order to take even Top into account.

6 Conclusions and future work

We explained why expansion rules and the second order β rule cannot be handled separately in a modular way and we showed how to handle them together by a careful restructuration of the usual reducibility candidate method. This work suggests that the expansionary approach to extensional rules is viable even in a second order context, and is a firm step towards a redesign of the extensional rules in more complex systems like Fω or the Calculus of Constructions. Expansion rules behave better than contractions in the presence of additional axioms (like the one for unit or for a fixpoint combinator) and give a natural characterization of the notion of η-long normal forms.

Finally, we would like to suggest that the use of expansion rules for extensional equalities is very promising in order to improve the modularity results on the combination of the lambda calculus with first or higher order algebraic rewriting systems (presented for example in [BTM86, BT88, BTG94] and [JO91]): these works use the traditional contractive interpretation of η, and cannot handle higher order rewrite rules like the one given above for the unit type, while such rule is not problematic at all in the presence of expansion rules.

Acknowledgements

We are endebted to Neil Ghani for the fundamental remark that we only need the set of strongly normalizing terms of basic types for the proof to go through.

References

[Aka93] Yohji Akama. On Mints’ reductions for ccc-Calculus. In Typed Lambda Calculus and Applications, number 664 in LNCS, pages 1–12. Springer Verlag, 1993.

[Bar84] Henk Barendregt. The Lambda Calculus; Its syntax and Semantics (revised edition). North Holland, 1984.

[BT88] Val Breazu-Tannen. Combining algebra and higher-order types. In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 82–90, Edinburgh, Scotland, July 5–8 1988. IEEE Computer Society.

[BTG94] Val Breazu-Tannen and Jean Gallier. Polymorphic rewiting preserves algebraic confluence. Information and Computation, 1994.

[BTM86] Val Breazu-Tannen and Albert R. Meyer. Polymorphism is conservative over simple types (preliminary report). In Proceedings, Symposium on Logic in Computer Science, pages 7–17, Cambridge, Massachusetts, June 16–18 1986. IEEE Computer Society.

[CDC91] Pierre-Louis Curien and Roberto Di Cosmo. A confluent reduction system for the λ-calculus with surjective pairing and terminal object. In Leach, Monien, and Artalejo, editors, Intern. Conf. on Automata, Languages and Programming (ICALP), volume 510 of Lecture Notes in Computer Science, pages 291–302. Springer-Verlag, July 1991.

[Cub92] Djordje Cubric. On free CCC. Distributed on the types mailing list, 1992.

[DCK94a] Roberto Di Cosmo and Delia Kesner. Combining first order algebraic rewriting systems, recursion and extensional lambda calculi. In Serge Abiteboul and Eli Shamir, editors, Intern. Conf. on Automata, Languages and Programming (ICALP), volume 820 of Lecture Notes in Computer Science, pages 462–472. Springer-Verlag, July 1994.

[DCK94b] Roberto Di Cosmo and Delia Kesner. Simulating expansions without expansions. Mathematical Structures in Computer Science, 4:1–48, 1994. A preliminary version is available as Technical Report LIENS-93-11/INRIA 1911.

[DCP95] Roberto Di Cosmo and Adolfo Piperno. Expanding extensional polymorphism. In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, Typed Lambda Calculus and Applications, volume 902 of Lecture Notes in Computer Science, pages 139–153, April 1995.

[Dou93] Daniel J. Dougherty. Some lambda calculi with categorical sums and products. In Proc. of the Fifth International Conference on Rewriting Techniques and Applications (RTA), 1993.

[Ges90] Alfons Geser. Relative termination. Dissertation, Fakultät für Mathematik und Informatik, Universität Passau, Germany, 1990. Also available as: Report 91-03, Ulmer Informatik-Berichte, Universität Ulm, 1991.

[Geu92] Herman Geuvers. The church-rosser property for βη-reduction in typed λcalculi. In 7thProceedings of the Symposium on Logic in Computer Science (LICS), pages 453–460, 1992.

[Gha95] Neil Ghani. Extensionality and polymorphism. University of Edimburgh, Submitted, 1995.

[GLT90] Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge University Press, 1990.

[Jay92] Colin Barry Jay. Long βη normal forms and confluence (revised). Technical Report 44, LFCS - University of Edinburgh, August 1992.

[JG92] Colin Barry Jay and Neil Ghani. The Virtues of Eta-expansion. Technical Report ECS-LFCS-92-243, LFCS, 1992. University of Edimburgh, preliminary version of [?].

[JO91] Jean-Pierre Jouannaud and Mitsuhiro Okada. A computation model for executable higher-order algebraic specification languages. In Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, pages 350–361, Amsterdam, The Netherlands, July 15–18 1991. IEEE Computer Society Press.

[Klo80] Jan Willem Klop. Combinatory reduction systems. Mathematical Center Tracts, 27, 1980.

[Nip90] Tobias Nipkow. A critical pair lemma for higher-order rewrite systems and its application to λ^{∗}. First Annual Workshop on Logical Frameworks, 1990.

A Strong normalization

Theorem 12 If R_{1} and R_{2} are reducibility candidates of types U_{1} and U_{2}, then R_{1} × R_{2} is a reducibility candidate of type U_{1} × U_{2}.

Proof. Assume that R_{1} and R_{2} are reducibility candidates of type U_{1} and U_{2}, respectively.

– (CR1) if t ∈ R_{1} × R_{2}, then π_{i}(t) is strongly normalisable by the hypothesis on R_{i}, since π_{i}(t) ∈ R_{i} by definition. Hence t is strongly normalisable by Lemma 10.

– (CR2) if t ⟶ t’ not via a basic expansion, then π_{1}(t) ⟶ π_{1}(t′) and π_{2}(t) ⟶ π_{2}(t′). As t ∈ R_{1} × R_{2}, then π_{1}(t) ∈ R_{1} and π_{2}(t) ∈ R_{2}. By hypothesis CR2 for R_{1} and R_{2} we get π_{1}(t′) ∈ R_{1} and π_{2}(t′) ∈ R_{2}, hence, by definition, t’ ∈ R_{1} × R_{2}. In the case t⟶⟨p_{1}t, p_{2}t⟩, we must prove that p_{i}⟨p_{1}(t), p_{2}(t)⟩ ∈ R_{i}. By definition of R_{1} × R_{2}, p_{1}t is in R_{1} and p_{2}t is in R_{2}, so we can apply Lemma 11.

– (CR3) t is neutral and every t’ one step from t other than basic expansions are in R_{1} × R_{2}. We need to show π_{1}(t) ∈ R_{1} and π_{2}(t) ∈ R_{2}. Now notice that applying a one step reduction to π_{i}(t) which is not a basic expansion can only result in some π_{i}(t′) as t is neutral. Furthermore, this t’ is not a basic expansion of t because it is in an influential position. So, t’ is in R_{1} × R_{2}, and then by definition π_{1}(t′) ∈ R_{1} and π_{2}(t′) ∈ R_{2}. Since the π_{i}(t) are neutral and every term one step from them other than basic expansions is in R_{i}, the hypothesis for R_{1} and R_{2} ensure π_{1}(t) ∈ R_{1} and π_{2}(t) ∈ R_{2}. So t ∈ R_{1} × R_{2} by definition.

This article was processed using the LaTEX macro package with LLNCS style