The Journal of Functional and Logic Programming

The MIT Press

Volume 1999, Article 1 16 February, 1999

ISSN 1080–5230. MIT Press Journals, Five Cambridge Center, Cambridge, MA 02142-1493, USA; (617)253-2889; journals-orders@mit.edu, journals-info @mit.edu. Published one article at a time in L^{A}TEX source form on the Internet. Pagination varies from copy to copy. For more information and other articles see:

• http://www.cs.tu-berlin.de/journal/jflp/

• http://mitpress.mit.edu/JFLP/

• gopher.mit.edu

• ftp://mitpress.mit.edu/pub/JFLP

\begin{matrix}c \\ ◯ \end{matrix}1999 Massachusetts Institute of Technology. Subscribers are licensed to use journal articles in a variety of ways, limited only as required to ensure fair attribution to authors and the journal, and to prohibit use in a competing commercial product. See the journal’s World Wide Web site for further details. Address inquiries to the Subsidiary Rights Manager, MIT Press Journals; (617)253-2864; journals-rights@mit.edu.

Kennaway et al. Meaningless Terms in Rewriting (Info)

The Journal of Functional and Logic Programming is a peer-reviewed and electronically published scholarly journal that covers a broad scope of topics from functional and logic programming. In particular, it focuses on the integration of the functional and the logic paradigms as well as their common foundations.

Editor-in-Chief: G. Levi

Editorial Board:

H. Aït-Kaci  L. Augustsson
Ch. Brzoska  J. Darlington
Y. Guo  M. Hagiya
M. Hanus  T. Ida
J. Jaffar  B. Jayaraman
M. Köhler^{∗}  A. Krall^{∗}
H. Kuchen^{∗}  J. Launchbury
J. Lloyd  A. Middeldorp
D. Miller  J. J. Moreno-Navarro
L. Naish  M. J. O’Donnell
P. Padawitz  C. Palamidessi
F. Pfenning  D. Plaisted
R. Plasmeijer  U. Reddy
M. Rodríguez-Artalejo F. Silbermann
P. Van Hentenryck  D. S. Warren

∗ Area Editor

Executive Board:

M. M. T. Chakravarty A. Hallmann
H. C. R. Lock  R. Loogen

A. Mück

Electronic Mail: jflp.request@ls5.informatik.uni-dortmund.de

[ii]

Meaningless Terms in Rewriting

Richard Kennaway  Vincent van Oostrom

Fer-Jan de Vries

16 February, 1999

Abstract

We present an axiomatic approach to the concept of meaninglessness in finite and transfinite term rewriting and lambda calculus. We justify our axioms in several ways. They can be intuitively justified from the viewpoint of rewriting as computation. They are shown to imply important properties of meaninglessness: genericity of the class of meaningless terms, confluence modulo equality of meaningless terms, the consistency of equating all meaningless terms, and the construction of Böhm trees and models of rewrite systems. Finally, we show that they can be easily verified for many existing notions of meaninglessness and easily refuted for some notions that are known not to be good characterizations of meaninglessness.

1 Introduction

The concept of a meaningless term in a rewrite system originates with the lambda calculus [Bar84, Bar92]. There exist terms in the lambda calculus that, in certain precisely definable senses, cannot be distinguished from each other and cannot contribute information to any context in which they are placed. Such terms may intuitively be considered meaningless or undefined, and in a denotational semantics they may be mapped to the bottom element of the semantic domain.

In the (pure untyped) lambda calculus, one such class of terms is the set of terms that have no head normal form, that is, those that cannot be reduced to a term of the form λx_{1} … λx_{n}.yM_{1} … M_{k}. Several other classes of terms have also been proposed as formalizing the notion of undefinedness.

1

Kennaway et al. Meaningless Terms in Rewriting §1

In our study of transfinite term rewriting ([KKSdV95]), that is, orthogonal term rewriting in which terms may be infinitely large and rewrite sequences may have any ordinal length, we have encountered a class of terms having similar properties — the so-called hypercollapsing terms. In addition, we have found that the Church–Rosser property of finitary orthogonal term rewrite systems fails for transfinite systems unless these terms are identified with each other. Several other classes of terms are also plausible candidates for notions of meaninglessness.

In this paper we consider the general concept of meaningless terms in a rewrite system. We present axioms that a set of terms in a rewrite system should satisfy to be considered as a reasonable notion of meaninglessness. The axioms can be easily verified for many existing notions; it is sufficient to prove several of their important properties, which in the past have been proved separately. We consider left-linear term rewrite systems and lambda calculus, in both finitary and transfinite forms. We assume the reader to be familiar with the basic theory of term rewriting [DJ90, Klo92] and lambda calculus [Bar84, HS86]. The basic theory of transfinite rewriting has already been set out [KKSdV95, KKSdV97].

We will show the usefulness of our axioms in several ways.

• They arise naturally from the notion of rewriting as computation of the meaning of terms.

• The axioms imply two standard lemmas: the Genericity Lemma and the Consistency Lemma. Genericity states that a meaningless subterm is irrelevant to the computational meaning of the term containing it. Consistency states that adding the rule that all meaningless terms are equal does not give an inconsistent system (one in which all terms are provably equal).

• The axioms allow us to derive the existence and uniqueness of a Böhm normal form for every term, which constitutes a denotational semantics for a term rewrite system or lambda calculus equipped with a notion of meaninglessness. The denotation of a term is simply its unique normal form with respect to “Böhm rewriting”: reduction by the ordinary rewrite rules plus an axiom allowing meaningless subterms to be replaced by a ⊥ symbol.

• The axioms can be checked straightforwardly for many existing notions

of meaninglessness, both for term rewriting systems and lambda calculi. 2

The results in this paper correct and extend results presented in [AKK^{+}94], which deals with term rewriting systems. Our second axiom here was missing from that paper, as observed by the second author of the present paper.

2 Notations

A position, also called an occurrence, is a finite sequence of positive integers. ϵ denotes the empty sequence. Given a position u and a term t, the subterm t|u, when it exists, is defined by t|ϵ = t, and F (t_{1}, …, t_{n})|(i · u) = t_{i}|u (if i ≤ n). There is a natural prefix ordering on positions, and two positions are said to be disjoint if neither is a prefix of the other.

We write s → t for a single reduction step, s →^{∗} t for a finite reduction sequence, and s → → t for a reduction of any ordinal length, finite or infinite. (Infinitely long reductions will be formalized in Section 6.)

A context is a term in which the “hole” symbol, [ ], may appear (any number of times). We write C[ ] to denote an arbitrary context, and C[t] to denote the result of replacing every occurrence of the hole by t. The hole behaves in effect like a variable symbol, but it is convenient to distinguish the two notions. In lambda calculus, the substitution of t for the hole symbol is assumed to involve renaming of bound variables as necessary to prevent variable capture. (Note that this is distinct from definitions of context substitution that are used in some other places, where the substitution is purely textual and allows capture of variables.)

Let U be a set of terms. s →^{U}_{A} t holds if A is a set of pairwise disjoint positions of subterms of s in U, and t can be obtained from s by replacing those subterms by arbitrary terms.

s ↔^{U}_{A} t holds if t can be obtained from s by replacing some set A of pairwise disjoint subterms of s in U by terms of U.

We write s →^{U} t or s ↔^{U} t if we do not wish to mention A.

=^{U} is the transitive closure of ↔^{U}.

s ⟶^{in U} t denotes a reduction of s to t of one step, which reduces a redex

inside some subterm s′ of s, where s′ ∈ U. s ⟶^{∗}^{in U} t and s ⟶ ⟶^{in U} t are reductions composed of ⟶^{in U}-steps, finitely many or arbitrarily many, respectively.

s ⟶^{out U} t is a one-step reduction that reduces a redex not contained in any

subterm of s in U. We similarly define s ⟶^{∗}^{out U} t and s ⟶ ⟶^{out U} t.

3

Kennaway et al. Meaningless Terms in Rewriting §3.1

Juxtaposition of relation symbols denotes relational composition. Reversing a relational symbol denotes the inverse relation.

Given an equivalence relation ≈ on the terms of a rewrite system, the reduction relation is said to be confluent up to ≈ if s ← ←→ → t implies s → → ≈ ← ← t. It is said to be confluent modulo ≈ if s ← ←≈→ → t implies s → → ≈ ← ← t. The reduction relation is said to be confluent up to (resp. modulo) U if it is confluent up to (resp. modulo) =^{U}.

Confluence modulo U is the more natural concept to define, but our main theorems only require the weaker notion of confluence up to U.

3 Axioms and properties of notions of meaninglessness

3.1 The axioms

Let U be a set of terms of some rewrite system. There are five axioms that we may require U to satisfy, to be considered as a notion of meaninglessness.

From the point of view of rewriting as the computation of meaning, if a term is meaningless, then so should be every term that it reduces to. This is our first axiom.

