Notes on the Confluence Property of Term Rewritings Systems and the λ-calculus

Zena M. Ariola Aiken Computational Laboratory Harvard University October 19, 1993

In this document we will prove the Church-Rosser theorem for both Regular^{1} Term Rewriting Systems (TRS’s) and the λ-calculus.

We also review some powerful proof methods, which require the introduction of basic notions about ordering relations.

1Researchers have coined the word “Orthogonal” for this subclass of TRS’s. However, in this document we will play conservative and still use the widely known term “Regular”.

1 Basic Definitions and Properties

Throughout the paper we will make use of the following notation:

− ; → ; →_{R} reduction relation induced by R
− ; → ; →^{+}  1 or more steps reduction
− ; → ; →^{n}  n steps reduction
− ; − ; →^{ρ}  reduction of redex ρ
ρ ⊆ M ρ is a subterm of term M

1.1 Ordering Relations

We first give a number of examples of ordering relations on a set X.

1. X = {{a}, {b}, {a, b}} and x R y := x ⊆ y

{a, b}
⊆  ⊆
{a}  {b}

2. X = P({a, b}) = {∅, {a}, {b}, {a, b}} and x R y := x ⊆ y

{a, b}

⊆  ⊆
{a}  {b}
⊇  ⊇
∅

3. X = {2, 3, 4, 6, 8, 12} and x R y := x is a divisor of y

4. X = {1, 2, 3, 4, 6, 8, 12, 24} and x R y := x is a divisor of y 5. X= Z and x R y := x ≤ y

6. X= N and x R y := x ≤ y

7. X= N × N and ⟨a, b⟩R⟨x, y⟩ := a ≤ x ∨ (a = x ∧ b ≤ y).

⟨0, 0⟩, ⟨0, 1⟩, ⟨0, 2⟩, ⋯ ⟨1, 0⟩, ⟨1, 1⟩, ⟨1, 2⟩, ⋯ ⟨2, 0⟩, ⋯

Definition 1.1 Let R be a binary relation on a set X. We say

- R is reflexive if ∀x ∈ X [x R x]

- R is irreflexive if ∀x ∈ X [¬x R x]

- R is antisymmetric if ∀x, y ∈ X [x R y ∧ y R x ⟹ x = y]

- R is transitive if ∀x, y, z ∈ X [x R y ∧ y R z ⟹ x R z]

- R is trichotomous if ∀x, y ∈ X [x R y ∨ y R x ∨ x = y]

Definition 1.2 (Weak Partial Ordering) A relation R on a set X is a weak partial ordering on X iff R is reflexive, antisymmetric, and transitive.

The one satisfying irreflexivity is named strict partial ordering. Hereon, if otherwise specified, we will assume that the partial order is a weak partial order. It is customary to use the symbol ⊑ for a weak partial order, and for a strict partial order. Note that the reason for the qualification partial is that some questions about order may be left unanswered.

Check that in the Examples 1 through 7, R is a weak partial ordering on X.

Instead of “R is a partial ordering on X” one sometimes says that “X =⟨X, R⟩ is a partially ordered set”. In the following, we will not make the distinction between a partially ordered set and the domain of the partial order, that is, we will use X and X interchangeably.

Definition 1.3 (Minimal element) A minimal element of a partially ordered set (X, ⊑) is a y in X such that

∄ x ∈ X [x ⊑ y ∧ x ≠ y]

Definition 1.4 (Least element) The least element of a partially order set (X, ⊑) is a y ∈ X such that

∀x ∈ X, y ⊑ x

Note that the least element, if it exists, is unique, and the least element is necessarily a minimal element. But, conversely, a minimal element is not necessarily a least element. In Example 1. {a} and {b} are minimal elements of X, but X does not have a least element. In Example 2. ∅ is the least element of X and hence also a minimal element of X. In Example 3. 2 and 3 are minimal elements of X, but X does not have a least element. In Example 4. 1 is the least element and hence also a minimal element of X. In Example 5. X has not minimal elements and hence no least element either.

Maximal element of X and the greatest element of X are defined analogously.

Definition 1.5 (Upper Bound) Let the set X be partially ordered by ⊑, z is the upper bound of a subset S of X (S ⊑ z) iff ∀x ∈ S [x ⊑ z]

Definition 1.6 (Least Upper Bound (Lub)) Let the set X be partially ordered by ⊑, z is the least upper bound of a subset S of X (denoted as ⨆ S) iff:

