Combining first order algebraic rewriting systems, recursion and extensional lambda calculi

Roberto Di Cosmo^{∗}  Delia Kesner ^{§}

Abstract

It is well known that confluence and strong normalization are preserved when combining left-linear algebraic rewriting systems with the simply typed lambda calculus. It is equally well known that confluence fails when adding either the usual extensional rule for η, or recursion together with the usual contraction rule for surjective pairing.

We show that confluence and normalization are modular properties for the combination of left-linear algebraic rewriting systems with typed lambda calculi enriched with expansive extensional rules for η and surjective pairing. For that, we use a translation technique allowing to simulate expansions without expansion rules. We also show that confluence is maintained in a modular way when adding fixpoints. This result is also obtained by a simple translation technique allowing to simulate bounded recursion with β reduction.

1 Introduction

Confluence and strong normalization for the combination of lambda calculus and algebraic rewriting systems have been the object of many researches [BT88, JO91, BTG94, HM90], where the modularity of these properties is studied. However, the lambda calculus under consideration cannot be equipped with extensional rules (notably η) since confluence immediately fails as the following example shows:

Example 1.1 Take a single algebraic rule fx⟶^{alg}a where f and a are algebraic symbols. Then the following diagram cannot be closed:

f⟵^{η}λx.fx⟶^{alg}λx.a

On the other side, there is some recent increasing interest on a different computational interpretation of the extensional axioms, which are turned into conditional expansion rules instead of contractions (see [Aka93, Dou93, DCK94b, Cub92, JG92]). For example, the η equality is turned into the rule

M⟶^{η}λx.Mx if M : A → B, M is not a λ-abstraction and M is not applied

With this expansionary interpretation the previous counterexample simply goes away as it becomes f⟶λx.fx⟶λx.a. It is then quite legitimate to ask if it is possible to recover the confluence property when combining confluent algebraic rewriting systems with the typed lambda calculus and expansive extensional rules, and moreover to ask whether this property can be derived in a modular way. Notice that these conditional expansion rules do not fit even into the very general framework of [JO91], where higher-order variables are not allowed as left-hand sides of rules. It is to be noticed that, if we just want to get rid of the specific counterexample above, without using expansion rules, there is also the possibility to state that an algebraic term f alone is not a well formed term if it has not a base type. While this approach can also lead to a confluent system, as shown by [?], it is important to consider that the expansional reading of extensional rules was not born just for handling the counterexample above, but to solve many different problems (like the ones posed by the combination with the terminal type, or the fixpoint operators): all work done using η as a contraction will inevitably be confronted with the same unsormontable difficulties as soon as

∗DMI-LIENS (CNRS URA 1347) Ecole Normale Supérieure - 45, Rue d’Ulm - 75230 Paris France

E-mail:dicosmo@ens.fr

§CNRS and LRI - Bât 490, Université de Paris-Sud - 91405 Orsay Cedex, France

E-mail:kesner@lri.fr

Another natural question also arises when taking into consideration fixpoint operators: whenever we want to show confluence in the presence of fixpoints, we usually resort to the very same technique of labeled reductions originated from Lévy’s work on the untyped lambda-calculus [Lév76], that is really not modular. Furthermore, it has already been shown that fixpoint are compatible with expansion rules for surjective pairing [DCK94b, Dou93], while recursion together with the (SP)-axiom oriented as a contraction rule cause confluence to fail [Nes89]. It is quite reasonable to ask again for a more friendly proof technique based on modular properties, possibly capable of handling conditional expansion rules.

In this paper we answer positively to these questions: confluence and normalization are modular properties when combining left-linear algebraic rewriting systems with typed lambda calculi featuring extensional rules, and confluence can be modularly derived when adding fixpoints, even in the presence of conditional expansion rules. We adapt the simulation technique developed in [DCK94b] for an extensional typed lambda calculus with expansion rules, in such a way that confluence and strong normalization in presence of extensionality are both reduced to the already known confluence and strong normalization properties of the system without extensionality.

For the fixpoint combinators we adopt also a similar technique: the confluence property of any left-linear reduction system with fixpoints is reduced to the confluence of the system without fixpoints. We also show how to extend this result to the expansive interpretation of extensional rules: they do not fit into the general definition of a left-linear reduction system because they are conditional rules, and must be handled separately.

The paper is logically divided into two main sections: we first show how the combination of leftlinear algebraic rewriting systems with the typed lambda-calculus preserves strong normalization and confluence even with expansion rules for η and surjective pairing, then we present a general technique for handling fixpoint combinators, even in the presence of expansion rules. These two results will give us the full picture: left-linear algebraic rewriting systems and fixpoint combinators can be added preserving confluence to the extensional simply typed lambda calculus, while fixpoint can be added preserving confluence to any left-linear reduction system containing β-reduction and possibly expansion rules.