Axiom 1 (Closure) U is closed under rewriting.

Our second axiom expresses the idea that a meaningless term cannot convey any information when looked at “from outside.” For example, Print(t) might be intended to reduce to some sort of printable representation of t. In order for this to happen, t must be reducible to a term that can be patternmatched from outside, that is, a term that can be overlapped by a redex. If t is meaningless, it should not be possible to extract information from t in this way; therefore, whenever such a t is overlapped by a redex, that redex should also be meaningless.

For term rewriting, this motivation justifies our restriction to left-linear systems. Non-left-linear systems are capable of performing a test of syntactic identity on any two terms whatever. In such systems, every term may contribute information to its context, and no term could be considered meaningless.

4 Definition 1 Let t be a redex, i.e., an instance σ(l) of the left-hand side l of some rewrite rule. The redex t overlaps its subterm at position u if u is a non-empty position of l and l | u is not a variable.

As an example, consider the term Head(Cons(A, B)) and the rule mentioned above. The redex at ϵ overlaps the subterm at 1, but does not overlap any other subterm. Notice that if a redex overlaps a subterm that is also a redex, the two redexes conflict — in general, if the inner redex is reduced, the outer redex will no longer be a redex. The orthogonal term rewrite systems are those in which no redex can overlap a redex.

Axiom 2 (Overlap) If a redex t overlaps a subterm in U, then t ∈ U.

This axiom can be stated for the lambda calculus in more concrete terms: it means that if λx.t is in U, then so is (λx.t)t′ for any t′.

The axiom can be related to Knuth–Bendix completion. If we have a rule that rewrites any member of U to the undefined symbol ⊥, then a redex that overlaps a subterm in U is an example of a conflict between that rule and the rule for the redex. The conflict is resolved if the redex itself is also in U.

For the lambda calculus, we will require that the set of meaningless terms is closed under substitution. This is because when a term is reduced, its subterms are not simply copied to give subterms of the result, but may be instantiated as well. For example, in lambda calculus, we have reductions such as (λx.xx)(λy.y) → (λy.y)(λy.y), in which the subterm xx becomes instantiated to (λy.y)(λy.y). A subterm that is meaningless should not become meaningful by this process. This condition is not required in our study of term rewriting, as variables in terms behave more like constant symbols and are never instantiated by rewriting.

Axiom 3 (Substitution) U is closed under substitution.

For transfinite rewriting, some of our results require that the set of meaningless terms contains all the hypercollapsing terms or all the root-active terms.

Definition 2 A term t is root-active if every reduct of t can be reduced to a redex. R is the set of root-active terms.

A term rewrite rule is collapsing if for every reduction by the rule, the reduct is a descendant of a subterm of the redex. A collapsing redex is a redex of a collapsing rule.

5

A term is hypercollapsing if each of its reducts reduces to a collapsing redex. H is the set of hypercollapsing terms.

We have phrased the definition of a collapsing rule in such a way that it can be applied both to term rewrite systems and lambda calculus. For term rewriting, the definition of a collapsing rule is equivalent to the following: a collapsing rule is one whose right-hand side is a variable. For example, the rules Head(Cons(x, y)) → x and I(x) → x are collapsing, but F (A) → A is not. For lambda calculus, the definition implies that beta reduction is collapsing. The definition also makes sense for higher-order rewriting (see e.g., [vO94]), but that is beyond the scope of this paper.

An example of a root-active term is the term A, given the rule A → A. Less trivially, consider the rules Last(Cons(x, y)) → Last(y) and Ones → Cons(1, Ones). For these rules, the term Last(Ones) is root-active. Neither of these terms is hypercollapsing. A contrived example of a hypercollapsing term is the term A, with the rules A → B(A) and B(x) → x. The latter rule is a collapsing rule, and every reduct of A in this system is reducible to a redex of that rule. In the lambda calculus, an example of a root-active term is Y I, where Y = λf.(λx.f(xx))(λx.f(xx)) and I = λx.x. Every reduct of Y I can be reduced to a term of the form IM for some M, which has a redex at the root.

Computation on a root-active term never reaches even a partial final result since further computation at the root of the term can always take place. Therefore, all such terms can reasonably be regarded as meaningless. Technically, we only need to assume that they are all in U in order to obtain the existence of Böhm normal forms.

Hypercollapsing terms are a special case of root-active terms. They resemble infinite applications of an identity operator. Every hypercollapsing term can be reduced to a term of the form C_{0}[C_{1}[C_{2}[…]]], where each C_{i}[x] is the left-hand side of a rule whose right-hand side is x. Their technical significance is that it is exactly these terms that cause the Church–Rosser property to fail in orthogonal transfinite rewrite systems. If they are all identified with each other, the Church–Rosser property is restored. We use this in proving the uniqueness of Böhm trees in orthogonal rewrite systems, and the Consistency property, which says that one may consistently identify all meaningless terms with each other, without introducing any “unwanted” equalities.

6 Axiom 4

1. (Hypercollapse) H ⊆ U.

2. (Root-active) R ⊆ U.

Since all hypercollapsing terms are root-active, Axiom 4(2) implies Axiom 4(1).

Beta reduction is a collapsing rule, so all redexes of lambda calculus are collapsing redexes, and the class of hypercollapsing terms is the same as the class of root-active terms. Therefore, the two versions of Axiom 4 need not be distinguished for lambda calculus.

The fifth axiom expresses that the meaningfulness of a term does not depend on the identity of its meaningless subterms. This is quite similar to the Genericity property, but not identical to it. We use this axiom in proving the uniqueness of Böhm trees.

Axiom 5 (Indiscernability) If s ↔^{U} t, then s ∈ U if and only if t ∈ U.

3.2 Related notions

Given a class of meaningless terms U, what terms can we say are definitely meaningful? Some terms not in U may reduce to terms in U, so we cannot say that every term outside U is meaningful. Very often, it is reasonable to regard every normal form as meaningful. However, one approach to the semantics of run-time type errors or domain errors is to regard terms such as 1/0 or factorial(−1) as valid terms, but “erroneous.” If division is not defined for a zero denominator, and factorial is not defined for negative integers, then these terms are normal forms, but not meaningful. Instead, we can define a notion of being “definitely meaningful” purely in terms of U.

Definition 3 A term is totally meaningful if none of its reducts contains any subterm in U.

Intuitively, meaningless terms should be computationally irrelevant. This is captured formally by the property of Genericity.

Definition 4 Suppose that for every term s in U and every context C[ ], if C[s] reduces to a totally meaningful term t, then C[r] reduces to t for every r. Then U is called a generic set.

7

An example of a generic set in the lambda calculus is the set of terms having no head normal form. (See [Bar84], Theorem 14.3.24 for a proof of this.) The set of terms having no normal form is not generic. This is demonstrated by the fixed-point operator Y = λf.(λx.f(xx))(λx.f(xx)) and the context C[ ] = [ ](λy.z). Y has no normal form, the term C[Y] has normal form z, but C[w] does not reduce to z.

Genericity is usually defined in terms of conversion to normal form C[r] (→ → ∪ ← ←)^{∗} t instead of reduction to totally meaningful form C[r] → → t. This is always done in the context of confluent rewriting systems with each subterm of a normal form being meaningful. In that context, the two notions coincide. Stating it in the ‘rewrite’ form has the advantage of making sense for non-confluent rewriting systems as well, as remarked by Mizuhito Ogawa (in personal communication).

Definition 5 A rewriting system is called consistent if there exist two normal forms that are not related by (→ → ∪ ← ←)^{∗}.

For a set of terms U, it is called U-consistent if there exist two totally meaningful terms (with respect to U) that are not related by (→ → ∪ ← ← ∪ =^{U})^{∗}.

The system is relatively consistent with respect to U if, for all totally meaningful terms s and t, s(→ → ∪ ← ← ∪ =^{U})^{∗}t implies s(→ → ∪ ← ←)^{∗}t.

4 Finite-term rewriting

In this section, only finitary TRSs are considered. That is, all terms are finite and all reduction sequences are finitely long. There is no limit on the number of symbols or rules in a rewrite system.

We first prove some general lemmas.

Lemma 1 ↔^{U} is transitive if and only if Axiom 5 holds.

Proof of Lemma 1 Assume Axiom 5. Suppose r ↔^{U}_{A} s ↔^{U}_{B} t. Let C be the set of minimal elements of A ∪ B. Then by Axiom 5, r ↔^{U}_{C} t.

Now suppose that ↔^{U} is transitive, s ↔^{U} t, and s ∈ U. Let r be a member of U containing no proper subterm in U. Then r ↔^{U} s ↔^{U} t, so by transitivity, r ↔^{U} t. But the choice of r implies that t ∈ U. Therefore, ↔^{U} is transitive.

Proof of Lemma 1 □

