Some thoughts on transfinite abstract reduction systems

Richard Kennaway

1 August 1996

1 Finitary systems

We briefly recall some definitions for the finitary case. These are taken from [GK93].

Definition 1.1 An abstract reduction systems or ARS consists of a set Ter of terms, a set Red of reductions, and two functions, source and target from Red to Ter. We write s ^{u} t if u is a reduction with source s and target t. u may also be called a redex of t. It is required that each term have only finitely many redexes.

Definition 1.2 A deterministic residual structure or DRA is an ARS together with a residual function denoted by /. If u is a redex of s, and s ^{v} t, then u/v is a set of redexes of t, called the residuals of u by v. The residual function is subject to several axioms, for which some further definitions are required.

The notion of the residual of a redex by a finite reduction sequence is defined by iteration in the obvious way. A development of a set U of redexes of a term is a reduction sequence in which each step reduces a residual of some member of U by the sequence so far. It is complete if the final term contains no residuals of U. We may write U to denote any complete development of the set of redexes U.

The axioms on the residual function are:

1. If u and u′ are distinct redexes of t, and v is a redex of t, then u/v and u′/v are disjoint sets.

2. u/u is empty.

3. All developments are finite (hence, every set of redexes has a complete development).

4. If S and S′ are complete developments of the same set of redexes of the same term, then they end with the same term, and for any redex u of their initial term, u/S = u/S′.

5. If u and v are distinct redexes of the same term, and u/v is empty, then v/U is nonempty.

Definition 1.3 Let s ^{u} t. A redex of t which is not a residual of any redex of s is said to be created by u. If v/u is empty, u is said to erase v. If v/u has more than one member, u is said to duplicate v.

Definition 1.4 A DRS is stable if, for any distinct redexes u and v of the same term, and any redex w created by u, every redex in w/(v/u) is created by some redex in u/v.

2 Transfinite systems

Here we define transfinite analogues of the finitary versions.

Definition 2.1 A transfinite abstract reduction system or TARS consists of a complete ultrametric space Ter of terms, a set Red of reductions, two functions, source and target from Red to Ter, and two functions δ and ϵ from Red to non-negative integers. We write s ^{u} t if u is a reduction with source s and target t. The distence between terms s and t is denoted by |s, t|.

These are subject to the following conditions.

1. If s ^{u} t, then |s, t| ≤ 2^{−δ(u)}.

2. Suppose that |t, t′| ≤ 2^{−n}, and u is a redex of t such that δ(u) + ϵ(u) ≤ n. Then there is a redex u′ of t′ such that δ(u′) = δ(u), ϵ(u′) = ϵ(u), and if t ^{u} s and t′ ^{u′} s′ then |s, s′| ≤ 2^{−n+ϵ(u)}.

The ultrametric and the functions δ and ϵ correspond to concepts in term rewriting. If two distinct terms in a concrete rewrite system have an identical common prefix of depth n, then the distance between them is 2^{−n}. δ(u) represents the depth of the redex u in the term containing it, that is, the distance from the root of the term to the root of the redex. ϵ(u) represents the depth of the pattern of the redex, that is, the maximum depth of any node in the left hand side of the rule associated with the redex.

The axioms are motivated by similar considerations. The first represents the fact that performing a reduction at a depth of d cannot change any part of the term at any lesser depth. Therefore the distance between source and target cannot be greater than 2^{−d}. The second represents the fact that if t contains a redex u whose pattern lies entirely within the common prefix of t and another term t′, then t′ must have a ‘similar’ redex. Reduction of both redexes must yield ‘similar’ terms s and s′. s and s′ may not be as close as t and t′, since reducing a redex with pattern-depth ϵ(u) may ‘lift’ subterms of t and t′ by up to that amount. Thus a difference between t and t′ at depth n may give rise to a difference between s and s′ at depth n − ϵ(u).

Notice that we have dropped the requirement that each term contain only finitely many redexes. The notion of a finite reduction sequence arises immediately by conjoining single reductions,

and this also gives the notion of a sequence of length ω. To define the limit if a sequence of length ω, and to define transfinite reductions of arbitrary ordinal length, we must use the ultrametric and the depth measure.