1. S ⊑ z (z is an upper bound);

2. ∀x ∈ X, S ⊑ x ⟹ z ⊑ x.

Note that a subset S of a partially ordered set X can have at most one least upper bound (by antisymmetry). Hence, in case that S has a greatest element, then this is clearly the least upper bound (lub). However, the lub for S does not need to belong to S and thus does not need to be the greatest element of S.

In Example 3. the set {8, 12} does not have an upper bound, so no lub. The set {4, 6} has two upper bounds, 8 and 12, respectively, but no lub. 12 is the lub of {2, 3, 6, 4, 12}.

Lower bound and greatest lower bound are defined analogously.

Definition 1.7 (Weak Linear Ordering) A relation R is a weak linear (total) ordering on X iff R is a weak partial ordering and R is trichotomous.

Analogously, we can define a strict linear ordering. A linear order is frequently called a chain. Examples 5.,6. and 7. are weak linear orders.

Definition 1.8 (Weak Well-ordering) A relation R on a set X is a weak well-ordering on X iff

i) R is a weak linear ordering;

ii) iff each non-empty subset has a least element.

The definition of a strict well-ordering implies that R is irreflexive. The relation R as defined in Example 6. is a weak well-ordering, while R in Example 5. is not, because X has no least element. As an exercise you can show that N is weakly well-ordered by ≤. On the other hand, (Z, ≤) is not a weakly well-ordered set.

Remark: One consequence of the above definition is that every well-ordered set X is totally ordered. Let x, y ∈ X, then {x, y} is a non-empty subset of X and has therefore a least element. If the least element is x, then x ⊑ y, otherwise, y ⊑ x.

We are interested in strict well-ordered sets because we can prove properties of their elements using a process similar to mathematical induction.

Definition 1.9 (Initial segment) Let X be a partially ordered set, if x ∈ X, then

{y ∈ X | y x}

is called the initial segment of x; we shall denote it by s(x).

Note that in the above definition we used the symbol and not ⊑. For this reason the above is usually called the strict initial segment of x.

Theorem 1.10 (Transfinite induction) Given a subset S of a strict well-ordered set X, then

[∀x ∈ X, s(x) ⊆ S ⟹ x ∈ S] ⟹ S = X

Proof: Suppose that S ≠ X. Since X is well-ordered then (X \ S) has a least element, say x_{0}. Thus, x_{0} ∉ S ∧ s(x_{0}) ⊆ S. Since s(x_{0}) ⊆ S, it follows from the hypothesis that x_{0} ∈ S. We reached a contradiction. Therefore, S = X. ♣

Notice that in the above we didn’t make any assumption about a starting element. This is so because all the minimal elements of X are included in S by definition. If x is the minimal element of X, then s(x) is empty, and since s(x) ⊆ S then x ∈ S.

If the set X is the set of terms defined over a given signature, it is interesting to think under which conditions the reduction relation − ; → ; → defines a partial ordering on X. We can think of the reduction relation as establishing an ordering between terms. For example, you can read x − ; → ; →^{n} y, with n ≥ 1, as saying y x. By definition is irreflexive and transitive, but, in general it is not antisymmetric, in fact, we can have terms M and N, such that

(M − ; → ; → N) ∧ (N − ; → ; → M) ∧ (M ≠ N).

However, if − ; → ; → is strongly normalizable then it is easy to verify that does satisfy the antisymmetric property, because it will never happen that (M − ; → ; → N) ∧ (N − ; → ; → M). Moreover, the strong normalization property guarantees that each non-empty subset of X has a minimal element.

Definition 1.11 (Minimum condition) A partially ordered set X satisfies the minimum condition if each non-empty subset of X has a minimal element.

Definition 1.12 (Noetherian Relation) Given a TRS (X, R), R is said to be noetherian if ⟨X, R⟩ satisfies the minimum condition.

Before introducing the noetherian principle we introduce a new definition, which says that a predicate is complete if it holds for an arbitrary element x of X whenever it holds for all elements less than x.

Definition 1.13 (Complete) Let P be a predicate defined on a partially order set X. We say that P is complete iff

∀x ∈ X, (∀y x P (y)) ⟹ P (x)

Theorem 1.14 (Noetherian Induction) Given TRS (X, R), if R is noetherian and P is a complete predicate then