8 Example 1 Consider terms constructed from nullary A and B, and unary F. Let U consist of every term except F (A). We have F (A) ↔^{U} F (B) ↔^{U} A,

but not F (A) ↔^{U} A.

Lemma 2

1. Suppose U satisfies Axiom 2. If s ←^{U} s′ ⟶ ⟶^{out U} t, then for some t′,

s → → t′ ←^{U} t.

2. Suppose U satisfies Axiom 2. If s ↔^{U} s′ ⟶ ⟶^{out U} t, then for some t′,

s → → t′ ↔^{U} t.

3. Suppose U satisfies Axiom 2. If s =^{U} s′ ⟶ ⟶^{out U} t, then for some t′,

s → → t′ =^{U} t.

4. Suppose U satisfies Axioms 1 and 2. If s ⟶ ⟶^{in U} s′ ⟶ ⟶^{out U} t, then for some

t′, s ⟶ ⟶^{out U} t′ ⟶ ⟶^{in U} t.

Proof of Lemma 2

1. Let s ←^{U} s′ by substitution at positions A of s′. Let A′ be the set of residuals of A by s′ ⟶ ⟶^{out U} t. No step of s′ ⟶ ⟶^{out U} t can happen inside any residual of the subterms of s′ at positions in A, nor, by Axiom 2, can it overlap any of them. These residuals, being identical to their ancestors, are in U. Therefore, starting from s instead of s′, the same sequence of reductions can be performed at the same positions, giving a term t′ differing from t by substituting terms for the subterms of t at A′.

2. The second part is proved similarly. Note that we cannot conclude that s ⟶ ⟶^{out U} t′ unless Axiom 5 also holds.

3. Immediate from the preceding item.

4. Suppose s ⟶ ⟶^{in U} s′ ⟶ ⟶^{out U} t. Let A be the set of positions of maximal subterms of s′ in U. Axiom 1 implies that each step of s ⟶ ⟶^{in U} s′ takes place at a position of which some member of A is a prefix. By Axiom 2, the reduction s′ ⟶ ⟶^{out U} t can only reduce redexes that are outside and do not overlap any residual of A. This reduction can therefore be performed on s, to give a reduction s ⟶ ⟶^{out U} t′. Let A′ be the set of

9 residuals of A in t′ by this reduction. The reduction s ⟶ ⟶^{in U} s′ is an interleaving of ⟶ ⟶^{in U}-reductions on the subterms of s′ at positions in A. By performing the same reductions on the subterms of t′ at positions in A′ we obtain a ⟶ ⟶^{in U}-reduction of t′ to t.

Proof of Lemma 2 □

Lemma 3 Suppose U satisfies Axioms 1 and 2. If s → → t then for some r,

s ⟶ ⟶^{out U} r ⟶ ⟶^{in U} t.

Proof of Lemma 3 The given reduction can be expressed as an alternation of ⟶ ⟶^{out U} and ⟶ ⟶^{in U} segments. A finite number of applications of Lemma 2(4) suffice to move all ⟶^{in U} steps to the end of the sequence.

Proof of Lemma 3 □

Lemma 4 Suppose U satisfies Axioms 1 and 2. If s → → t and t is totally meaningful, then s ⟶ ⟶^{out U} t.

Proof of Lemma 4 This follows from Lemma 3 since, by Axiom 1, if r ⟶ ⟶^{in U} t and t is totally meaningful, then r = t.

Proof of Lemma 4 □

Lemma 5 Suppose U satisfies Axioms 1 and 2. If s =^{U} s′ → → t, and t is totally meaningful, then s → → t.

Proof of Lemma 5 Assume Axioms 1 and 2, and that s =^{U} s′ → → t. By Lemma 4, s′ ⟶ ⟶^{out U} t. By Lemma 2, s → → t′ =^{U} t. Since t is totally meaningful, t′ = t.

Proof of Lemma 5 □

Lemma 6 Suppose U satisfies Axiom 1. Then ⟶ ⟶^{in U} is a subrelation of =^{U}.

Proof of Lemma 6 Suppose that s ⟶^{in U} t by reducing a redex contained in an undefined subterm at position u. By Axiom 1, s ↔^{U}_{{u}} t. Therefore, for a finite reduction s ⟶ ⟶^{in U} t, s =^{U} t.

Proof of Lemma 6 □

10 Lemma 7 Suppose U satisfies Axioms 1 and 2. If s =^{U} r → → t, then for

some q, s → → q =^{U} t.

Proof of Lemma 7 Assume Axioms 1 and 2 hold. By transitivity of =^{U}, it is sufficient to prove the lemma from the hypothesis that s ↔^{U} r → → t. By Lemma 3, we have s ↔^{U} r ⟶ ⟶^{out U} t′ ⟶ ⟶^{in U} t. By Lemma 2(2), this implies s → → r′ ↔^{U} t′. By Axiom 1 and Lemma 6, r′ =^{U} t.

Proof of Lemma 7 □

4.1 Genericity

The Genericity Lemma formalizes our intuition that meaningless terms are computationally irrelevant.

Lemma 8 (Genericity) In a left-linear term rewrite system, every set U satisfying Axioms 1 and 2 is generic.

Proof of Lemma 8 Suppose that C[ ] is a context, s ∈ U, t is totally meaningful, and C[s] → → t. By Axioms 1 and 2 and Lemma 4, C[s] ⟶ ⟶^{out U} t. For any term r, C[s] →^{U} C[r]. By Axiom 2 and Lemma 2(1), C[r] → → t′ ←^{U} t. Since t is totally meaningful, t = t′. Therefore, U is generic.

Proof of Lemma 8 □

We remark that the axioms we gave in [AKK^{+}94] do not suffice for genericity, as is demonstrated by the example of the rule F (A) → B and the set U = {A}. This satisfies the axioms of that paper, but U is not generic. F (A) reduces to the totally meaningful term B, but F (B) does not reduce to B.

The axioms here are sufficient but not necessary, as demonstrated by the following examples.

Example 2

• The rules {A → B, B → B} and the set U = {A}. U is generic, and satisfies Axiom 2 but not Axiom 1.

• The rules {G(A) → B, G(x) → B} and the set U = {A}. U is generic, and satisfies Axiom 1 but not Axiom 2.

11

[figure: • = U  •; 1; ..............; • ====== U  •  2  •; ..............; 3; ..............; ..............; • ====== U  •]

Figure 1: Diagram for the proof of Lemma 9

These are deliberately contrived counterexamples. The axioms are satisfied by many notions of meaninglessness occurring in the literature. In many cases in Section 8, an example showing failure of an axiom can be used directly to show failure of genericity.

4.2 Confluence and consistency

Lemma 9 (Confluence) In an orthogonal term rewrite system, if U satisfies Axioms 1 and 2 then the system is confluent modulo U.

Proof of Lemma 9 See Figure 1. (1) and (3) are given by Lemma 7. (2) is given by confluence of finite orthogonal term rewrite systems.

Proof of Lemma 9 □

Lemma 10 In a left-linear term rewrite system, suppose that U satisfies Axioms 1 and 2, and the rewrite system is confluent up to U. Then the system is relatively consistent with respect to U.

Proof of Lemma 10 Consider a proof of equality of two totally meaningful terms s_{0} and s_{n}. It takes the form of a deduction s_{0}R_{1}s_{1}R_{2} … R_{n}s_{n}, where each relation R_{i} is either a reduction sequence (forwards or backwards) or an instance of =^{U}.

12 Consider the leftmost occurrence in the proof of either =^{U} or ← ←→ →. If the former is leftmost, then the proof must begin with s_{0} =^{U} s_{1}, s_{0} → →

s_{1} =^{U} s_{2} or s_{0} ← ← s_{1} =^{U} s_{2}. The first two are impossible because s_{0} is totally meaningful. The third implies, by Lemma 5 and total meaningfulness of s_{0}, that s_{0} ← ← s_{2}.

If ← ←→ → occurs to the left of all occurrences of U, then the proof must begin s_{0} ← ← s_{1} → → s_{2} or s_{0} → → s_{1} ← ← s_{2} → → s_{3}. By confluence up to U, this can be transformed into s_{0} → → =^{U} ← ← …, and then by the previous case into s_{0} → →← ← . . ..

Therefore, if the proof contains any occurrences of =^{U} or ← ←→ →, the leftmost can be removed without introducing any new such segments. Therefore, all of them can be removed. The result is a proof of equality of s_{0} and s_{n} of the form s_{0} → →← ← s_{n}, which is a proof in the original system.

Proof of Lemma 10 □

Corollary 1 (Relative consistency) In an orthogonal term rewrite system, suppose that U satisfies Axioms 1 and 2. Then the system is relatively consistent with respect to U.

Proof of Corollary 1 Since orthogonal systems are confluent, they are confluent up to any set U. The corollary is then immediate from Lemma 10.

Proof of Corollary 1 □