These results provide a simple, clean and powerful way of incorporating extensionality into a higher order language with algebraic data types, and have clearly immediate application in the field of automated theorem proving, by providing a simple way of deciding extensional equality that does not rely on ad-hoc normalization strategies as it is done in previous works.

2 Basic definitions

We first recall the standard definitions concerned with algebraic rewriting systems and extensional typed lambda calculus with pairs. We also fix the notations for the different reduction relations.

Definition 2.1 (Signature) A signature Σ = ⟨T , F, D⟩ consists of • A set T of base types.

• A set F of function symbols

• A set D of declarations of the form f : α_{1} → … → α_{n} → α, where f ∈ F, α_{1}, …, α_{n}, α ∈ T and n ≥ 0. We say that n is the arity of f.

We assume the sets F and T to be disjoint and we require every functional symbol in F to have exactly one declaration in D. From now on, we suppose the signature Σ to be fixed.

Given a signature Σ, we define the set of types of our calculus by the following grammar:

A ::= ξ | A × A | A → A

where ξ ranges over the set of base types. Variables and constants are typed by the following axioms:

x_{1} : A_{1}, …, x_{n} : A_{n} ⊢ x_{i} : A_{i} (1 ≤ i ≤ n)
x_{1} : A_{1}, …, x_{n} : A_{n} ⊢ f : A if f : A is in the signature

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}}

Definition 2.2 (Algebraic Term) A term is algebraic if it is either a variable of base type or has the form f T_{1} … T_{n}, where f ∈ F has arity n, and every T_{i} is an algebraic term. Note that an algebraic term is always of base type according to our definition.

Definition 2.3 (Algebraic rewriting system) An algebraic rewriting rule is an ordered pair (L, R) of algebraic terms such that L is not a variable, and every variable of R appears also in L. An algebraic rewriting system R is a finite set {(L_{i}, R_{i})}_{i=1}^{n} of algebraic rewriting rules.

Definition 2.4 (Left-linear rewriting system) A rewriting system is left linear if no variable occurs in the left-hand side of the same rule more then once.

We note F V (M) the set of free variables of the term M. We write [\overline{N}/\overline{x}] for the typed substitution mapping each variable x_{i} : A_{i} to a term N_{i} : A_{i} and M[\overline{N}/\overline{x}] for the term M where each variable x_{i} free in M is replaced by N_{i}.

Definition 2.5 (Algebraic reduction) The algebraic reduction between terms is a binary relation ⟶^{R} , defined in such a way that C[T] ⟶^{R} C[H] if and only if there exists a substitution θ and a rule (L, R) ∈ R such that T = θ(L) and H = θ(R).

We identify terms up to α-conversion and we consider the following set of elementary rules:

(β) (λx : A.M)N ⟶^{β} M[N/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}

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

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

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

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

We use ⟹^{B} to denote the reduction relation ⟹ without extensional rules, and ⟹^{E} to denote the relation ⟹ with only extensional rules.

Definition 2.8 We denote by ⇝ the reduction relation ⟹ ∪ ⟶^{R} , by ⇝_{B} the relation ⟹^{B} ∪ ⟶^{R} and by ⇝_{E} the relation ⟹^{E} ∪ ⟶^{R} .

We use the standard notions of substitutions, reduction, confluence, normalization, etc from the theory of rewriting systems.

3 Modularity of confluence and strong normalization

We know from [BT88, BTG94] that combining the non-extensional simply typed lambda calculus (even with pairs) with a left-linear confluent algebraic rewriting system preserves confluence. On the other hand, this combination yields a strongly normalizing system when the algebraic one is.

We use here these very same results to show that the restriction to non-extensional lambda calculus can be raised when using expansion rules.

3.1 An overview of the proof technique

To do so, we use a technique originally developed in [DCK94b] for a specific typed lambda calculus with expansion rules, that is general enough to be applied in this context. For that, we define a translation ^{∘} from our calculus into itself satisfying the following property:

• Any reduction step M⇝N can be simulated by a reduction sequence M^{∘}⇝_{B}^{+}N^{∘}

• The translation is the identity on the (η, δ)-normal forms

The first property (called simulation ) is sufficient to show that strong normalization is preserved when adding expansion rules, while both properties allow to derive the preservation of confluence.

Proposition 3.1 (Normalization via translation) Given two reduction relations R, S on a given set of terms, and a translation s.t. any reduction step ⟶^{R∪S} can be simulated by a reduction ⟶^{S}+, then if S is strongly normalizing, also R ∪ S is strongly normalizing.

Proof. Straightforward since any infinite reduction sequence of R ∪ S can be turned via simulation into an infinite reduction of S, leading to a contradiction with the hypothesis.