Definition 2.2 For any ordinal α, a reduction sequence of length α is a function from α to Red satisfying the following conditions. For each β < α we write t_{β} ^{u_{β}} s_{β} for the corresponding reduction.

1. If β + 1 < α then s_{β} = t_{β+1}.

2. t_{β} is a continuous function of β, with respect to the usual topology on ordinals and the ultrametric on Ter.

3. If λ < α is a limit ordinal, then lim_{β<λ} δ(u_{β}) = ∞.

If either α is a succesor ordinal, or condition 3 holds also for λ = α, then the sequence is said to be strongly convergent. In that case its limit is respectively s_{α−1} or the limit with respect to the ultrametric of the terms {t_{β}|β < α}.

Most of the definition of a DRS generalises in an obvious way to the transfnite setting, except for two points. Firstly, we need a notion of the residuals of a redex by an infinite reduction sequence. Secondly, we must allow for the fact that in transfinite term rewriting systems and in transfinite lambda calculus, not all sets of redexes have complete developments. The obstruction to complete developments involves the collapsing redexes, redexes of rules whose right hand side is a variable.

In our abstract setting, it turns out that we can define both transfinite residuosity and a concept of collapsing redex in terms of the concepts we already have, without introducing any new structure.

Definition 2.3 A transfinite deterministic residual structure or TDRS is a TARS together with a residual function denoted by ?. If u is a redex of s, and s ^{v} t, then u/v is a set of redexes of t, called the residuals of u by v. The residual function is subject to further axioms to be developed below.

In a TDRS as so far defined, we have the notion of the residuals of a redex by a finite reduction sequence, just as for the finitary case. Now consider a strongly convergent sequence of length ω, t_{0} ^{u_{0}} t_{1} ^{u_{1}} t_{2} ^{u_{2}} ⋯ t_{ω}. Consider a sequence of redexes v = (n_{n}, v_{n+1}, v_{n+2}, …) such that each v_{i} is a redex of t_{i}, and v_{i+1} ∈ v_{i}/u_{i}. If the depths of the v_{i} tend to a (finite) limit, then we stipulate that there is a redex of t_{ω}, denoted lim v, which is a residual of each v_{ı} by the tail of the reduction sequence. Two such sequences which differ only in which n they start with are stipulated to have the same limit.

This construction of residuals can be extended to sequences of any ordinal length by considering sequences of redexes (v_{β}|β < α) and modifying the construction in the obvious way.

Having defined the notion of residual by an arbitrary strongly convergent sequence. we can state the remaining axioms for TDRSs. They are of two sorts: those which correspond to the axioms for DRSs, and those specific to the transfinite setting.

Axiom 2.4 The generalised finitary axioms are:

1. If u and u′ are distinct redexes of t, and v is a redex of t, then u/v and u′/v are disjoint sets.

2. u/u is empty.

3. If S and S′ are complete developments of the same set of redexes of the same term, then they end with the same term, and for any redex u of their initial term, u/S = u/S′.

These are just the finitary axioms, with the exclusion of the property of finite developments.

Axiom 2.5 The transfinite axioms are:

1. For any strongly convergent reduction sequence S, if v′ ∈ v/S, then ϵ(v′) = ϵ(v).

2. Let v′ ∈ v/u. If δ(v) ≤ δ(u), then δ(v′) = δ(v) and v/u has exactly one member. Otherwise, δ(v′) ≥ max(δ(u), δ(v) − ϵ(u)).

The first of these axioms corresponds in the concrete case to the fact that the resiiduals of a redex are always redexes of the same rule as their parent. In particular, their patterns must have the same depth. The second axiom is motivated by the fact that reduction of a redex cannot affect any redexes outside it. In particular, every redex at the same depth or less than the reduced redex must have exactly one residual by it, at the same depth as the parent. If a redex is contained in the reduced redex, then the depth of each of its residuals must be at least the depth of the reduced redex, and can fall short of the depth of the parent by at most the pattern-depth of the reduced redex.

3 The compression property