5 Finite lambda calculus

Our results for finitary lambda calculus with beta reduction are rather similar to the above, but with the addition of an extra hypothesis on U, Axiom 3. With this axiom, the proofs of Lemmas 2, 3, 4, and 5 carry over to the lambda calculus, and the Genericity property follows immediately.

Lemma 11 (Genericity) In finitary lambda calculus, every set U satisfying Axioms 1, 2, and 3 is generic.

Lemma 12 (Relative consistency) Suppose that U satisfies Axioms 1, 2, and 3. Then the system is relatively consistent with respect to U.

13 Proof of Lemma 12 The lambda calculus is left-linear and confluent and, therefore, confluent up to U for any U. Thus, the other hypotheses of Lemma 10 hold. The proof proceeds as for that lemma.

Proof of Lemma 12 □

6 Transfinite rewriting

6.1 Basic concepts

The basic concepts of transfinite term rewriting and lambda calculus have already been set out [KKSdV95, KKSdV97]. (Although the title of the former paper appears to restrict it to orthogonal systems, its basic definitions and some of its results apply to left-linear systems.) We shall very briefly state the fundamental definitions and two basic theorems.

The infinite terms may be obtained by defining a metric on the space of finite terms and taking the metric closure. The metric defines the distance between non-identical terms s and t to be 2^{−d} where d is the depth of the shortest position at which they differ^{1}. The metric completion adds terms such as Cons(1, Cons(2, Cons(3, …))) or A(A(A(…, …), A(…, …)), A(A(…, …), A(…, …))). A reduction step is defined as in the finite case. We require that the left-hand side of a rewrite rule be a finite term, but the right-hand side may be infinite.

Transfinite rewrite sequences may be of any ordinal length, finite or infinite. For a review of the basic definitions of ordinal numbers, see [Phi92].

A transfinite rewrite sequence of length α, an ordinal number, consists of a sequence of terms ( t_{β} | 0 ≤ β ≤ α), and for each β < α a reduction step t_{β} → t_{β+1}. An open transfinite rewrite sequence is defined similarly, except that if α is a limit ordinal, there is no term t_{α}.

Given such a sequence, let the reduction t_{β} → t_{β+1} be performed at position u_{β}, with depth d_{β}. The sequence is strongly continuous if for every limit ordinal λ < α, d_{β} tends to infinity as β tends to λ from below. If α is not a limit ordinal, or if it is and the above condition on depths is satisfied also for λ = α, then the sequence is strongly convergent.

14

1Readers familiar with [KKSdV97] should note that for brevity, we only discuss Λ^{111} in this paper. Our results also apply to Λ^{001} and Λ^{101} — see the discussion of abc-active terms in Section 8.1.2.

There is a standard topology on the class of ordinals, called the order topology, in which a basis for the open sets is the class of intervals { γ | α ≤ γ < β } for all α and β. Every strongly continuous (resp. convergent) sequence is continuous (resp. convergent) with respect to this topology on ordinals and the metric on the space of finite and infinite terms.

We consider only strongly convergent reductions. All reductions mentioned are either proved or implicitly assumed to be strongly convergent.

For transfinite rewriting, the definitions of →^{U}_{A} and ↔^{U}_{A} in Section 2 apply verbatim. This implies that the set A can be infinite. However, the transitive closure =^{U} is for both finite and infinite rewriting the union of all finite compositions of the relation ↔^{U}. We do not define any notion of an infinite composition of relations.

Sequences of length greater than ω may seem to lack computational meaning, but their existence cannot be avoided. As soon as we allow ourselves to take the limit of an infinite reduction sequence, there is the possibility of the limit term containing redexes, and hence of the construction of sequences longer than ω. Furthermore, the usual “tiling” method of constructing the projection of one sequence over another will, in general, build sequences of lengths much greater than ω. Fortunately, such sequences need not lose computational motivation, because of the Compression Lemma:

Lemma 13 (Compression) [KKSdV95, KKSdV97] For left-linear TRSs and for lambda calculus, for any ordinal α, if t reduces to s by a reduction of length α, then t reduces to s by a reduction of length at most ω.

The main difference with finite rewriting is that infinitary confluence (confluence of → →) is not implied by orthogonality. The canonical counterexample is given by the rules A(x) → x and B(x) → x and the term A(B(A(B(…)))), which reduces to both A(A(A(…))) and B(B(B(…))), each of which reduces only to itself. The only obstacle to confluence lies with the hypercollapsing terms. All of the terms in the example are hypercollapsing.

Lemma 14 ([KKSdV95], Theorem 7.4, [KKSdV97], Theorem 57) Transfinite orthogonal TRSs and lambda calculus are confluent up to H.

For lambda calculus, Theorem 57 of [KKSdV97] in fact proves confluence modulo H. [KKSdV95] omits to do this for term rewriting, but our results later imply that transfinite orthogonal TRSs are in fact confluent modulo H.

15 Corollary 2 Transfinite orthogonal TRSs and lambda calculus are confluent up to any U satisfying Axiom 4(1).

6.2 Basic properties

We now establish, for transfinite left-linear term rewriting, counterparts of the lemmas we proved for finite rewriting, and counterexamples where the lemmas do not extend.

Lemma 15 If Axiom 5 holds, then ↔^{U} is transitive.

Proof of Lemma 15 The proof in Lemma 1 is still valid for this direction of the implication.

Proof of Lemma 15 □

The proof in Lemma 1 of the reverse implication is not valid. The choice of r as “a member of U containing no proper subterm in U” may not be possible, for example, if U is the set of all infinite terms.

Lemma 16 Lemma 2 holds for transfinite term rewriting.

Proof of Lemma 16 The proof requires little more than the original proof of Lemma 2. We need only note that in each of the four parts, each step of the given sequence s′ ⟶ ⟶^{out U} t is at the same position as the corresponding step of the constructed sequence s → → t′. This establishes that it is strongly convergent. From that it follows that the set A associated with the substitution of subterms of s′ has a set of residuals A′ in t. In part (4), strong convergence of t′ ⟶ ⟶^{in U} t follows from the fact that it is an interleaving of disjoint copies of strongly convergent reductions of subterms of s.

Proof of Lemma 16 □

Lemma 17 Lemma 3 holds for transfinite term rewriting.

Proof of Lemma 17 Suppose U satisfies Axioms 1 and 2. Let s → → t. By the Compression property, this reduction can be assumed to have length at most ω. It can then be expressed as an alternation of at most ω many ⟶ ⟶^{out U} and ⟶ ⟶^{in U} segments. Our aim is to construct the diagram of Figure 2, in which the zig-zag path from s to t down the lower edge of the figure is

16

[figure: s; •; •; •; …; r; •; ∗; •; •; •; …; •; •; ∗; •; •; …; •; •; ∗; •; …; •; ⋮  ⋮; t]

Figure 2: Diagram for the proof of Lemma 17

the given sequence, and where every horizontal sequence is ⟶ ⟶^{out U} and every vertical sequence is ⟶ ⟶^{in U}. Each square of the diagram can be constructed by Lemma 16(4). To construct the right edge, the reduction of r to t, we must show that each of the horizontal sequences is strongly convergent, and that their limits can be joined by suitable vertical segments whose concatenation will strongly converge to t.

From the construction of Lemma 16(4), each step of each horizontal sequence of the diagram is at the same depth as the corresponding horizontal step in the zig-zag. Since by hypothesis the latter is strongly convergent, so is the former.

Each segment of the right edge exists by the same argument as used in Lemma 16(4).

Finally, we prove strong convergence of the whole right edge. Choose any depth d. By strong convergence of the given sequence, there is an n such that every step of the zig-zag after the nth ⟶ ⟶^{out U} segment has depth greater than d. Therefore, every step of the top row after the nth segment has depth greater than d, as do all the horizontal segments below those. Therefore, every segment of the right edge after the nth is the projection of one sequence of depth greater than d over another and, therefore, has depth

17 greater than d. Therefore, the right edge is strongly convergent.

Furthermore, after n segments, the terms of the right edge are within a distance of 2^{−d} of the corresponding terms of the zig-zag. Therefore, the right edge has the same limit as the given sequence, t.

Proof of Lemma 17 □

Lemma 18 Lemma 4 holds for transfinite term rewriting.

Proof of Lemma 18 This follows from Lemma 17 in the same way as Lemma 4 followed from Lemma 3.

Proof of Lemma 18 □

Lemma 19 Lemma 5 holds for transfinite term rewriting.

Proof of Lemma 19 The proof is as for Lemma 5, using Lemmas 18 and 16 instead.

Proof of Lemma 19 □

Lemma 20 Suppose U satisfies Axiom 1. Then ⟶^{∗}^{in U} is a subrelation of =^{U}. If Axiom 5 holds, then ⟶ ⟶^{in U} is a subrelation of ↔^{U}.