∀x ∈ X, P (x)

Proof: Suppose, by contradiction, that P does not hold in each element of X, therefore, the set S of all elements which do not satisfy P is non-empty. Since R is noetherian from its definition we have:

∃m ∈ S such that ∀z ∈ S, m z

This means that s(m) ∩ S ≠ ∅ (otherwise m would not be a minimal element). We then have

s(m) ⊈ S ∧ m ∈ S

This contradicts the hypothesis that P is a complete predicate. Therefore, S is the empty set. ♣

At this point the reader may feel confused about the difference among the various kinds of induction principles he may have come across. In the following, we will try to throw some light on these differences, if any. We will consider mathematical induction, structural induction and transfinite induction. Let’s first say that noetherian induction is the general version of structural induction. Structural induction, as the name may recall, consists in reasoning on the structure of a term or formula. For example, most of the proofs in propositional logic, go like this:

suppose ϕ and ψ are true, then prove that ϕ ∧ ψ is true

We clearly have a partial ordered set (i.e., ϕ (ϕ ∧ ψ) and ψ (ϕ ∧ ψ)), which satisfy the minimum condition, where the minimal elements are the atomic terms or formulae. The main difference between structural induction and both mathematical induction and transfinite induction, is that the first is defined on partially ordered sets, where each chain has a least element, while both mathematical induction and transfinite induction require that an arbitrary subset of X has a least element. Moreover, structural induction, like transfinite induction, passes to each element from the set of its predecessors, and, as said before, does not make any assumption about a starting element.

An an application of noetherian induction we give the proof of the following lemma.

Lemma 1.15 (Newman’s Lemma) SN ∧ WRC ⟹ CR .

Proof: Since the reduction relation is SN then all we have to show is that the following predicate P (x) is complete

P (x) : ∀y, z, [x − ; → ; → y ∧ x − ; → ; → z ⟹ ∃ s such that y − ; → ; → s ∧ z − ; → ; → s]

Without loss of generality assume that

x − ; − ; → y_{1} − ; → ; → y ∧ x − ; − ; → z_{1} − ; → ; → z

By WCR:

∃ u, y_{1} − ; → ; → u ∧ z_{1} − ; → ; → u

By induction hypothesis P holds in y_{1} (since y_{1} x),

∃ v, y − ; → ; → v ∧ u − ; → ; → v

By induction hypothesis P holds in z_{1} (since z_{1} x),

∃ s, v − ; → ; → s ∧ z − ; → ; → s

Thus proving P(x). See the diagram below:

x  \overline{>} z_{1}  \overline{>} z
∨ W CR ↓ ↓  ↓ ↓
y_{1} − ; → ; → u HP
↓ ↓ HP ↓ ↓
y − ; → ; → v − ; → ; → t
♣

1.2 Reduction Properties

Hereon we will not make the distinction between a set of rules R and the induced reduction relation − ; − ; →_{R}. Definition 1.16 (Diamond Property) Let R be a reduction relation on a set X. Then R has the diamond property (notation R ⊧ ⋄ ) if

∀ t, t_{1}, t_{2} ∈ X [t − ; − ; → t_{1} ∧ t − ; − ; → t_{2} ⟹ ∃ t_{3} [t_{1} − ; − ; → t_{3} ∧ t_{2} − ; − ; → t_{3} ]]

See diagram below:

t

[figure]
t_{1}  t_{2}
[figure]

t_{3} Fact 1.17 R ⊧ ⋄ ⟹ R^{∗} ⊧ ⋄.

Fact 1.18 R ⊧ ⋄ ⟹ R ⊧ CR.

Definition 1.19 (Underlining) Let R be a reduction relation in X, define \underline{R} and \underline{X} as follows

- \underline{R} is the reduction relation in \underline{X}, obtained by underlining all the leftmost function symbols in the left-hand-side of the reduction rules in R.

- \underline{X} is the set containing all terms in X, plus terms with some function symbols underlined.

There are operations that allow us to go from the structure (X,R) to (\underline{X},\underline{R}) and vice-versa. One can convert a term t in X to t′ in \underline{X} by possibly underlining some function symbols (lifting). Conversely, a term t′ in \underline{X} can be converted to t in X by erasing all underlnings ( i.e., t =| t′ |) . More formally:

Lemma 1.20

(i)