Definition 3.1 A TDRS is α-compressible if for every reduction sequence S of length at most α, there is a sequence S′ of length at most ω with the same initial and final term. Furthermore, if d is a lower bound on the depth of reductions in S, then S′ can be chosen so that d is also such a lower bound on S′.

A TDRS is compressible if it is α-compressible for all α.

Theorem 3.2 If a TDRS is ω + 1-compressible, then it is α-compressible for all α.

Proof. (Taken from the transfinite term rewriting paper.) We prove this by induction on the length of reduction sequences. It is immediate that every system is α-compressible for α ≤ ω.

Suppose the system is α-compressible for some α > ω. Then for any sequence s ^{α+1} [figure] t, there is a sequence s ^{≤ω+1} [figure] t, and hence by hypothesis a sequence s ^{≤ω} [figure] t.

Suppose the system of α-compressible for all α < λ, for some limit ordinal λ > ω. Consider a sequence t_{0} ^{λ} [figure] s in which every step has depth at least d. We shall show how to construct a reduction t_{0} ^{∗} t_{1} ^{≤λ} [figure] s in which every step in the first segment has depth at least d, and every step in the second segment has depth at least d + 1. Iterating this construction gives a reduction t_{0} ^{∗} t_{1} ^{∗} t_{2} ^{∗} … of length at most ω. Since |t_{i}, s| ≤ 2^{−d−i}, the sequence strongly converges to s.

Since t_{0} ^{λ} [figure] s is strongly convergent, it can be split into two parts: t_{0} ^{β} [figure] r ^{λ} [figure] s, such that every reduction in the second part has depth at least d + 1. Since β < λ, we can find a reduction of t_{0} to r of length at most ω, in which every step has depth at least d. This reduction can be split into two parts: t_{0} ^{∗} t_{1} ^{≤ω} r, where every step of the first part has depth at least d, anbd every step of the second has depth at least d + 1. Thus we now have a sequence t_{0} ^{∗} t_{1} ^{≤ω} r λ [figure] s of the required form. □

Theorem 3.3 If a set of redexes has a complete development, it has one of length at most ω.

Proof. Let U be a set of redexes in a term t, having a complete development. We can construct a development of U by reducing at each step some residual of minimal depth. From the axioms it follows that the sequence of depths of reductions is monotonically increasing. If the sequence terminates in finitely many steps, then it is a complete development. If in ω steps its limit tends to infinity, then it is again a complete development. If in ω steps its limit remains finite, then it is not strongly convergent. We will show that if U has a complete development, then the last alternative cannot happen.

[To be continued.] □

Theorem 3.4 Given a reduction sequence t_{0} [figure] t_{1} [figure] t_{2} [figure] ⋯ t_{ω} in which each reduction t_{n} [figure] t_{n+1} is a complete development of a set of redexes U_{n}, there is a reduction of length at most ω from t_{0} to t_{ω}.

Proof. Suppose the minimum depth of any reduction step in the given sequence is d. By strong convergence, for some n every step of the reduction of t_{n} to t_{ω} has depth at least d + 1. For any choice of integers d_{0}, …, d_{n−1}, and each i in 0 … n, the reduction of t_{i} to t_{i+1} can be split into a finite initial segment t_{i} ^{∗} t′_{i}, and a final segment in which every step has depth at least d_{i}.

t_{0}

[figure: t′_{0}; ∗; ≤ ω; t_{1}]

[figure: t′_{1}; ∗; ≤ ω; t_{2}]

[figure: t′_{2}; ∗; ≤ ω; t_{3}]

[figure: t′′_{0}; ∗; ≤ ω; t′′_{1}; ∗; ≤ ω; t′′_{2}; ∗; ≤ ω; t′′_{3} = t′_{3}; ∗; ≤ ω × ω; t_{ω}]

Figure 1: ω × ω-compression

Take d_{n−1} = d, and define t′′_{n−1} = t′_{n−1}. Then for each i from n − 2 down to 0, we efine d_{i}, t′′_{i}, and a finite reduction of t′_{i} to t′′_{i}.

d_{i} is the sum of d_{i+1} and all of the ϵ(u) for u ranging over all the reductions in t_{i+1} ^{∗} t′′_{i+1}.