Proof of Lemma 20 For the first part, the proof is as for Lemma 6.

For the second part, assume Axioms 1 and 5, and suppose s ⟶ ⟶^{in U} t. Let A be the set of positions of maximal subterms of s in U. Suppose that some step of the sequence is performed at a position of which no member of A is a prefix. There must be a first such step s′ ⟶^{in U} t′. Let its position be u. Since this is a ⟶^{in U}-reduction, s′|u ∈ U. Since all previous steps are within subterms at positions in A, Axiom 1 implies that s′|u ↔^{U} s|u. By Axiom 5, s|u ∈ U. But this implies that some member of A is a prefix of u, contrary to the choice of u. Therefore, the entire reduction of s to t happens within the subterms at positions in A. By Axiom 1, those subterms of t are also in

U, and s ↔^{U} t.

Proof of Lemma 20 □

18

Unlike the finite case, Axiom 5 is necessary. Without it, there is a counterexample to ⟶ ⟶^{in U} being a subrelation of =^{U}. Take a nullary symbol A, a unary symbol F, and a binary symbol B. Let there be a rule F (A) → A. Let U = {F (A), A}. U satisfies every axiom except Axiom 5. Consider the infinite term s = B(A, B(F (A), B(F (F (A)), B(F (F (F (A))), …)))). This rewrites by ⟶ ⟶^{in U} to t = B(A, B(A, B(A, B(A, …)))). But s and t are not related by =^{U}.

Lemma 21 Suppose U satisfies Axioms 1 and 2. If s =^{U} r →^{∗} t, then for

some q, s →^{∗} q =^{U} t.

If Axiom 5 also holds, then if s =^{U} r → → t, then for some q, s → → q =^{U} t.

Proof of Lemma 21 The proof is as for Lemma 7, using Lemmas 17, 16, and 20 (where the extra hypothesis of Axiom 5 is needed).

Proof of Lemma 21 □

6.3 Genericity, confluence and consistency for transfinite term rewriting

With the lemmas just proved, the proofs of genericity and consistency for finite term rewriting carry over exactly to the transfinite case.

Lemma 22 (Transfinite Genericity) In a left-linear transfinite term rewrite system, every set U satisfying Axioms 1 and 2 is generic.

Lemma 23 (Confluence) In an orthogonal term rewrite system, if U satisfies Axioms 1, 2, 4(1), and 5, then the system is confluent modulo U.

Proof of Lemma 23 See Figure 3. (1) and (3) are given by Axioms 1, 2, and 5, and Lemma 21. (2) is given by Axiom 4(1) and Lemma 14.

Proof of Lemma 23 □

In a transfinite TRS, U can satisfy every axiom except Axiom 5, and the system can fail to be confluent modulo U. For an example, take U = {A, F (A), B} and rules A → F (A) and C(x) → D(x, C(x)).

The terms F (A) and F (B) show that Axiom 5 is false. We have F (A) ↔^{U} F (B), F (A) ∈ U, but F (B) ∉ U. All the other axioms are satisfied.

19

[figure: • = U  •; 1; ..............; • ====== U  •  2  •; 3; •; . . . . . . . . . . . . . . . .; ====== U; •; . . . . . . . . . . . . . . . .; ============= U; •; . . . . . . . . . . . . . . . .]

Figure 3: Diagram for the proof of Lemma 23

s = C(B) ↔^{U} C(A) → → D(A, D(F (A), D(F (F (A)), …))) = t, but there is no term t′ such that s → → t′ =^{U} t. Therefore, the system is not confluent modulo U.

Lemma 24 Suppose U satisfies Axioms 1 and 2 and the rewrite system is confluent up to U. Then the system is relatively consistent with respect to U.

Corollary 3 (Transfinite relative consistency) In an orthogonal transfinite term rewrite system, suppose that U satisfies Axioms 1, 2 and 4(1). Then the system is relatively consistent with respect to U.

Proof of Corollary 3 From Corollary 2 and Lemma 14.

Proof of Corollary 3 □

6.4 Genericity, confluence, and consistency for transfinite lambda calculus

For transfinite lambda calculus, the Genericity, Confluence, and Consistency Lemmas carry over by taking the union of the axioms required for the cases of finite lambda calculus and transfinite term rewriting.

Thus, with the additional hypothesis of Axiom 3, transfinite lambda calculus satisfies the lemmas of Section 6.2. We conclude that with Axiom 3 it satisfies Lemma 11, and with Axioms 3 and 4, it satisfies Lemma 12.

20

7 Böhm trees

In lambda calculus we have the notion of a Böhm tree [Bar84]. This is a possibly infinite lambda term in normal form that may also contain the constant ⊥, which represents undefinedness. We can generalise this concept to other rewrite systems, and show that, given suitable constraints on the notion of undefinedness, the Böhm trees relative to that notion form a semantic domain for the rewrite system, and that the computation of the ‘value’ of a term consists of computing its normal form in a transfinite extension of the rewrite system. For terms to have unique Böhm trees, confluence up to U is required, so we will only consider orthogonal TRSs in this section. As Böhm terms are closely connected with transfinite rewriting, we also consider only transfinite rewrite systems.

Definition 6 The Böhm terms are obtained by adjoining the nullary function symbol ⊥ to a rewrite system. Böhm terms are partially ordered by stipulating that ⊥≤ s for every term s, and that all the term-forming operations are monotonic.

The set of Böhm terms is an algebraic domain in which the order-finite terms are the finite Böhm terms. The maximal elements of the domain are the terms not containing ⊥, i.e., the original terms of the system.

There is a natural way of extending a set U of terms of the original system to a set of Böhm terms.

Definition 7 If t is a Böhm term, a ⊥-instance of t is a term t′ that can be obtained from t by replacing every occurrence of ⊥ by a term in U. (Different occurrences of ⊥ may be replaced by different terms.)

Definition 8 U_{⊥} is the set of Böhm terms having a ⊥-instance in U.

The following lemma makes U_{⊥} easier to work with.

Lemma 25 Let U satisfy Axiom 5. If some ⊥-instance of t is in U, then every ⊥-instance is.

For each of Axioms 1–5, if U satisfies that axiom, then so does U_{⊥}.

Proof of Lemma 25 Let t′ and t′′ be ⊥-instances of t. t′ and t′′ differ only by substitution of subterms in U. By Axiom 5, t′ ∈ U if and only if t′′ ∈ U.

21

For the second part, we prove Axiom 2 as an example. Proofs for the others are equally simple. Let t ∈ U_{⊥}, and let C[t] be a redex whose pattern includes the root of t. Let t′ ∈ U result from a substitution of members of U for ⊥ in t. Let C′[ ] result from C[ ] by making some substitution of members of U for occurrences of ⊥. Then C′[t′] is a redex whose pattern overlaps the root of t′. By Axiom 2 for U, C′[t′] ∈ U. Therefore, C[t] ∈ U_{⊥}.

Proof of Lemma 25 □

Definition 9 Böhm reduction is reduction by the rules of the system together with the ⊥-rule: t →⊥ if t is not ⊥ and t ∈ U_{⊥}. We write →_{B} for a Böhm reduction step, and →_{⊥} for a reduction by the ⊥-rule.

A Böhm normal form or Böhm tree (e.g., a set U) is a term that is in normal form with respect to Böhm reduction.

Theorem 1 If U satisfies Axiom 4(2), then every term has at least one Böhm normal form.

Proof of Theorem 1 Let t be a term. If t is not root-active, it is reducible to a root-stable term t′. Apply the same argument recursively to the immediate subterms of t′. This gives a strongly convergent reduction sequence, ending with a term t′′ having the property that every redex is contained in a root-active subterm. By Axiom 4(2), these subterms are all in U. Hence, if all the outermost redexes by the ⊥-rule in t′′ are reduced, the result is a Böhm normal form.

Proof of Theorem 1 □

Lemma 26 Let U satisfy Axiom 5. Then the ⊥-rule is transfinitely Church– Rosser, and if s =^{U_{⊥}} t, then s and t have a common reduct by → →_{⊥}.

Proof of Lemma 26 Suppose that p reduces to q by the ⊥-rule. It follows from Axiom 5 that if every outermost subterm of p and q is replaced by ⊥, the results must be identical. Therefore, if p is ⊥-reducible to q_{0} and q_{1}, then q_{0} and q_{1} reduce to the same term by outermost ⊥-reduction. That is, the ⊥-rule is transfinitely Church–Rosser.

If s →^{U_{⊥}} t, then it is clear that s and t have a common reduct by ⊥- reduction. Therefore, if s =^{U_{⊥}} t, then s and t are convertible by ⊥-reduction. By the first part of the lemma, they have a common reduct by → →_{⊥}.

Proof of Lemma 26 □

22 Lemma 27 If s → →_{B} t, then s → →→ →_{⊥} t, provided that, in the case of lambda calculus, U satisfies Axiom 3.