t′ > t′_{1} t′, t′_{1} ∈ \underline{X}
||∨  ∨||
t − ; → ; → t_{1}  t, t_{1} ∈ X

(i)

t′ − ; → ; → t′_{1}  t′, t′_{1} ∈ \underline{X}
||∨  ∨||
t  > t_{1}  t, t_{1} ∈ X

Definition 1.21 (Development with respect to F) Given a term t ∈ X, and F a set of redex occurrences in t, let t′ ∈ \underline{X} be the term obtained by underlining the redexes in F, then the reduction sequence σ : t′ → t′_{1} → … → t′_{n} in \underline{R} is called a development of t with respect to F . A development of a term t is a development of t with respect to the set of all redex occurrences in t.

Informally, the previous definition says that a development of a term t is a reduction in which only “old” redexes (i.e., , redexes already present in t), are rewritten.

Definition 1.22 (Complete Development with respect to F) Given a term t ∈ X, and F a set of redex occurrences in t, let t′ ∈ \underline{X} be the term obtained by underlining the redexes in F, then the reduction sequence σ : t′ → t′_{1} → … → t′_{n} in \underline{R} is called a complete development of t with respect to F, if t′_{n} does not contain any more underlines. A complete development of a term t is a complete development of t with respect to set of all redex occurrences in t.

2 Confluence for Regular TRS’s

The proof of CR for Regular TRS’s follows the steps below:

(i) R Regular ⟹ \underline{R} is Regular (lemma 2.1) (ii) \underline{R} ⊧ WCR ( lemma 2.1 and lemma 2.3) (iii) \underline{R} ⊧ SN (lemma 2.4) (iv) (ii ∧ iii) ⟹ \underline{R} ⊧ CR (by Newman’s lemma)

(v) R ⊧ CR (because R^{∗} = \underline{R}^{∗}) The main point to grasp here is that in order to show that a reduction relation R is CR, we define a new reduction relation \underline{R}, for which it’s easier to show that is CR. We reduce the problem to something more tractable, and the translation between the two different problems is given by showing that the two reduction relations have the same transitive closure. Therefore, once proved that \underline{R} is CR, it follows that R is also CR. Lemma 2.1 R Regular ⟹ \underline{R} Regular. Proof: Left to the reader. ♣ Fact 2.2 Given a Regular TRS (X,R), ∀t ∈ X, t − ; − ; →^{ρ_{1}} t_{1} ∧ t − ; − ; →^{ρ_{2}} t_{2} then the (ρ_{1}) ρ_{2}-reduction does not modify the (ρ_{2}) ρ_{1}-redex. At first look it seems that the above is only due to non-overlapping patterns. Instead also non-left linearity can cause problems. As an example, given the rules

\begin{matrix}D x x − ; − ; → x \\ I x − ; − ; → x \end{matrix}

consider the term

\underbrace{D \underbrace{(I x)}_{ρ_{1}} (I x)}_{ρ_{2}}

the ρ_{1}-reduction modify the ρ_{2}-redex. Lemma 2.3 Given a Regular TRS (X,R), R is WCR. Proof: We want to show the following:

∀t ∈ X, t − ; − ; →^{ρ_{1}} t_{1} t − ; − ; →^{ρ_{2}} t_{2} ⟹ ∃ t_{3}, t_{1} − ; → ; → t_{3} and t_{1} − ; → ; → t_{3}

We do the proof by case analysis.

1: Redexes ρ_{1} and ρ_{2} are disjoint

Trivial. See diagram below:

t
[figure: ρ_{1}; ρ_{2}]
t_{1}  t_{2}
[figure: ρ_{2}; ρ_{1}]
t_{3}

2: Without loss of generality assume that ρ_{1} is nested inside ρ_{2} Since R is regular, by the previous fact, only two cases are possible

(2.1) ρ_{2}-reduction destroys the ρ_{1}-redex; (2.2) ρ_{2}-reduction duplicates the ρ_{1}-redex;

We consider the two cases above separately.

2.1: ρ_{2}-reduction destroys the ρ_{1}-redex This means that ρ_{2} occurrs in t_{1} (ρ_{2} ⊆ t_{1}). Suppose by contradiction that the above is not true, i.e., the ρ_{1}-reduction must have erased ρ_{2}. The only way this could have happened is if ρ_{2} ⊆ ρ_{1}. In conclusion:

ρ_{1} ⊆ ρ_{2} ∧ ρ_{2} ⊆ ρ_{1} ⟹ ρ_{1} = ρ_{2}

We reached a contradiction, since R is not ambiguous.

Therefore,

t \overline{ρ_{2}} \overline{>} t_{2} ≡ t_{3}
ρ_{1}∨ [figure: ρ_{2}]
t_{1}

2.2: ρ_{2}-reduction duplicates ρ_{1} For the same reasons as before ρ_{2} ⊆ t_{1}, therefore

t \overline{ρ_{2}} \overline{>} t_{2}
ρ_{1}∨  ρ_{1}∨
⋮
ρ_{1}∨
t_{1} \overline{ρ_{2}} \overline{>} t_{3}
♣

Lemma 2.4 For any TRS (X,R), \underline{R} is SN. Proof: The proof strategy is similar to the one given in the next section. ♣ Theorem 2.5 Given a Regular TRS (X,R), R is CR.

Proof: Left to the reader. ♣

3 The λ-calculus

Hereon Λ indicates the set of λ-terms, and β indicates a reduction relation on Λ.

Fact 3.1 β |̸= ⋄.

For an example, consider:

(_{ρ} (λ x.x x)(_{τ} II)) \overline{ρ} \overline{>} (_{τ_{0}} II) (_{τ_{1}} II)
τ∨  τ_{0}∨
I (_{τ_{1}} II)
τ_{1}∨
(_{ρ} (λ x.x x) I \overline{ρ} \overline{>} II

In the above example the reduction of redex ρ duplicates the redex τ, the two copies are named τ_{0} and τ_{1} respectively. For this reason the λ-calculus has the so called duplicative property. This raises many issues regarding efficient implementations.

Proof strategy of CR for λ-calculus:

(i) Define a new type of reduction relation, − ; − ; →_{1}

(ii) − ; − ; →_{1} ⊧ ⋄

(iii) β^{∗} = − ; → ; →_{1}.

3.1 Marked λ-calculus ( Λ′)

In order to formalize the ideas of development and complete development, we introduce the new calculus Λ′. The Λ′ terms are given by the following production:

E = x | λ x.E | E E | (\underline{λ} x.E) E

The rules of Λ′ are:

\begin{matrix}β_{0} : (\underline{λ} x.M) N − ; − ; → M [N/x] \\ β : (λ x.M) N − ; − ; → M [N/x] \end{matrix}

Notice that we do not underline arbitrary λ’s, only the ones that constitute the operator part of a redex. Thus, given the well-know term (λ x.x x) (λ x.x x), you can certainly underline the first λ, obtaining (\underline{λ} x.x x) (λ x.x x). However, you should convince yourself that (λ x.x x) (\underline{λ} x.x x) is not a term in Λ′.

Definition 3.2 (Development with respect to F) Let M ∈ Λ and F a set of redex occurrences in M, then σ is a development of M relative to F iff the lifted reduction σ’, starting with \underline{M}, is a β_{0}-reduction, where \underline{M} is M with all the redexes in F underlined,

Definition 3.3 (Complete Development with respect to F) Let M ∈ Λ and F a set of redex occurrences in M, then σ : M − ; → ; → M_{1} is a complete development of M relative to F iff the lifted reduction σ′ : \underline{M} − ; → ; → \underline{M_{1}} is a β_{0}-reduction and \underline{M_{1}} is a normal form with respect to β_{0}.

As an example, consider:

(_{ρ} (\underline{λ} x.x x)(_{τ} \underline{I}(I a))) \overline{ρ} \overline{>} (_{τ} \underline{I} (I a)) (_{τ} \underline{I} (I a))
τ∨  τ∨
(I a) (_{τ} \underline{I} (I a))
τ∨
(_{ρ} (\underline{λ} x.x x) (I a)  \overline{ρ}  \overline{>} (I a) (I a)

3.2 Confluence for λ-calculus

Definition 3.4 (Variable Convention) Given a λ-term M then all bound variables of M are supposed to be different from the free variables.

From now on we will always assume that all terms satisfy the variable convention.

Lemma 3.5 (Substitution lemma) If x ≢ y and x ∉ FV(L), then

M [N/x][L/y] ≡ M [L/y][N [L/y]/x]

Proof:[By structural induction]

1: M is a variable

1.1: M ≡ x Perform the substitution in both sides and you obtain

N [L/y] ≡ N [L/y]

1.2: M ≡ y

Perform the substitution in both sides and you obtain

L ≡ L [N [L/y]/x] ≡ L x ∉ F V (L)

1.3: M ≡ z ≢ x, y

In both sides we obtain z

2: M ≡ M_{1} M_{2} Follows directly from induction hypothesis

3: M ≡ λ z.M_{1} By the variable convention we may assume z ≢ x, y and z ∉ F V (N) ∪ F V (L).

(λ z.M_{1}) [N/x][L/y] ≡ λ z.(M_{1} [N/x][L/y])  by definition of substitution
≡ λ z.(M_{1} [L/y][N [L/y]/x]]) by induction hypothesis
≡ (λ z.M_{1}) [L/y][N [L/y]/x]] by definition of substitution
♣