From the various axioms it should follow [handwaving alert!] that the reduction t′_{i} ^{ω} t_{i+1}

∗ t′_{i+1} can be transformed to t′_{i} ^{∗} t′′_{i} ^{≤ω} t′_{i+1}, such that in the first segment, every reduction has depth at least d, and in the second segment, at least d + 1.

We thus transform the original reduction into t_{0} ^{∗} t′_{0} ^{∗} t′′_{0} ^{≤ω×n} t′_{n} ^{≤ω×ω} t_{ω}, in such a way that every step before t′′_{0} has depth at least d, and every step after has depth at least d + 1. See Figure 1.

By iterating this construction, we obtain a strongly convergent reduction of t_{0} to t_{ω} of length at most ω. □

Theorem 3.5 Every TDRS is ω + 1-compressible.

Proof. Consider a reduction t_{0} ^{ω} t_{ω} t_{ω+1}. Let the final redex u_{ω} have depth d and pattern-depth e. Consoder a final segment t_{n} ^{ω} t_{ω} of the given reduction in which every step has depth at least d + e. Then u_{ω} is the unique residual of a redex u_{n} in t_{n} by this sequence. We can construct the diagram of Figure 2. The theorem follows by applying Theorem 3.4 to the reduction of t′_{n} to t_{ω+1}. □

Putting together these theorems, we obtain:

[figure: t_{0}; ∗; t_{n}; t_{n+1}; t_{n+2}; ⋯; t_{ω}; t′_{n}; ≤ ω; t′_{n+1}; ≤ ω; t′_{n+2}; ⋯; t_{ω+1}; u_{ω}]

Figure 2: ω × ω-compression

Corollary 3.6 Every TDRS is compressible. □

4 Church-Rosser properties

Definition 4.1 A redex u of s is a collapsing redex if there exist a reduction S of s to t, a residual u′ ∈ u/S, a redex v of t, and a residual v′ ∈ v/u′, such that δ(v) > δ(u′) and δ(v′) = δ(u′).

A reduction sequence is non-collapsing if none of its steps reduces a collapsing redex.

A TDRS is non-collapsing if it contains no collapsing redexes.

Definition 4.2 A term t is hyper-collapsing if there is a reduction sequence starting from t of which infinitely many steps are reductions of collapsing redexes at depth zero.

Theorem 4.3 Every set of non-collapsing redexes has a complete development.

Proof. It is sufficient to show that every development of such a set is strongly convergent. Let U be a set of non-collapsing redexes in a term. Consider a development of U of length α, where α is a limit ordinal. Let U_{β} be the set of residuals of U after the first β steps, for each β < α. Let D_{β} be the multiset of depths of redexes in U_{β}. Consider the transformation of D_{β} to D_{β+1}. Suppose this step reduc es a redex at depth d, with pattern-depth e. Each member of D_{β} less than or equal to d produces a single copy of itself in D_{β+1}. Each member with a value d′ > d give rise to some number of copies, each at least the maximum of d + 1 and d′ − e. (The figure of d + 1 follows from the hypotheses about non-collapsing redexes. If collapsing redexes were present, this figure could be d.) The theorem therefore follows from the next theorem about sequences of multisets. □

Theorem 4.4 Let there be given a continuous sequence (D_{β}|β < α) of countable multisets of non-negative integers, where α is a limit ordinal. Assume that D_{0} contains only finitely many occurrences of each integer. Suppose that for β < α, d_{β+1} is derived from D_{β} by deleting an occurrence of some integer d_{β}, and adding any countable multiset of integers greater than d_{β} with only finitely many repetitions of each integer. Suppose that for each limit ordinal β < α, D_{β} = lim_{γ<β} D_{γ}. Then the sequence (d_{β}|β < α) tends to infinity, and lim_{β<α} D_{β} exists.