Proof of Lemma 27 Let the steps of s → →_{B} t be s_{β} →_{B} s_{β+1}, where s = s_{0} and t = s_{α}.

Define a new sequence by transfinite induction thus.

Base case: s′_{0} = s_{0}.

Successor case: Suppose s′_{β} has been defined. If s_{β} →_{B} s_{β+1} is a ⊥- reduction, define s′_{β+1} = s′_{β}. Otherwise, let it be a reduction by a rewrite rule applied at position u. Define s′_{β} → s′_{β+1} by reduction at u.

Limit case: If s′_{β} has been defined for all β less than a limit ordinal λ, define s′_{λ} to be the limit of the sequence.

To prove that this defines a reduction sequence, we must show that in the successor case, s′_{β} has a redex at u, and in the limit case, the limit s′_{λ} exists. We will also need to know that for all β, s′_{β} → →_{⊥} s_{β}. These can be proved simultaneously by induction. Clearly, if s′_{β} → →_{⊥} s_{β} and s_{β} → s_{β+1}, then s′_{β} has a redex everywhere that s_{β} does (which requires Axiom 3 in the case of lambda calculus), and s′_{β+1} → →_{⊥} s_{β+1}. Since s′_{β} → s′_{β+1} takes place at the same place as s_{β} → s_{β+1}, the constructed sequence is strongly convergent, and, therefore, s′_{λ} exists.

This also shows that s′_{α} → →_{⊥} s_{α} = t.

Proof of Lemma 27 □

Theorem 2 Let U satisfy Axioms 1, 2, 4(2), and 5 (and 3 in the case of lambda calculus). Then Böhm reduction has the transfinite Church–Rosser property.

Proof of Theorem 2 See Figure 4. We are given Böhm reductions from s to t_{0} and t_{1}. By Axiom 4(2) and Theorem 1 we can extend these to reach Böhm normal forms u_{0} and u_{1}. Squares 1 and 3 in the figure are given by Lemma 27 (requiring Axiom 3 in the case of lambda calculus).

The ⊥-reductions of v_{0} and v_{1} to u_{0} and u_{1} can be performed by replacement of the maximal undefined subterms of v_{0} and v_{1} by ⊥. Let these be at sets of positions A_{0} and A_{1}, respectively.

23

[figure: s; B; B; t_{0}  1  v_{0}  2  v_{1}  3  t_{1}; ⊥; ⊥; u_{0}; B; w_{0}; = H; w_{1}; u_{1}; B]

Figure 4: Proof of CR^{∞} for Böhm reduction

By Lemma 14, v_{0} and v_{1} are reducible (by ordinary reduction) to terms w_{0} and w_{1}, which are related by =^{H} and hence, by Axiom 4(1), by =^{U_{⊥}}. This gives the pentagon 2.

v_{0} and v_{1} contain no redexes outside subterms at A_{0} and A_{1}. Axiom 5 implies that no (ordinary) reduction of v_{0} or v_{1} can create any redexes outside those subterms. Therefore, the reductions of v_{0} and v_{1} to w_{0} and w_{1} lie entirely inside them. By Axiom 1, v_{0} ↔^{U_{⊥}} w_{0} and v_{1} ↔^{U_{⊥}} w_{1}.

The ⊥-reductions of v_{0} and v_{1} to u_{0} and u_{1} can be performed by replacing every subterm in A_{0} and A_{1} by ⊥. Therefore, v_{0} ↔^{U_{⊥}} u_{0} and v_{1} ↔^{U_{⊥}} u_{1}.

Putting these together, we find that u_{0} =^{U_{⊥}} u_{1}. By Axiom 5 and Lemma 15, ↔^{U_{⊥}} is transitive, therefore u_{0} ↔^{U_{⊥}} u_{1}. Since u_{0} and u_{1} are Böhm normal forms, this implies that u_{0} = u_{1}.

Proof of Theorem 2 □

Corollary 4 Under the same hypotheses, every term has a unique Böhm tree.

The Böhm tree of a term can be considered to be its meaning in the domain of Böhm trees. Thus any set of terms U satisfying the axioms gives a denotational semantics for the rewrite system, where the meaning of a term is its normal form with respect to transfinite Böhm reduction.

24

Kennaway et al. Meaningless Terms in Rewriting §8.1.2

8 Sets of meaningless terms

8.1 Sets of meaningless terms in term rewriting

We now check our axioms for some sets of first-order terms that seem intuitively good candidates. These include all the examples in [AKK^{+}94]. Although our genericity theorems apply to all left-linear TRSs, most of the following notions are only defined for orthogonal TRSs.

8.1.1 False, True

The empty set and the set of all terms (i.e., the predicates ‘false’ and ‘true’ on terms) satisfy all the axioms, except that the empty set fails Axiom 4(1) or Axiom 4(2) if there are any hypercollapsing or root-active terms, respectively. Hence, they satisfy the Genericity and (with the same exception) the Consistency Lemmas. Note that the Consistency Lemma is vacuous when U is the set of all terms, since there are then no totally meaningful terms.

8.1.2 Has no normal form/Has an infinite rewrite

In general, neither the set of terms without normal form nor the set of terms having an infinite rewrite is generic, even for orthogonal systems. The former violates Axiom 2 for the rules {A → A, G(H(x)) → B}. The term H(A) has no normal form, but replacing H(A) by B in G(H(A)) changes the normal form of the latter term from B to G(B). The set of terms having an infinite rewrite violates Axiom 1, as is shown by the system {A → A, B(x) → C}. B(A) has an infinite rewrite, but its reduct C does not.

However, for finitary orthogonal non-erasing TRSs — that is, where every variable occurring on the left of a rule also occurs on the right of that rule (cf. [Klo92, p. 75]) — the two classes coincide and are generic. Axiom 4(2) holds, since root-active terms have no normal form. Axiom 5 holds because in a non-erasing system, if a subterm of a term has no normal form, then neither does the whole term.

In the transfinite case, the natural analogues of these concepts are the class of terms having no normal form (by transfinite reduction) and the class of terms having an infinite non-strongly convergent rewrite. These two classes do not coincide, even in non-erasing systems, as demonstrated by the rules {A → A, G(H(x)) → J(G(H(x)))}. H(A) does not have a normal form.

25 G(H(A)) has the normal form J(J(J(…))) (the troublesome subterm H(A) is “pushed into infinity”). As a result, neither class is generic.

We can strengthen the concept of non-erasingness for transfinite systems, by calling a system transfinitely non-erasing if for any reduction t → → t′, every subterm of t has at least one residual in t′. For transfinitely non-erasing TRSs, the property of having an infinite rewrite is once more equivalent to the property of having no normal form. (However, unlike non-erasingness, transfinite non-erasingness is not a decidable property.) For such TRSs, this class of terms satisfies Axioms 1, 2, 4(2), and 5, and so the genericity and consistency lemmas hold, and there is a Böhm model. An example of the distinction is given by the rule A(x) → B(A(x)). This rule is non-erasing, but an infinite reduction from the term A(C) gives the term B(B(B(…))), which contains no residual of the subterm C. Therefore it is not transfinitely non-erasing.

8.1.3 Opaque

This is a concept that applies to orthogonal rewrite systems. A closed term is opaque if no term reachable from it is overlapped by any redex^{2}. A general term is opaque if every closed instance is opaque.

In an orthogonal system, every root-active term is opaque, but in general there may be more opaque terms, and it is even possible for the class to include some normal forms. An example is Head(Nil), given only the rule Head(Cons(x, y)) → x.

Axiom 1 holds by definition in the finitary case, and the infinitary version then follows from the fact that left-hand sides of rules are finite. Axiom 2 is trivially true, since a proper subterm overlapping with a redex is not opaque. Axiom 4(2) is immediate from orthogonality. To prove Axiom 5, suppose that s ↔^{U} t and that s is not opaque. Then s → → q for some term q that is overlapped by a redex. Since this property of q depends only on some finite prefix of q, it follows (from the Compressing Lemma 13 and the finiteness of the left-hand side of a rule) that there is a finitely long reduction of s to some term q′ having the same property. From Lemma 21 we have t → → q′ =^{U} q. By Axiom 2, q′ must also be overlapped by a redex; therefore, t is not opaque.

26 8.1.4 ω-undefined

2In [AKK^{+}94] the definition of opaqueness is stated erroneously, but this was the concept intended.

A finite term is ω-undefined if all terms reachable from it can be decomposed into ‘redex compatible’ parts [Klo92, Def. 3.3.15]. We add a nullary symbol ω, and define a partial ordering on terms containing ω by stipulating that ω ≤ t for all t, and that all function symbols are monotonic. Say that a term t (which may contain ω) is a partial redex if t ≤ t′ for some redex t′. Define the ω-rule: t → ω if t is a partial redex other than ω. It is easy to show that every finite term t has a unique normal form ω(t) by this rule. For an infinite term t, define ω(t) to be the least upper bound of ω(t′) for all finite terms t′ < t. A term t is ω-undefined if for every reduct t′ (by the ordinary rewrite rules of the system) of every instance of t, ω(t′) = ω.