Lemma 3.6 β_{0} ⊧ WCR. Proof: Let ρ_{1} and ρ_{2} be the two redexes contracted, we will do the proof by case analysis on the relative position of ρ_{1} and ρ_{2}.

1: ρ_{1} and ρ_{2} are disjoint Trivial

2: Without loss of generality assume that ρ_{1} ⊆ ρ_{2} Assume that ρ_{1} ≡ (\underline{λ} y.P) Q and ρ_{2} ≡ (\underline{λ} x.M) N.

2.1: ρ_{1} ⊆ M.

Follows from Substitution lemma. 2.2: ρ_{1} ⊆ N.

(_{ρ_{2}} (\underline{λ} x. · · · x ⋯ x)(⋯ (_{ρ_{1}} (\underline{λ} y.P)Q) ⋯) \overline{ρ_{2}}\overline{>} ⋯ (_{ρ_{1}} (\underline{λ} y.P) Q) ⋯ (_{ρ_{1}} (\underline{λ} y.P) Q) ⋯
ρ_{1}∨  ρ_{1}∨
⋮
ρ_{1}∨
(_{ρ_{2}} (\underline{λ} x. · · · x ⋯ x)(⋯ P [Q/y] ⋯)) \overline{ρ_{2}}  \overline{>} ⋯ P [Q/y] ⋯ P [Q/y] ⋯
♣

We are going to show next that β_{0} is SN. The main technique to prove that a reduction relation in a set X is SN, is to show that the reduction relation well-orders X, that is, each chain in X has a minimal element. Thus we proceed as follows:

• Assign a weight to each M ∈ Λ′, call the term so obtained | M |

• show:

M − ; − ; → N ⟹ | N | < | M |

that is, the “weight” of a term is decreasing as we reduce it.

Definition 3.7 (Weighting) Given M in Λ, associate a positive integer to each variable occurrence in M.

We thus obtain a new calculus, Λ^{∗}, that has the usual inductive definition with the variables ranging over x^{0} ⋯ x^{n}. The definition of reduction on Λ^{∗} (β_{0}^{∗}) carries over in the usual way.

Definition 3.8 (Weight) Let M in Λ^{∗}, define | M | as the sum of the weights occurring in M.

Definition 3.9 (Decreasing Weighting Property) Let M in Λ^{∗}, then M has decreasing weight property (dwp) if for every β_{0}^{∗}-redex (\underline{λ}x.P)Q in M :

∀x ∈ P, | x | > | Q |

Example: (\underline{λ}x.x^{6}x^{7})(\underline{λ}x.x^{2}x^{3}) has the dwp, while (\underline{λ}x.x^{4}x^{7})(\underline{λ}x.x^{2}x^{3}) does not.

Lemma 3.10 For all M in Λ^{∗}, there exists an initial weight assignment so that M has decreasing weight property.

Proof: Start enumerating all variables occurrences in M from right to left, and assign to the m^{th} variable occurrence the weight 2^{m}. Since

2^{m} > 2^{m−1} + 2^{m−2} + ⋯ 2 + 1

M has the dwp. ♣

Lemma 3.11 If M − ; − ; → N, and M has dwp then

| N | < | M |

Proof: Let M be ⋯ (\underline{λ}x.P)Q ⋯

1: x ∉ P Then Q vanishes

2: x ∈ P The weight must decrease because the weight of the substituted expression, i.e., | Q |, is less than every x.

♣

Lemma 3.12 Let M − ; − ; → N, then if M has dwp so does N.

Proof: Suppose M − ; − ; →^{R_{0}} N, where R_{0} ≡ (\underline{λ}x.P_{0})Q_{0}. Examine the effect of R_{0}-reduction on some other redex R_{1} ≡ (\underline{λ}y.P_{1})Q_{1} in M. We will do the analysis on the relative positions of R_{0} and R_{1}.

1: R_{0} ∩ R_{1} = ∅ R_{0}-reduction does not affect R_{1}

2: R_{1} ⊆ R_{0} 2.1: R_{1} is inside the rator \underline{λ}x.P_{0}

R_{0} ≡ (\underline{λ}x. · · · ((\underline{λ}y.P_{1})Q_{1}) ⋯)Q_{0}.

By the dwp of M,

∀y ∈ P_{1}, | y | > | Q_{1} |

and, by the fact that y ∉ FV(Q_{0}),

∀y ∈ P_{1} [Q_{0}/x], | y | > | Q_{1} |

And,

∀x ∈ R_{0}, | x | > | Q_{0} |

then

| Q_{1} | > | Q_{1} [Q_{0}/x] |

In conclusion,

∀y ∈ P_{1} [Q_{0}/x], | y | > | Q_{1} [Q_{0}/x] |

2.2: R_{1} is inside the rand Q_{0}

R_{0} ≡ (\underline{λ}x.P_{0})(⋯ R_{1} ⋯)

R_{0}-reduction does not modify R_{1} (may just copy it or destroy it) 3: R_{0} ⊆ R_{1}

3.1: R_{0} is inside the rator of R_{1}

R_{1} ≡ (\underline{λ}y. · · · ((\underline{λ}x.P_{0})Q_{0}) ⋯)Q_{1}

The weights of any y’s in R_{1} are not affected by R_{0}-reduction. 3.2: R_{0} is inside the rand of R_{1}

R_{1} ≡ (\underline{λ}y.P_{1})(⋯ ((\underline{λ}x.P_{0})Q_{0}) ⋯)

The weight of Q_{1} after R_{0}-reduction decreases.

♣

From the previous lemma we can infer, Lemma 3.13 β_{0} ⊧ SN. Corollary 3.14 β_{0} ⊧ CR. Proof: By Newman’s lemma, since β_{0} is WCR and SN. ♣ Theorem 3.15 (Finite Development) Let M ∈ Λ and F ⊆ M

(i) All developments of M related to F are finite; (ii) All complete developments of M related to F end up with the same term.

Proof:

(i) follows from lemma 3.13 (ii) follows from corollary 3.14 ♣

We can now define the new reduction relation,

Definition 3.16 (Parallel reduction) M − ; − ; →_{1} N, iff N is the result of a complete development of M with respect to some F.

Notice that one step of the parallel reduction consists in reducing multiple redexes. Exercise: Let M ≡ (λ x.x x)(I I). Then it is a good exercise to see what M parallel reduces to. In particular, does M

− ; → ; →_{1} I (I I) ?.

Theorem 3.17 − ; − ; →_{1} ⊧ ⋄.

Proof:

\begin{aligned}t & \overline{F_{2}} & \overline{>} & t_{2} \\ F_{1}∨ & [figure: F_{1} ∪ F_{2}] & ∨ & F′_{1} \\ t_{1} & F′_{2} & > & t_{3} \end{aligned}

Follows from the finite development (theorem 3.15) that ∃ a complete development of t with respect to F_{1} ∪ F_{2}: t − ; − ; →_{1} t_{1} − ; − ; →_{1} t′_{3}. Analogously, we have the complete development with respect to F_{2} ∪ F_{3}: t − ; − ; →_{1} t_{2} − ; − ; →_{1} t′′_{3}. Since β_{0} is CR, it must be the case that t′_{3} ≡_{α} t′′_{3}. ♣

Theorem 3.18 − ; → ; →_{β}=− ; → ; →_{1} .

Proof: Left to the reader. ♣

Theorem 3.19 β ⊧ CR.

Proof: Follows from the diamond property of the parallel reduction (theorem 3.17) and the fact that β and the parallel reduction do have the same transitive closure (theorem 3.18). ♣

Acknowledgements

Funding for this work has been provided in part by the Advanced Research Projects Agency of the Department of Defense under the Office of Naval Research contract N00014-84-K-0099 (MIT) and N0039-88-C-0163 (Harvard).

Many thanks to Arthur Lent and Allyn Dimock for reading the current draft of the paper and for providing insightful comments.