Proof. Let d be the minimum of {d_{β}|β < α}. Then every step which deletes an occurrence of d reduces the number of occurrences by 1, and no step increases the number of occurrences. Since D_{0} has only finitely many occurrences of d, d can occur only finitely often in the sequence (d_{β}|β < α). Let the last occurrence be d_{γ}. Consider the sequence (D_{β}|β < γ). d + 1 can occur only finitely often in each of these D_{β}, since only when an occurrence of d is removed can the number of its occurrences increase, and then only by a finite amount. By an inductive argument, it follows that every integer occurs only finitely often in each D_{β} for β ≤ γ. In the remainder of the sequence of depths, (d_{β}|γ < β < α), the minimum value is at least d + 1. Thus by another inductive argument, we can conclude that every integer occurs only finitely often in (d_{β}|β < α). Therefore the sequence tends to infinity. From this it is immediate that the sequence of multisets has a limit. □

Theorem 4.5 Every non-collapsing TDRS has the infinitary weak Church-Rosser property (WCR^{∞}). That is, for any two redexes u and v of a term t, their reducts have a common reduct.

Proof. By Theorem 4.3, u/v and v/u have complete developments. Since u · (v/u) and v · (u/v) are both complete developments of {u, v}, by Axiom ?? they must have the same final term. □

Theorem 4.6 (Strip Lemma) In a non-collapsing TDRS, if t ^{u} t′ and t ^{S} [figure] s, then there is a sequence S′ and a term s′ such that s ^{u/S} [figure] s′ and t′ ^{S′} [figure] s′.

Proof. We shall actually prove the slightly stronger statement, where instead of a single step t ^{u} t′, we take an arbitrary complete development t ^{U} [figure] t′.

Represent S as a concatenation of a sequence of complete developments (U_{β}|β < α).

If α = 1, the theorem follows by taking S′ to be a complete develpoment of U_{0}/U.

If α = β + 1, and the theorem holds for concatenations of β complete developments, then the theorem follows from that and the preceding case.

Finally, suppose that α is a limit ordinal, and the theorem holds for concatenations of any number of complete developments less than α. By induction we can construct a sequence S′ which is the concatenation of all the complete developments S_{β}/(U/(U_{0} ⋯ U_{<β})). We must show that this is strongly convergent, and that its limit is the same as the limit of a complete development of U/S.

   [TO BE WRITTEN: proof that it is strongly convergent.]

Choose any depth d ≥ 0. For some β < α, every step of S_{[β,α]} has deph at least d. Therefore |t_{β}, t_{α}| ≤ 2^{−d}. Now consider the developments U_{β} and U_{α}. The respective subsets of these two sets consisting of redexes u with δ(u) + ϵ(u) ≤ d are in 1 − 1 correspondence, by Axiom ??. Let thse

subsets be U′_{β} and U′_{α}. Consider reductions t_{β} ^{U′_{β}} [figure] t′_{β} ^{U_{β}/U′_{β}} [figure] t′′_{β} and t_{α} ^{U′_{α}} [figure] t′_{α} ^{U_{α}/U′_{α}} [figure] t′′_{α}. See Figure ??. |t′_{β}, t′_{α}| is no more than 2^{−levels(U′_{β})}.

   [INCOMPLETE: notion of levels not defined.]

Complete devcelopment of U_{β}/U′_{β} and U_{α}/U′_{α} performs reductions only at a depth of at least [UNK1]. Therefore |t′′_{β}, t′′_{α}| is no more than [UNK2]. Since [UNK2] tends to zero as d tends to infinity, the theorem is proved. □

Theorem 4.7 (Church-Rosser) Every non-collapsing TDRS satisfies CR^{∞}.

Proof. [TO BE WRITTEN: Similar to proof of Strip Lemma, but more complicated.] □

Theorem 4.8 (Strip Lemma) Every TDRS satisfies CR^{∞} for non-collapsing reduction sequences.

Proof. Since every residual of a non-collapsing redex is non-collapsing, the proof of the preceding theorem applies. □

Vague Conjecture 4.9 Every TDRS satisfies the transfinite CR property up to equality of hypercollapsing terms. This is vague because in the abstract setting we have no concept of equality up to some set of terms.

Wild Speculation 4.10 Develop a notion of partial terms. Ter is an ultrametric cpo. Ter as used earlier in this paper would be the set of maximal members of this cpo. Is this useful?

References

[GK93] Glauert J.R.W., Khasidashvili Z. Discrete normalization and standardization in deterministic residual structures. RTA 1993.