It is clear that every root-active term is ω-undefined. There are many other ω-undefined terms. For example, given the rule Head(Cons(x, y)) → x, Head(t) will be ω-undefined whenever t is. The infinite term Head(Head( Head(…))) is also ω-undefined (even though it is a normal form).

Axiom 2 is immediate. Axiom 1 is immediate in the finitary case and is simple to prove in the transfinite case. Axiom 4(2) follows from orthogonality. To prove Axiom 5, suppose that s and t are ω-undefined, and C[s] is not. Then some instance C[s][x := r] = C[x := r][s[x := r]] is reducible to a term q for which ω(q) ≠ ω. Since this property of q is determined by some finite prefix of q, there is a finite reduction C[s][x := r] to some q′ for which ω(q′) ≠ ω, by the same argument as for the case of opaque terms. C[x := r][s[x := r]] =^{U} C[x := r][t[x := r]] = C[t][x := r]; therefore, from Lemma 21 it follows that for some q′′, C[x := r][t[x := r]] → → q′′ =^{U} q′. This implies that ω(q′′) ≠ ω, and hence that C[t] is not ω-undefined.

8.1.5 Hypercollapsing, root-active

If U is the set of hypercollapsing terms or the set of root-active terms in an orthogonal term rewrite system, then Axiom 1 holds since by the parallel moves lemma, projecting an infinite rewrite over finitely many steps can erase only finitely many root-reductions. Axiom 2 holds by orthogonality. Axiom 4(1) is true for both, and Axiom 4(2) for the root-active terms, by definition. Axiom 5 follows by an argument similar to the cases of opaqueness and ω-undefinedness.

For non-orthogonal systems the genericity lemma fails, as witnessed by {A(x) → x, B(x) → x, G(A(x)) → C}. The hypercollapsing terms are all

27 terms of the form f_{0}(f_{1}(f_{2}(…))), where each f_{i} is A or B. G(A^{ω}) reduces to the totally meaningful term C, but G(B^{ω}) does not. Clearly, Axiom 2 is false.

8.2 Sets of meaningless lambda terms

The axioms are easily checked for many known notions of meaninglessness in lambda calculus. Some other classes known not to be good notions of meaninglessness violate one or more of the axioms.

8.2.1 Has no normal form/Has an infinite rewrite

As for the case of TRSs, neither the class of terms having no normal form nor the class of terms having an infinite rewrite is generic. When lambda terms are restricted such that each abstracted variable occurs at least once in the body of the lambda term (Church’s λI-calculus [Chu41]), then the two classes coincide and are generic, by an argument similar to the one for non-erasing orthogonal TRSs.

In the transfinite λI-calculus this does not hold, because of the same phenomenon of ‘pushing to infinity’ that we saw for transfinite TRSs. Let Ω =_{def} (λx.xx)(λx.xx) and Y = λf.(λx.f(xx))(λx.f(xx)). Then the function part of the redex (λy.yxΩ)Y does not have a normal form, but the whole redex transfinitely reduces to the infinite normal form x(x(x(…))).

8.2.2 Non-simply typable λ-terms

The set of non-simply typable λ-terms is not generic. For example, the term (λx.xx)I reduces to the totally meaningful term I, but if its non-typable subterm λx.xx is replaced by λx.λy.yx, the whole term reduces to the totally meaningful term λy.yI. All the axioms hold except for Axiom 1, as the nonsimply typable terms are clearly not closed under reduction (even in the λI-calculus).

8.2.3 ΩM

For any n ≥ 0, the set Ω_{n} of terms of the form ΩM_{1} … M_{n} satisfies all the axioms except Axiom 4(1). Each of these classes is therefore generic and consistent but does not give a Böhm model.

28 8.2.4 Zero terms

A zero term [Bar92] is a term that cannot be reduced to an abstraction. The terms, all of whose instances are zero terms, are the opaque terms of lambda calculus. These are easily shown to satisfy Axioms 1, 2, 3 and 4(2).

To prove Axiom 5, the argument is similar to the way this was proved for notions of undefinedness in TRSs. Suppose that every instance of s and t is a zero term, but some instance of C[s] is not, say, C[s][x := r] = C[x := r][s[x := r]]. Then C[x := r][s[x := r]] reduces to an abstraction λy.r and, therefore, does so in finitely many steps. By the lambda-calculus equivalent of Lemma 21, C[x := r][t[x := r]] is reducible to a term q such that λy.r =^{U} q. Since abstractions are not zero terms, q must be an abstraction. Therefore C[x := r][t[x := r]] is not a zero term, and C[t] is not in the class of meaningless terms.

8.2.5 Easy terms

t is an easy term if for every closed term s, the λβ-calculus plus the equation t = s is consistent [JZ85]. It is immediate that Axiom 1 holds for the class of easy terms. Axiom 3 holds, since t[x := r] = s follows from t = s if s is closed. To prove Axiom 4(2), suppose that t is root-active and s is closed, and that adding the axiom t = s allows a proof of K = I (where K = λx.λy.x and I = λx.x). By confluence of beta reduction, such a proof must exist that begins with a series of beta-expansions on K, then uses the axiom t = s to replace some instance of t (or more generally, some reduct of some instance) by s, and then continues with more proof steps ending with I. Consider that use of the axiom and the beta expansion preceding it. We have r ←_{β} C[t′] = C[s]. If the beta reduction takes place within t′, then we can go from r to C[s] by a single application of the axiom. If it takes place outside t′, then the redex is also present in C[s], and we can get from r to C[s] by first applying the axiom t = s to each residual of t′ in r, and then beta-expanding to s. The redex cannot overlap t′, since a reduct of an instance of a root-active term cannot be an abstraction. Therefore, in all cases, the first application of the axiom in a proof of K = I can be moved closer to the beginning. But the first step in such a proof cannot be an application of the axiom, since K contains no easy subterms. To check Axiom 2, we must show that if an abstraction λx.t is easy, then so is (λx.t)s for any s. (λx.t)s = r follows from t[x := s] = r. But t[x := s] is easy;

29 therefore, so is (λx.t)s. We do not know the status of Axiom 5.

8.2.6 Unusable

Consider the lambda calculus λδ with δ-rules of [Kup94, Sec. 7.2] and [Kup95]. Define the notion of strict context thus: The empty context [ ] is a strict context, and if C[ ] is a strict context, then so are C[ ]s, λx.C[ ] and F C[ ], for any term s, variable x, and constant F. Then, a term s is usable if C[s] has a normal form for some strict context C[ ]. Axiom 1 holds by definition and confluence. Axiom 2 for λδ-redexes holds because this amounts to showing that if s is unusable, then st is unusable, which follows directly from the definition of strict context. Axiom 3 holds because if s[x := t] is usable, then (λx.s)t is, and by the definition of strict context, so is s. Axiom 4(2) holds since the unusable terms include the unsolvables, and root-active terms are unsolvable. Axiom 5 is proved as before.

8.2.7 abc-active

(cf. [KKSdV97]) Given a string of three binary digits abc, there is a measure D^{abc}(s, ϕ) of length of a position ϕ of a term s:

D^{abc}(s, ϵ) =^{def} 0
D^{abc}(λx.s, 0ϕ) =^{def} a + D^{abc}(s, ϕ)
D^{abc}(st, 0ϕ) =^{def} b + D^{abc}(s, ϕ)
D^{abc}(st, 1ϕ) =^{def} c + D^{abc}(t, ϕ)

Any of these measures can be used instead of the usual “syntactic” measure of depth of a subterm (which is D^{111}), to give seven different versions of infinitary lambda calculus, plus the finitary lambda calculus as the case D^{000}.

A term is (abc-)stable if it cannot be reduced to a term having a redex at abc-depth 0. It is (abc-)active if it cannot be reduced to a abc-stable term. Three particular instances of these abstract concepts are well-known: 111-active is just another formulation of root-active, the 001-stable terms are exactly the terms having a head normal form, and the 101-stable terms are exactly the terms having a weak head normal form. For all depth measures, Axioms 1 and 2 are immediate from the definitions. For depth measures 001, 101, and 111, the other axioms all hold. For all the other measures, at least one of them fails. (Detailed proofs for each axiom and depth measure are

Kennaway et al. Meaningless Terms in Rewriting §Appendix

30 given in the appendix.) From this we conclude that Genericity, Consistency, and the existence and uniqueness of Böhm trees hold for the measures 001, 101, and 111, for both finite and transfinite lambda calculus. This confirms the conclusion of [KKSdV97] that these are the only measures that yield well-behaved versions of infinitary lambda calculus.