Proposition 3.2 (Confluence via translation) Given two reduction relations R, S on a given set of terms, and a translation ^{∘} s.t.

• Any reduction step M ⟶^{R∪S} N can be simulated by a reduction M^{∘} ⟶^{S}+N^{∘}

• The translation is the identity on the R normal-forms

then if S is confluent and R is weakly normalizing, R ∪ S is confluent.

Proof. The following picture shows how to close any diagram of R ∪ S:

P_{1}  \overline{R∗} \overline{>} \overline{P_{1}}  ≡ \overline{P_{1}}^{∘}
[figure: R ∪ S∗; S∗; S∗]
M ····· ························ M^{∘}  Q
[figure: R ∪ S∗; S∗; S∗]
P_{2}  \overline{R∗} \overline{>} \overline{P_{2}}  ≡ \overline{P_{2}}^{∘}

The dotted line pinpoints the first translation step from M to M^{∘}, while \overline{P_{i}} is any R-normal form of P_{i}.

The weak normalization property for R ensures the existence of the R normal forms \overline{P_{1}} and \overline{P_{2}}. Of course, in case S is strongly normalizing such hypothesis on R can be derived from the simulation property, and is then superfluous. The link between the outer and inner diagrams can be done by the second property since translation does not affect R normal forms. Finally, the inner diagram can be closed by the confluence property of the reduction relation S.

We exhibit now a translation with these properties from ⇝ into ⇝_{B} so that the desired modularity result can be derived from the above proposition.

3.2 Translating the extensional rules

In this section we show that confluence and strong normalization are modular properties of the combination of left-linear algebraic rewriting systems with the extensional typed lambda calculus with pairing based on expansion rules. We first define a translation of terms mapping our calculus into itself such that for every possible reduction in the original system from a term M to another term N, there is a reduction sequence from the translation of M to the translation of N, that is non empty and does not contain any expansion. We show in this way how the calculus without expansions can be used to simulate the calculus with expansions. For a detailed discussion about the following translation we refer the reader to [DCK94b].

Definition 3.3 (Translation for expansions) To every type C we associate a term, called the expansor of type C and denoted Δ_{C}, defined by induction as follows:

Δ_{A→B} = λx : A → B.λz : A.Δ_{B}(x(Δ_{A}z))
Δ_{A×B} = λx : A × B.⟨Δ_{A}(π_{1}(x)), Δ_{B}(π_{2}(x))⟩
Δ_{A}  is empty, in any other case

We then define a translation M^{∘} for a term M : A as follows^{1}:

M^{∘} = \{ \begin{matrix}M^{∘∘} & if M is a λ-abstraction or a pair \\ Δ_{A}^{k}M^{∘∘} for any k > 0 & otherwise \end{matrix}

where Δ_{A}^{k}M denotes the term \underbrace{(Δ_{A} … (Δ_{A}}_{k times} M) …) and M^{∘∘} is defined by induction as:

\begin{aligned}x^{∘∘} & = x & f^{∘∘} & = f \\ ⟨M, N⟩^{∘∘} & = ⟨M^{∘}, N^{∘}⟩ & (λx : B.M)^{∘∘} & = λx : B.M^{∘} \\ π_{i}(M)^{∘∘} & = π_{i}(M^{∘∘}) & (MN)^{∘∘} & = (M^{∘∘}N^{∘}) \end{aligned}

We can show by induction on the structure of terms that translation preserves types and leave unchanged terms when expansions are not possible.

Lemma 3.4 If Γ ⊢ M : A, then Γ ⊢ M^{∘} : A.

Proof. By induction on the structure of M; see [DCK94b] for details.

Lemma 3.5 (Translation and normal forms) If M is in (η, δ)-normal form, then M^{∘} = M.

Proof. By induction on the structure of M; see [DCK94b] for details.

The following property is essential to show that every time we perform a β-reduction on a term M in the original system, any translation of M reduces to a translation of the term we have obtained via ⟶^{β} from M. Take for example the reduction (λx : A.M)N ⟶^{β} M[N/x]. We know that ((λx : A.M)N)^{∘} = Δ_{A}^{k}((λx : A.M^{∘})N^{∘}) and we want to show that there is a non empty reduction sequence leading to M[N/x]^{∘}. Since Δ_{A}^{k}((λx : A.M^{∘})N^{∘}) ⟶^{β} Δ_{A}^{k}M^{∘}[N^{∘}/x], we have now to check that the term (M[N/x])^{∘} can be reached. We state the property as follows:

Lemma 3.6 If Γ ⊢ M : A, then ∀k ≥ 0, Δ_{A}^{k}M^{∘}[\overline{N^{∘}}/\overline{x}]⇝^{∗}_{B} (M[\overline{N}/\overline{x}])^{∘}.

Proof. Exactly as in [DCK94b], as algebraic constants behave as free variables.

Lemma 3.7 Let M be an algebraic linear term such that θ(M) = N. Then, there is a substitution φ such that φ(M) = N^{∘} and ∀x ∈ F V (M) we have φ(x) = θ(x)^{∘}.

Proof. By induction on the structure of M.

• M ≡ x. Then we define φ(x) = θ(x)^{∘} = N^{∘}.

• M ≡ f M_{1} … M_{n}. Then M is of base type and N ≡ f N_{1} … N_{n}, where θ(M_{i}) = N_{i} for i = 1 … n. By i.h. there are substitutions φ_{1}, …, φ_{n} verifying the hypothesis of the lemma such that φ_{i}(M_{i}) = N_{i}^{∘} for i = 1 … n. Let φ = φ_{1} ∪ … ∪ φ_{n}. Since M is linear φ(f M_{1} … M_{n}) = f φ_{1}(M_{1}) … φ_{n}(M_{2}) = f N_{1}^{∘} … N_{n}^{∘} = (f N_{1} … N_{n})^{∘} = N^{∘}. As every x in F V (M) is a variable in F V (M_{i}) for some 1 ≤ i ≤ n, then φ(x) is uniquely determined by φ_{i}(x) (so φ(x) = φ_{i}(x)) and by i.h. φ_{i}(x) = θ(x)^{∘}.

1Actually, this is really a family of translations, but this does not affect the proofs.

Lemma 3.8 Let M be an algebraic term, θ a substitution with F V (M) ⊆ Dom(θ) and φ the substitution defined by φ(x) = θ(x)^{∘}, for every x ∈ F V (M). Then φ(M) = θ(M)^{∘}.

Proof. By induction on M.

Theorem 3.9 (Simulation for expansions) If Γ ⊢ M : A and M⇝N, then M^{∘}⇝^{+}_{B}N^{∘}.

Proof. The proof proceeds by induction on the structure of M and then by case-analysis. We consider here only the case M ≡ f P_{1} … P_{n} and we refer the reader to [DCK94b] for all the other details.

First of all remark that f P_{1} … P_{n} is not reducible by η nor by δ because it is of base type. Therefore, there are just two cases to consider:

• If N = f P_{1} … N_{i} … P_{n}, where P_{i}⇝N_{i}, then

\begin{aligned}(f P_{1} … P_{i} … P_{n})^{∘} & = & f P_{1}^{∘} … P_{i}^{∘} … P_{n}^{∘} & ⇝^{+}_{B} by i.h. \\ f P_{1}^{∘} … N_{i}^{∘} … P_{n}^{∘} & = & (f P_{1} … N_{i} … P_{n})^{∘} & = N^{∘} \end{aligned}

• If N = θ(R), where (L, R) ∈ R and M = θ(L). By lemma 3.7 there is a substitution φ such that φ(L) = M^{∘} and for every x ∈ F V (L) we have φ(x) = θ(x)^{∘}. Since every x in F V (R) is also in F V (L), then φ(R) = θ(R)^{∘} by lemma 3.8. Hence M^{∘} = φ(L) ⟶^{R} φ(R) = N^{∘}.

Theorem 3.10 (Modularity of the strong normalization property) Let R be any strongly normalizing left-linear algebraic rewriting system. Then R plus the simply typed lambda calculus with pairing and expansion rules for η and δ is strongly normalizing.

Proof. We know by [HM90, BTG94] that the combination of a strongly normalizing left-linear algebraic rewriting system with the lambda calculus with pairing yields a strongly normalizing reduction. By proposition 3.1 and theorem 3.9, our reduction ⇝ is strongly normalizing.

Corollary 3.11 The relation ⟹^{E} is strongly normalizing.

Proof. A trivial consequence of the previous theorem. Independent proofs can be found in [Min77, Kes93].

Theorem 3.12 (Modularity of the confluence property) Let R be any confluent left-linear algebraic rewriting system. Then R plus the simply typed lambda calculus with pairing and expansion rules for η and δ is confluent.

Proof. We know by [BT88, HM90] that the combination of a confluent left-linear algebraic rewriting system with the lambda calculus with pairing yields a confluent reduction. So, our reduction relation ⇝_{B} is confluent. In view of proposition 3.2, using theorem 3.9 and lemma 3.5 this is enough to deduce that ⇝ is also confluent.

4 Adding recursion

We focus now on adding fixpoint operators to a rewriting system S. We assume a new constant fix_{A} : (A → A) → A for each type A, with the reduction rule^{2}

(fix) fix_{A} ⟶^{fix} λf.f(fix_{A} f)

We also assume that the fix constant does not occur in any rule of S. To simplify notations, we will drop the type suffix in the rest of this section.

2We choose to work with this rule instead of the more common one fix_{A} M ⟶^{fix} M(fix_{A} M), because it is computationally equivalent but allows to simplify the proofs a bit. This version is also used for example in [HM90].

4.1 The traditional approach

Let us recall here a proof technique essentially due to Lévy (see [Lév76]) that is used quite often to prove that a specific confluent calculus stays confluent when combined with a fixpoint operator. Usually, one considers an auxiliary reduction relation with bounded fixpoint operators fix^{n} and the more restrictive reduction rule^{3}

(\overline{fix})  fix^{n} ⟶^{\overline{fix}} λf.f(fix^{n−1} f) n > 0

Essentially, this puts a bound on the depth of any recursive call, so to preserve strong normalization of the original reduction relation S. If it happens that local confluence also still holds, then by

Newman’s Lemma we have confluence of this auxiliary reduction relation ⟶^{S∪\overline{fix}}. Then for the specific system under consideration one has to show the following facts:

(Erasing) If M ⟶^{S∪\overline{fix}}N, then |M| ⟶^{S∪fix}|N|, where |M| is obtained from M by removing all the indices from the fix terms.

(Lifting) For any reduction sequence M_{0} ⟶^{S∪fix}M_{1} ⟶^{S∪fix} … ⟶^{S∪fix}M_{n}, there exists an indexed

computation N_{0} ⟶^{S∪\overline{fix}}N_{1} ⟶^{S∪\overline{fix}} … ⟶^{S∪\overline{fix}}N_{n} such that |N_{i}| = M_{i}, for i = 0 … n (usually it suffices to index all the fix constructors in M_{0} by a number k ≥ n).

Finally, using just the confluence property for ⟶^{S∪\overline{fix}}, the confluence of the reduction relation ⟶^{S∪fix} can be derived using the following general proposition.

Proposition 4.1 If ⟶^{S∪fix} and ⟶^{S∪\overline{fix}} satisfy the erasing and lifting properties, then confluence of

⟶^{S∪\overline{fix}} implies confluence of ⟶^{S∪fix}.

Proof. Take any diagram M′ ∗ ⟵^{S∪fix} M ⟶^{S∪fix}∗ M′′. By lifting we get N′ ∗ ⟵^{S∪\overline{fix}} N ⟶^{S∪\overline{fix}}∗ N′′

with M = |N|, M′ = |N′| and M′′ = |N′′|. Then by confluence of ⟶^{S∪\overline{fix}} there exists a Q s.t.

N′ ⟶^{S∪\overline{fix}}∗ Q ∗ ⟵^{S∪\overline{fix}} N′′ and finally by erasing we get that M′ ⟶^{S∪fix}∗ |Q| ∗ ⟵^{S∪fix} M′′.

4.2 Our approach

Only two points of the traditional approach are really needed to prove confluence with unbounded recursion :

1. The erasing and lifting properties

2. Bounded fixpoints preserve confluence of the original specific reduction system

Indeed, the strong normalization property of ⟶^{\overline{fix}} is used only as a technical tool to prove

confluence of ⟶^{\overline{fix}}, and has no real interest: we show that bounded fixpoints preserve confluence for any reduction relation, as soon as it includes the usual β-rule, and we do not need at all the strong normalization property in the proof. For the sake of completeness, though, we will briefly also show that strong normalization is preserved for any reduction relation including the β-rule.

Surprisingly enough, only the lifting property puts some constraint on the reduction system under consideration. But let’s start with strong normalization.

3The corresponding bounded rule for the more common fixpoint rule is fix^{n} M⟶^{\overline{fix}}M(fix^{n−1} M) n > 0.

Instead of adapting an existing normalization proof to take into account the bounded fixpoint reduction rule, as is usually done, it is better to look for a more modular approach.

If one starts with a system that includes the usual β-rule for the lambda calculus, such an approach exists indeed, and is based on a very simple observation, already present for example in [Dou93], where it is used for a specific calculus:

Remark 4.2 (Bounded recursion is just iteration) What n-bounded recursion does is just nfold iteration of a function over an argument fix^{0} f. Such a behavior can be quite easily simulated in the simply typed lambda calculus by means of the terms λf.f^{n}(yf) where y is a fresh variable.

This suggests a very simple and natural translation of the fix^{n} constants into simply typed λ-terms as follows^{4}:

Definition 4.3 (Translation for fixpoints)

[[ fix^{0} ]] = y (y fresh)
[[ fix^{n} ]] = λf.f(λh.([[ fix^{n−1} ]]h)f)

We extend [[ ]] to all the terms in the calculus by just taking the identity on all terms that are not one of the fix^{n} constants.

This translation has the property that

[[ fix^{n} ]] = λf.f(λh.([[ fix^{n−1} ]]h)f) ⟶^{β} λf.f([[ fix^{n−1} ]]f)

so that every step of fixpoint reduction in the bounded recursion relation can be simulated by a β step in the relation without recursion^{5}.

Using this property, we can prove the following

Proposition 4.4 (Simulation for bounded fixpoints) Given any reduction system S that con-

tains β, if M ⟶^{S∪\overline{fix}} N, then [[ M ]] ⟶^{S}[[ N ]].

Proof. We have already shown that a \overline{fix} step can be simulated by a β step. As for S-steps, notice that this translation preserves equality, so all possible S-reductions on a term M are still possible on [[ M ]], even the non linear ones.

By proposition 3.1, we can conclude that:

Theorem 4.5 (Bounded recursion preserves strong normalization) Let S be any reduction system including the β rule for the simply typed lambda calculus. If S is strongly normalizing, then so is S plus bounded recursion.

As we already remarked, this very simple and general result has no real interest because, as we will show shortly, we can prove directly that confluence is a modular property with respect to fixpoints. We considered anyway that it was worth presenting here in view of the fact that it does not seem to be very well known: in many works normalization with bounded fixpoints is proven again and again without noticing that it is a fairly general property [PV87, HM90, DCK93].

4This translation is different from the one suggested in [Dou93], and is crucial to be able to show the modularity of the confluence property.

5Notice that we can reason in the same way if we directly take here a given fresh variable y for fix^{0}.

The traditional approach to confluence with bounded fixpoints would require here to go through any (usually old) already available proof of (local) confluence for the reduction relation without fixpoints, and find the spots where to fit the slight modifications necessary to accommodate the presence of fix^{n} in the calculus. Once this is done, if the calculus with bounded fixpoints is strongly normalizing (that is now a much easier task using the result above), one gets easily confluence using Newman’s lemma.

But we can do much better: indeed, we do not need at all to assume that the calculus without fixpoint is confluent and strongly normalizing, because we can show immediately that confluence is a modular property with respect to bounded fixpoints.

Theorem 4.6 (Bounded recursion preserves confluence) Let L be any left-linear reduction system including the β rule for the simply typed lambda calculus. If L is confluent, then so is L plus bounded recursion.

Proof. We apply proposition 3.2 taking \overline{fix} as R and L as S using our simple translation of the fix^{n} constants (definition 4.3). We already verified the simulation property. The normalization of \overline{fix} alone trivially comes from the simulation property of the translation applied to the simply typed lambda calculus, that is strongly normalizing. Finally, with our reduction rules for bounded fixpoints, in a \overline{fix} normal form there are no occurrences of fix^{n} constants with n > 0, and we can take fix^{0} to be a fixed fresh variable y, so that the translation on these normal forms is just the identity. We can then conclude that L plus bounded recursion is confluent.

When we turn to the unbounded fixpoint operator, though, we face a difficulty that limits these

results: for a general reduction relation ⟶^{S}, the confluence (with or without normalization) of ⟶^{S∪\overline{fix}} does not implies confluence for ⟶^{S∪fix}. The reason is that if there is some rule (like the contractive version of surjective pairing) where some metavariable appears more than once, it is easy to build counterexamples like the following one to the lifting property that is crucial for Lévy’s trick:

Example 4.7 Let P = λx.x, and consider the reduction sequence (λp.⟨π_{1}(p), π_{2}(p)⟩)fix P ⟶^{β}

⟨π_{1}(fix P), π_{2}(fix P)⟩ ⟶^{fix} ⟨π_{1}(P (fix P)), π_{2}(fix P)⟩ ⟶^{β} ⟨π_{1}(fix P), π_{2}(fix P)⟩ ⟶^{SP}fix P .

Whatever index n we associate to the original fix operator, there is no way to simulate the SP reduction step in the labeled calculus as required by proposition 4.1, because the occurrences of fix in the first component of the pair ⟨π_{1}(fix P), π_{2}(fix P)⟩ and the occurrences of fix in the second component of the same pair will have labels differing by 1.

Indeed, we know from [Nes89] that Klop’s counterexample [Klo80] can be adapted to show that the contractive version of surjective pairing is not confluent in the presence of a fixpoint operator.

Nevertheless, if the reduction system S is left-linear, then it is quite trivial to verify that ⟶^{S∪\overline{fix}} can simulate ⟶^{S∪fix}, so we can conclude that

Theorem 4.8 (Recursion preserves confluence of left-linear systems) Let L be any leftlinear reduction system including the β rule for the simply typed lambda calculus. If L is confluent, then so is L plus unbounded recursion.

This result can be extended to conditional rewriting systems as soon as we can guarantee that our coding of fixpoint operators satisfies the simulation property. Of course, the expansion rules for the extensional axioms for arrow and product types are interesting conditional rewrite rules to consider, and our result still holds for left-linear systems extended with these expansion rules.

The proof technique still relies on a translation: let S be our given left-linear rewriting system extended with the expansion rules for η and surjective pairing, and let R be the bounded fixpoint reduction rule alone. We cannot proceed as we did in the absence of expansion rules, because now the conditional nature of the expansions can prevent the translation of an expandable term from being expandable: for example, fix^{n} can be expanded to λg.fix^{n}g, but its translation λf.f(λh.([[ fix^{n−1} ]]h)f) cannot be expanded to λg.(λf.f(λh.([[ fix^{n−1} ]]h)f))g as it is already a λ-abstraction.

Fortunately, it is possible to modify slightly the original translation to avoid this pitfall:

Definition 4.9 (Expansion compatible translation)

≪fix^{0} ≫ = y (y fresh)
≪fix^{n} ≫ = \{ \begin{matrix}λf.f(λh.(≪fix^{n−1} ≫h)f) if fix^{n} is applied \\ (λr.λx.(rx))λf.f(λh.(≪fix^{n−1} ≫h)f) if fix^{n} is not applied \end{matrix}

We extend the translation ≪ ≫ to all the terms in the calculus by just taking the identity on all terms that are not one of the fix^{n} constants.

For this translation, η expansions are no longer problematic: indeed, if fix^{n} occurs not applied, then it can undergo an η expansion to λx.(fix^{n}x), but then

≪fix^{n} ≫ = (λr.λx.(rx))λf.f(λh.(≪fix^{n−1} ≫h)f) ⟶^{β}λx.(λf.f(λh.(≪fix^{n−1} ≫h)f)x) = ≪λx.(fix^{n}x)≫

Notice that we do not need to modify the translation in order to accommodate surjective pairing expansions, because the fix^{n} constants have always functional types, so they can never undergo SP expansions.

Anyway, we can be forced, with this definition, to give different translations to different occurrences of a same constant fix^{n}, depending on the fact that they occur applied or not. This fact has the negative consequences that:

• the translation no longer preserves equality, so it is wiser to restrict our attention to left linear rewriting systems, that are the only system we are really interested in, in view of the Theorem 4.11 for unbounded fixpoints;

• it is no longer trivial that if M ⟶^{S∪\overline{fix}}N, then ≪M ≫ ⟶^{S}≪N ≫.

Indeed, in the presence of a rule of the form:

xy ⟶^{extract}x

the term fix^{n}N would reduce to fix^{n}, while on the translations we have

≪fix^{n} N ≫ ≡ (λf.f(λh.(≪fix^{n−1} ≫h)f))N ⟶^{extract}λf.f(λh.(≪fix^{n−1} ≫h)f)

but this last term does not reduce to ≪fix^{n} ≫ ≡ (λr.λx.(rx))λf.f(λh.(≪fix^{n−1} ≫h)f) as would be required. What is happening here is that an applied subterm is extracted and put into a non applied position. We will call extractive a rule capable of doing this.^{6} For this reason, we will focus only on non-extractive rules, in view of the following Proposition 4.10 (Simulation for fixpoints with expansions) Let S be any left-linear rewriting system containing β and the expansion rules, s.t. no rule is extractive.

6This can only be a higher-order rule, but we will stay more general by forbidding only extractive rules and not all the higher order rules.

If M ⟶^{S∪\overline{fix}}N, then ≪M ≫ ⟶^{S}≪N ≫.

Proof. We first remark that β, η and SP expansions are non-extractive rules. This is evident for η and SP, while for β it comes from the fact that substitution can put a non applied term into applied position, but not vice-versa.

As for the simulation, we have already seen that there is no problem with η and SP expansions. Also,we can still simulate fix^{n} reductions (applied or not) using β:

≪fix^{n} ≫ = \{ \begin{matrix}λf.f(λh.(≪fix^{n−1} ≫h)f)⟶^{β}λf.f(≪fix^{n−1} ≫f) = ≪λf.f(fix^{n−1}f)≫ \\ (λr.λx.(rx))λf.f(λh.(≪fix^{n−1} ≫h)f)⟶^{β}λf.f(≪fix^{n−1} ≫f) = ≪λf.f(fix^{n−1}f)≫ \end{matrix}

Finally, notice that a nonextractive rule cannot extract an applied subterm and put it in a non applied position, but it can put a non-applied subterm in an applied position, like in the case of the following β reduction:

(λx.xM)fix⟶^{β}fix M

This kind of situation is very easy to handle, because the translation of a non-applied fix^{n} constant reduces (via β) to the translation of an applied fix^{n} constant, so we just need to perform some additional β steps. On the example above:

≪(λx.xM)fix≫ ≡ (λx.xM)((λr.λx.(rx))λf.f(λh.(≪fix^{n−1} ≫h)f))
⟶^{β} ((λr.λx.(rx))λf.f(λh.(≪fix^{n−1} ≫h)f)) M
⟶^{β}∗ (λf.f(λh.(≪fix^{n−1} ≫h)f)) M ≡ ≪fix M ≫

Then, we can apply again proposition 3.2 and proposition 4.1 and conclude that

Theorem 4.11 (Modularity of confluence with fix and expansions) Let L be any left-linear non-extractive rewriting system containing β and extended with expansion rules for η and surjective pairing. If L is confluent, then so is L plus unbounded recursion.

5 Conclusions and future work

We have shown that extensional equalities can be easily incorporated in higher order programming languages with algebraic data-types: the problems encountered in previous work to accomplish this goal where not due to extensional equalities themselves, but to the wrong choice of orientation of the associated rewrite rules. The well known modularity results for confluence and normalization extend naturally once we choose expansion rules instead of the traditional contractive ones, thus providing a fully satisfactory solution to this long standing problem. In particular, this proves a simple way of deciding extensional equality that does not rely on ad-hoc normalization strategies as is done in previous works. We believe that this new approach can be successful also in the framework of polymorphic calculi, where the contractive interpretation of extensional equalities poses similar problems.

We have also shown how to deal in full generality with fixpoint combinators: confluence is preserved under very permissive hypotheses, so that for many interesting calculi it is now possible to focus on the recursion-free fragment.

Based on an earlier presentation of these results which appeared in [DCK94a], Oostrom showed that the same results can be obtained using a different proof technique that makes use of developments ??.

These observations have another nice consequence: it is a long time that many people (including the authors) was looking for a confluent rewriting system for the lambda calculus with extensional (categorical) sums. We know that categorical sums are incompatible with arbitrary fixpoints on terms, so the goal was set to find such a system without general recursion, but with weaker notions, like integer iteration or no recursion at all. The last theorem above narrows sharply the region of this quest: it tells us that any confluent (and consistent) left-linear rewriting system with just β and extensional sums would yield a confluent (and consistent) rewriting system with unbounded recursion, which we know is impossible. So, if any confluent reduction system ever exists for extensional sums, it cannot be left-linear.

This fact is stated in a weaker form in [Dou93]: there it is noticed that an equivalent of theorem 4.5 used in conjunction with Lévy’s trick rules out any left-linear confluent and strongly normalizing rewriting system (but this simple observation does not hold in the presence of conditional rules). Our more general technique can be used to rule out even the conditional rule (!+) suggested in [Dou93].

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.

[BT88] Val Breazu-Tannen. Combining algebra and higher order types. In IEEE, editor, Proceedings of the Symposium on Logic in Computer Science (LICS), pages 82–90, July 1988.

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

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

[DCK93] Roberto Di Cosmo and Delia Kesner. A confluent reduction for the extensional typed λ−calculus with pairs, sums, recursion and terminal object. In Andrzej Lingas, editor, Intern. Conf. on Automata, Languages and Programming (ICALP), volume 700 of Lecture Notes in Computer Science, pages 645–656. Springer-Verlag, 1993.

[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)21, number 820 in 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.

[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.

[HM90] Brian Howard and John Mitchell. Operational and axiomatic semantics of pcf. In Proceedings of the LISP and Functional Programming Conference, pages 298–306. ACM, 1990.

[JG92] Colin Barry Jay and Neil Ghani. The virtues of eta-expansion. Technical Report ECS-LFCS-92-243, LFCS, 1992. University of Edimburgh, to appear inJournal of Functional Programming.

[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.

[Kes93] Delia Kesner. La définition de fonctions par cas à l’aide de motifs dans des langages applicatifs. Thèse de doctorat, Université de Paris XI, Orsay, december 1993. To appear.

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

[Lév76] Jean-Jaques Lévy. An algebraic interpretation of the λβκ-calculus and a labelled λ-calculus. Theoretical Computer Science, 2:97–114, 1976.

[Min77] Gregory Mints. Closed categories and the theory of proofs. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V.A. Steklova AN SSSR, 68:83–114, 1977.

[Nes89] Dan Nesmith. An application of klop’s counterexample to a higher-order rewrite system. Draft Paper, 1989.

[PV87] Axel Poigné and Josef Voss. On the implementation of abstract data types by programming language constructs. Journal of Computer and System Science, 34(2-3):340–376, April/June