Project topics and materials
Get Complete Project Material File(s) Now! »
Normalization properties of the λµµ′-calculus
Before turning our attention to the main subject of the present chapter we list some of the basic definitions and notation which will be used in the sequel. Most of the definitions are taken from Klop [32].
Definition 28 An Abstract Reduction System (ARS) is a pair A = {Σ, (→i)i∈I }, where Σ is a set and (→i)i∈I is a set of binary relations defined on Σ. The relations (→i)i∈I are called reduction relations.
Remark 29 The sets we are concerned are sets of terms of some calculi. In every case it is supposed that a reduction relation → is compatible with the term formation rules.
Definition 30 Let → be a reduction relation. Then ։ is its reflexive, transitive, →+ is its transitive, →= is its reflexive closure. →n (n ≥ 0) denotes the n-step reduction (the n-th product relation obtained from →). Moreover, if →1, →2 are reductions, then →1,2 means the union of the two reductions as relations.
Remark 31 Let A = {Σ, (→i)i∈I } be an ARS. In the definitions below we denote by → the union of the set of reductions (→i)i∈I .
Definition 32 Let A = {Σ, (→i)i∈I } be an ARS. Then a ∈ Σ is in normal form, if there is no b ∈ Σ such that a → b. In notation: a ∈ N F . Further, a has a normal form, if there is a b in normal form for which a ։ b. In this case, the reduction sequence starting from a and yielding a b ∈ N F is called a normalizing reduction sequence for a.
Definition 33 The reduction relation → on an every a has a normal form. In this case we also (in notation: A is W N ).
ARS A is weakly normalizing, if say that A is weakly normalizing
Definition 34 Let A be an ARS. We say that an element a ∈ A strongly normal-izes (a ∈ SN ), if every reduction sequence starting from a is finite. A is strongly normalizing (A is SN ), if, for every a ∈ A, a ∈ SN .
Definition 35 An ARS A is finitely branching, if, for all a, the set of one-step reducts of a, {b | a → b}, is finite.
Remark 36 If we have a finitely branching A, then, by K¨onig-lemma, Definition 34 is equivalent to saying that the length of each reduction sequence starting from a is bounded uniformly by some number n.
Thus, the following definition makes sense:
Definition 37 Suppose A is SN , let a ∈ A. Then η(a) denotes the length of the longest reduction sequence starting from a.
Definition 38 A reduction relation is confluent (or Church-Rosser), if it is self-commuting. That is, for every a, b, c ∈ Σ there is a d such that a ։ b and a ։ c imply b ։ d and c ։ d.
Definition 39 Let A be →1 if, for every a, b ∈ Σ, an ARS. The relation →2 in A can be postponed w.r.t. a ։1,2 b implies a ։1 c ։2 b for some c.
Definition 40 Let A be an ARS. The relation →2 in A can be strongly postponed w.r.t. →1 if for every a, b ∈ Σ such that a ։1,2 b and the reduction sequence contains at least one →1-reduction we have a →+1 c ։2 b for some c.
The Parigot-style λµµ′-calculus
The θ-rule can be postponed
In the sequel, we are concerned with the untyped µµ′ρ- and the simply typed λµµ′ρ- and λµµ′ρθ-calculi. In the first subsection of the chapter we examine the Parigot-style formulation and in the second one the de Groote-style formulation of the calculi. As for the basic definitions and notations we refer to the introduction. We prove in this subsection that the θ-rule can be postponed w.r.t. the β-, µ-and µ′-rules. Though, the proof is implemented in the Parigot-style λµ-calculus, it remains valid in the de Groote-style calculus as well. Prior to this, we present some more definitions frequently used later on.
Definition 41 The complexity of a term is defined inductively as follows.
cxty(x) = 1,
cxty((α M )) = cxty(M ) + 1,
cxty(λxM ) = cxty(M ) + 1,
cxty(µαM ) = cxty(M ) + 1,
cxty((M N )) = cxty(M ) + cxty(N ) + 1.
The complexity of a term in the de Groote-style λµµ′-calculus is understood in an analogous way, with the necessary notational changes.
Notation 42 1. We use the notation N ≤ M (or M ≥ N ) if N is a subterm of M , and the notation N < M (or M > N ) if N is a subterm of M other than M .
By ηc(M ) we denote the lexicographically ordered pair η(M ), cxty(M ) for a term M .
Definition 43 Let M , N be terms. N ≺ M (or M ≻ N ) will denote the fact that there is an M ′ such that M ։ M ′ ≥ N holds and either M →+ M ′ or M > N is valid. will be the reflexive closure of ≺.
Remark 44 1. ≺ and are transitive. Moreover, N M iff there is an M ′ such that M ։ M ′ ≥ N . N ≺ M implies ηc(N ) < ηc(M ).
Having settled the necessary terminology we prove that the ρ- and the θ-rules can be strongly postponed w.r.t. the β-, µ- and µ′-rules. More precisely we show something more:
Theorem 45 Let M , N be such that M ։βµµ′ρθ N and the reduction sequence contains at least one β- or µ- or µ′-reduction. Then there is a P for which M →+βµµ′ P ։ρθ N.
We prove the theorem in two steps. First we establish that the θ-reduction can be strongly postponed w.r.t. all of the rules β, µ, µ′, ρ, then we show that the ρ-rule can be strongly postponed w.r.t. the remaining three rules.
Definition 46 Let →µ0 and →µ′0 be defined as follows:
(µαM N ) →µ0 µαM [α :=r N ], if α occurs at most once in M
(M µαN ) →µ′0 µαN [α :=l M ], if α occurs at most once in N .
Lemma 47 Assume M →θ P →β N . Then either we have a Q such that
M→βQ։θN,
or there are R, Q for which
M→µ0R→βQ→θN.
Proof By induction on cxty(M ). Let us only treat the case M = (M1 M2).
M1 →θ M1′. The only nontrivial case is M1′ = λxM3 and M1 = µα(α M1′). Now we obtain
= (µα(α λxM3) M2) →µ0 µα(α (λxM3 M2))
→β µα(α M3[x := M2]) →θ M3[x := M2].
Ā Ȁ ⸀Ā ᜀ Ā ᜀ Ā ᜀ Ā ᜀ Ā ᜀ Ā ᜀ Ā ᜀ Ā ᜀ Ā ᜀ Ā㴀Ā ᜀ Ā ᜀ Ā ᜀ Ā ᜀ Ā ᜀ Ā ᜀ Ā ᜀ M2 →θ M2′. Analogous to the above one. The only difference is the case M1 = λxM3, N = M3[x := M2′]. Then, with Q = M3[x := M2], we have M→βQ։θN.
The remaining cases follow easily from the induction hypothesis.
Lemma 48 Let M →θ P →µ N . Then either M→µQ։θN for some Q or there are R, Q such that M→µ0R→µQ→θN.
Proof By induction on cxty(M ). Let M = (M1 M2).
M1 = µα(α M1′) →θ M1′. The only interesting case is M1′ = µβM3. Let Q = (µβM3 M2), then, applying α ∈/ M1′, we have
= (µα(α µβM3) M2) →µ0 µα(α (µβM3 M2))
→µ µα(α µβM3[β :=r M2]) →θ µβM3[β :=r M2].
M2 = µα(α M2′) →θ M2′. Analogously. The only difference is M1 = µβM3, N = µβM3[β :=r M2′], where with Q = µβM3[β :=r M2] we obtain M →µ Q →∗θ N.
The remaining cases can be verified easily. S →nθ−1
Lemma 49 Let M →θ P →µ0 N . Then either M→µ0Q→θN for some Q or there are R, Q such that M→µ0R→µ0Q→θN.
Proof The proof proceeds as that of Lemma 48 with the necessary changes im-plemented.
Lemma 50 Let M →θ P →µ′ N . Then either M→µ′Q։θN or some Q or there are R, Q such that M →µ′0 R →µ′ Q →θ N.
Proof Similar to the proof of Lemma 48.
Lemma 51 Let M →θ P →µ′0 N . Then either we have M→µ′0Q→θN for some Q or there are R, Q such that M →µ′0 R →µ′0 Q →θ N.
Proof Analogous to that of Lemma 48.
Lemma 52 Let M →θ P →ρ N . Then we have a Q such that M→ρQ→θN.
Proof An obvious induction on cxty(M ). The only interesting case is M µα(α M1) →θ M1 →ρ M2, but then M = µα(α M1) →ρ µα(α M2) →θ M2 true.
Lemma 53 Let M →nθ P →µ0 N (resp. M →nθ P →µ′0 N ). Then there is a Q such that M ։µ0 Q →nθ N (resp. M ։µ′0 Q →nθ N ).
Proof Follows from Lemma 49 by induction on n.
Lemma 54 Let M ։θ P →βµµ′ρ N . Then there is a Q such that →+βµµ′ρ Q ։θ N.
Proof Let us suppose first M →nθ P →µ N . The proof proceeds by induction on n. We may assume n ≥ 1, that is, M →nθ−1 U →θ P holds for some U . By Lemma 48 we have either U →µ R ։θ N or U →µ0 R →µ V →θ N . In the former case the induction hypothesis applies to M →nθ−1 U →µ R. In the latter case by Lemma there exists an S such that M ։µ0 R is true, and we can apply the induction hypothesis again to S →n−1 R → V .
The proof for P →β N is similar to that for P →µ N , and, finally, the case P →ρ N is straightforward by Lemma 52.
Theorem 55 Let M ։θ P ։βµµ′ρ N such that the reduction sequence P ։βµµ′ρ is not empty. Then there is a Q for which →+βµµ′ρ Q ։θ N.
Proof By Lemma 54.
Remark 56 The above proof, thus Theorem 55, is valid in the de Groote-style λµµ′-calculus as well.
The ρ-rule can be postponed
In this subsection we show that the ρ-reduction can be strongly postponed w.r.t. the β-, µ- and µ′-reductions in the Parigot-style λµµ′-calculus. The proofs of this subsection can be found in Py [51] as well. The presentation there, however, may differ in some places from the one applied here. We also outline the proofs here so that the material is self contained.
Theorem 57 Let M ։ρ P ։βµµ′ N such that the reduction sequence P ։βµµ′ N is not empty. Then there is a Q for which M →+βµµ′ Q ։ρ N.
Lemma 58 Let M →ρ P →β N . Then we have a Q such that M→βQ։ρN.
Proof By induction on cxty(M ). Let us only treat the case M = (M1 M2).
M1 →ρ M1′. The only nontrivial case is M1′ = λxM3. Then either M1 = (α µβM4) →ρ M1′ = M4[β := α] or M1 = λxM4 and M4 →ρ M3. The first case is impossible, since then M4 = (γ M4′) for some M4′, and in the second case (λxM4 M2) →β M4[x := M2] →ρ M3[x := M2], which gives the result.
M2 →ρ M2′. Analogous to the above one. The only difference is the case M1 = λxM3, N = M3[x := M2′]. Then, with Q = M3[x := M2], M →β Q ։ρ N .
The remaining cases follow easily from the induction hypothesis.
Lemma 59 Let M , M ′, N be given such that M →ρ M ′ and α ∈/ F v(N ). Then either M [α :=r N ] →ρ M ′[α :=r N ] (resp. M [α :=l N ] →ρ M ′[α :=l N ]) or M [α :=r N ] →µ P →ρ M ′[α :=r N ] (resp. M [α :=l N ] →µ′ P →ρ M ′[α :=l N ]) for some P .
Proof By induction on cxty(M ). The only interesting case is M = (γ µβM1). 1. γ = α. Then (α µβM1)[α :=r N ] = (α (µβM1[α :=r N ] N ))
→µ (α µβM1[α :=r N ][β :=r N ])
→ρ M1[α :=r N ][β :=r N ][β := α]
M1[β := α][α :=r N ].
γ = α. In this case (γ µβM1)[α :=r N ] = (γ µβM1[α :=r N ]) →ρ M1[β := γ][α :=r N ].
Lemma 60 Let M →ρ P →µ N . Then there exists a Q for which M→µQ։ρN.
Proof By induction on cxty(M ). Assume M = (M1 M2).
M1 →ρ M1′. The only interesting case is M1′ = µγM4. In this case the only possibility is M1 = µγM3, M3 →ρ M4. This is the point where we have made use of the fact we are in the realm of the Parigot-style λµµ′-calculus. By Lemma 59 we have µγM3 M2 →µ µγM3[γ :=r M2] ։µ Q →ρ µγM4[γ :=r M2] for some Q.
M = (M1 M2), M2 →ρ M2′. Similar to the above one. The only additional case is M1 = µαM3, N = µαM3[α :=r M2′]. Then, with Q = µαM3[α :=r M2], M →µ Q ։ρ N holds.
The other cases can be verified easily.
Lemma 61 Let M →ρ P →µ′ N . Then there exists a Q for which
M→µ′Q։ρN.
Proof Analogous to the above one.
Lemma 62 Let M ։ρ P →β N . Then there exists a Q for which M→βQ։ρN.
Proof Let M →nρ P →β N . The proof goes by induction on n using Lemma 58.
Lemma 63 Let M ։ρ P →µ N (resp. M ։ρ P →µ′ N ). Then there is a Q such that M →µ Q ։ρ N (resp. M →µ′ Q ։ρ N ).
Proof Let M →nρ P →µ N . The statement follows from Lemmas 60 and 61 by induction on n.
We obtain Theorem 57 as a consequence of Lemmas 62 and 63. Theorems 55 and 57 together yield Theorem 45.
The Parigot-style λµµ′-calculus strongly normalizes
Theorem 64 The Parigot-style λµµ′-calculus with the ρ- and θ-rules is strongly normalizing.
Proof It is proved in David and Nour [14] that the de Groote-style λµµ′-calculus is strongly normalizing. Since the Parigot-style λµµ′-calculus is contained in the de Groote-style one, we have the strong normalization of the Parigot-style λµµ′- calculus as well. Let M be a λµ-term, let ηβµµ′ (M ) denote the length of the longest βµµ′-reduction sequence starting from M . We prove by induction on ηβµµ′ (M ) that has no infinite βµµ′ρθ-reduction sequence. Let M be a term, assume we have an infinite βµµ′ρθ-reduction sequence σ starting from M . Since this cannot consist entirely of ρ- and θ-reductions, we may suppose σ begins with M ։ρθ M ′ →βµµ′ M ′′ for some M ′ and M ′′. By Theorem 45 we have an N such that M ։+βµµ′ N ։ρθ M ′′. This means N would have an infinite βµµ′ρθ-reduction sequence, contradicting the induction hypothesis.
The de Groote-style λµµ′-calculus
In respect of normalization properties the de Groote-style λµµ′-calculus manifests a somewhat different behaviour than the version treated in the previous section.
We state first the following theorem:
Theorem 65 The de Groote-style λµµ′-calculus without the ρ-rule is strongly nor-malizing.
Proof For the proof see David and Nour [14].
The proof in David and Nour [14] is arithmetical in the sense that it can be formalized in Peano arithmetic. In fact, proofs for the strong normalization of the Sym λµµ˜- and λProp -calculi, which turned out in the meantime to be equivalent with the extended λµµ′-calculus (cf. Rocheteau [55] for the equivalence of λµµ˜ and λµµ′, Sym and Chapter 5 in this work for the equivalence of λµµ˜ and λProp ), were already known. Polonovski has proved that λµµ˜ is strongly normalizing (Polonovski [49]), Sym
Berardi and Barbanera proved the same for λProp , but none of these proofs were arithmetical, that is, they could not be formalized in first order Peano arithmetic. Thus, the proof in David and Nour [14] can be considered as the first arithmetical proof of the strong normalization of a symmetric logical calculus which can be related to classical logic. Proceeding in this direction all proofs in the present work are arithmetical.
The proof of Theorem 65 consists of two parts: proving first that the untyped µµ′-calculus is strongly normalizing, the demonstration of the strong normalization of the typed case can be regarded as an extension of the result for the untyped one. Keeping this method in mind, in the following investigations we also treat the untyped and typed cases separately. In the sequel, unless otherwise stated, by referring to an instance of the µµ′- or the λµµ′-calculi we understand the de Groote-style versions of the calculi.
First, we present a proof of the strong normalization of the µµ′-calculus, proba-bly somewhat simpler than the one given in David and Nour [14]. It seems to be an appealing task to find a proof for the strong normalization of the typed case along the same lines.
Table of contents :
Introduction
1 Normalization properties of the λμμ′-calculus
1.1 The Parigot-style λμμ′-calculus
1.1.1 The θ-rule can be postponed
1.1.2 The ρ-rule can be postponed
1.1.3 The Parigot-style λμμ′-calculus strongly normalizes
1.2 The de Groote-style λμμ′-calculus
1.2.1 A strong normalization proof for the μμ′-calculus
1.2.2 The μμ′ρ-calculus is not strongly normalizing
1.2.3 The μμ′ρ-calculus is weakly normalizing
1.2.4 The λμμ′ρ-calculus is weakly normalizing
1.2.5 The λμμ′ρθ-calculus
1.2.6 Standardization for the λμμ′ρθ-calculus
1.2.7 Concluding remarks
2 An estimation for the lengths of reduction sequences of the λμρθ- calculus
2.0.8 Standardization in the λμρθ-calculus
2.0.9 On the lengths of standard reduction sequences
2.0.10 The estimation for the λμρθI-calculus
2.0.11 The general case
2.1 Concluding remarks
2.1.1 A possible attempt to calculate an upper bound for the λμρ- calculus
2.1.2 A translation of the λμ-calculus into the λ∗c -calculus
3 Strong normalization of the λ Sym Prop-calculus
3.1 The λ-calculus is strongly normalizing
3.2 The cases of the η- and η⊥-reductions
3.3 The λ Sym Prop-calculus is strongly normalizing
4 Translations between the λ Sym Prop-calculus and the λμ˜μ∗-calculus
4.1 Relating the λ Sym Prop-calculus to the λμ˜μ∗-calculus
4.1.1 The λμ˜μ∗-calculus
4.1.2 A translation of the λμ˜μ∗-calculus into the λ Sym Prop-calculus
4.1.3 A translation of the λ Sym Prop-calculus into the λμ˜μ∗-calculus
4.1.4 The connection between the two translations
4.2 Concluding remarks
4.2.1 The strong normalization of the μ˜μ-calculus
4.2.2 The strong normalization of the λμ˜μ∗-calculus
Conclusions
Overview
Open questions
Bibliography