8.2.8 Unsolvable/ω-undefined/001-active

A lambda term s is solvable [Bar84] if there exist tuples \overline{x} of variables and \overline{t} of terms such that (λ\overline{x}.s)\overline{t} → → I. Taking the same definition of ω-undefinedness as for TRSs, it is not difficult to check that the unsolvable terms coincide with the ω-undefined ones. It is well known that the unsolvable terms are exactly the terms without head normal form. This implies that unsolvability is equivalent to 001-active, treated above. Hence all axioms hold.

8.2.9 Strongly unsolvable/101-active

A term is strongly unsolvable [Ong88, Sec. 2.1.1–2] if it is a zero term and it is not convertible to a term of the form x\overline{s}. That is, it has no weak head normal form, or equivalently it is a 101-active form, treated above. Hence all axioms hold.

8.2.10 Mute/hypercollapsing/root-active/111-active

A term is mute if it is a zero term that cannot be reduced to a variable or to an application of a zero term to any term [Ber]. This definition is equivalent to the properties of being hypercollapsing or being root-active, which in turn are equivalent to 111-activeness. All axioms hold.

9 Acknowledgments

We thank Jan Kuper, Mizuhito Ogawa, and Femke van Raamsdonk for useful discussions, Zena Ariola, Jan Willem Klop, and Ronan Sleep for their earlier collaboration, and Stefan Kahrs and the anonymous referees for their detailed comments.

31

Appendix abc-active terms in transfinite lambda calculus

Theorem 3 In transfinite lambda calculus, Axiom 2 holds for all measures except 0∗0 (i.e., 000 and 010). Axiom 3 is false for ∗∗0, and true for ∗∗1. Axiom 5 is false for ∗∗0 and 011, and true for 001, 101, and 111.

Proof of Theorem 3 Axiom 2 is false for 0∗0 (i.e., 000 and 010). A counterexample is the term (λx.xΩ)(KI). λx.xΩ is 0∗0-active, but the whole term reduces to the normal form I. It is true for 1∗∗, since λx.s cannot be 1∗∗-active. The remaining depth measures are 0∗1. For these we argue thus: if (λx.s)t is reducible to a 0∗1-stable term, then so is s[x := t]. By Axiom 3 (proved below), this implies that s is also.

Axiom 3 is false for ∗∗0. A counterexample is xΩ. This is ∗∗0-active, but its instance KIΩ is not. The axiom is true for ∗∗1. Let s be ∗∗1-active, and consider any reduction d of s[x := t] to a term r. We must prove that r is reducible to a redex. The proof is rather tedious^{3}, and it is summarized in Figure 5. We split the reduction into two segments: first a reduction e′ of s[x := t] to a term r′ = r′′[x := t], which performs reductions only outside the copies of t, followed by a reduction f′ of r′ to r, which performs reductions only within subterms of the form tp_{0} … p_{n}.

For each term s_{i} in the reduction of s[x := t] to r, we construct a set of positions A_{i} and a term s′_{i}. A_{0} is the set of positions of maximal subterms of s[x := t] of the form x\overline{p}. s′_{0} is s. Given s′_{k} and A_{k}, let u be the position of the reduction from s_{k} to s_{k+1}. If u is inside a member of A_{k}, then take A_{k+1} = A_{k} and s′_{k+1} = s′_{k}. If u is outside every member of A_{k}, then s′_{k} is obtained by reducing s′_{k} at u. For each residual v of each member of A_{k} by this reduction, take the minimal position v′ such that s′_{k}|v is at the bottom end of a left-branching chain of applications whose top end is at v′. (If the chain is empty, then, of course, v′ = v.) The minimal elements of the set of all such v′ for the set A_{k+1}.

Let r′′ be the final term in the sequence of terms s′_{k}, and A the corresponding set of positions of s′. We thus have a reduction e of s to r′′ and a reduction e′ of s[x := t] to r′ = r′′[x := t], such that r′ is reducible to r by a reduction f′ operating only within the subterms at A.

Kennaway et al. Meaningless Terms in Rewriting (Ref)

32 [figure: s; e; r′′; g; p′′; r′′[x := t] ≡ r′; g′; p′′[x := t] ≡ p′; e′; f′; s[x := t]; d; r; •]

3There does not exist a syntactic characterisation of the 011- or 111-stable terms, making proofs like [Bar84, Cor. 11.4.8] impossible.

Figure 5: Axiom 3 for **1 depth in lambda calculus

By Axiom 1, r′′ is ∗∗1-active. Therefore, there is a reduction g of r′′ to a term p′′ having a redex at zero ∗∗1-depth. This gives a reduction g′ of r′ to the term p′ = p′′[x := t], which also contains a redex at zero ∗∗1-depth. Since every redex of r′′ below positions in A is in a subterm of the form x\overline{p}, and x is free in r′′, no residual of any such redex can be at zero ∗∗1-depth in the reduction to p′′. The reduction f′ reduces only redexes within the subterms at A. Therefore, the canonical projection of f′ over g′ preserves the redex at depth zero of p′. Thus the canonical projection of g′ over f′ reduces r to a term having a redex at zero ∗∗1-depth, a contradiction.

Axiom 5 is false for ∗∗0, by the same counterexample as Axiom 3. xΩ and Ω are both ∗∗0-active, but in the context (λx.[ ])(KI), only the second yields a ∗∗0-active term. A counterexample for 011 is given by the terms (λx.Ω)y and Ωy. These differ by substitution of λx.Ω for Ω, both of which are 011-active, but (λx.Ω)y is 011-active and Ωy is not. For the other three ∗∗1 measures, the usual argument based on Lemma 21 goes through, since Axioms 1, 2, and 3 all hold, and when a term is reducible to abc-stable form, it is so reducible in finitely many steps.

Proof of Theorem 3 □

These results establish the positive parts of the following theorem, and the counterexamples given above also demonstrate the negative parts.

Theorem 4 The Genericity and Consistency properties hold for ∗∗1- and fail for ∗∗0-active terms. The unique existence of the Böhm normal form holds for the 111-, 101-, and 001-active terms, and fails for the other depth measures.

33 Acknowledgment of support: Richard Kennaway was supported by an EPSRC Advanced Fellowship and by EPSRC grant no. GR/F 91582. Vincent van Oostrom’s work work was mostly performed at NTT Basic Research Laboratories, Atsugi, Japan, and supported by an HCM grant at Institut für Informatik, Technische Universität München, Germany. Fer-Jan de Vries’s work was partially performed at Hitachi Advanced Research Laboratory, Hatoyama, Saitama 350-03, Japan.

References

[AKK^{+}94] Z. M. Ariola, J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries. Syntactic definitions of undefined: On defining the undefined. In International Symposium on Theoretical Aspects of Computer Software, Sendai, volume 789 of Lecture Notes in Computer Science, pages 543–554, Berlin, 1994. Springer-Verlag.

[Bar84] H. P. Barendregt. The Lambda Calculus, Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. Elsevier Science Publishers B.V., Amsterdam, revised edition, 1984.

[Bar92] H. P. Barendregt. Representing ‘undefined’ in lambda calculus. Journal of Functional Programming, 2(3):367–374, July 1992.

[Ber] A. Berarducci. Infinite λ-calculus and non-sensible models. Presented to the conference in honour of Roberto Magari, Siena 1994.

[Chu41] A. Church. The Calculi of Lambda Conversion. Princeton University Press, Princeton, NJ, 1941.

[DJ90] N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In [?, Ch. 6 pp. 243–320], 1990.

[HS86] J. R. Hindley and J. P. Seldin. Introduction to Combinators and λ-Calculus, volume 1 of London Mathematical Society Students Texts. Cambridge University Press, Cambridge, 1986.

[JZ85] J. G. Jacopini and M. Venturini Zilli. Easy terms in the lambda

calculus. Fundamenta Informaticae, VIII, 1985. 34 [KKSdV95] J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries.

Transfinite reductions in orthogonal term rewriting systems. Information and Computation, 119:18–38, 1995.

[KKSdV97] J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries. Infinitary lambda calculus. Theoretical Computer Science, 175(1):93–125, 1997.

[Klo92] J. W. Klop. Term rewriting systems. In [?, vol. 2, pp. 1–116], 1992.

[Kup94] J. Kuper. Partiality in Logic and Computation, Aspects of Undefinedness. PhD thesis, Universiteit Twente, February 1994.

[Kup95] J. Kuper. Proving the Genericity Lemma by leftmost reduction is simple. In Proceedings of the Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Computer Science, pages 271–278, Berlin, 1995. Springer-Verlag.

[Ong88] C.-H. L. Ong. The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming. PhD thesis, Imperial College of Science and Technology, University of London, May 1988.

[Phi92] I. C. C. Phillips. Recursion theory. In [?, vol. 1, pp. 79–188], 1992.

[vO94] V. van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, March 1994.

35