Relative Normalization in Deterministic Residual Structures

John Glauert and Zurab Khasidashvili School of Information Systems University of East Anglia Norwich NR4 7TJ England jrwg@sys.uea.ac.uk, zurab@sys.uea.ac.uk ^{∗}

Submitted to ASCS’95

Abstract This paper generalizes the Huet&Lévy theory of normalization by neededness to an abstract setting. We define Stable Deterministic Residual Structures (SDRS) and Family Structures by axiomatizing some properties of the residual relation and the family relation on redexes in an Abstract Rewriting System. We present two proofs of the Relative Normalization Theorem, one for SDRSs for regular stable sets, and another for DRSs for all stable sets of desirable ‘normal forms’. We further prove the Relative Optimality Theorem for Family Structures.

1 Introduction

A normalizable term, in a rewriting system, may have an infinite reduction, so it is important to have a normalizing strategy which enables one to construct reductions to normal form. It is well known that the leftmost-outermost strategy is normalizing in the λ-calculus.

For Orthogonal Term Rewriting Systems (OTRSs), a general normalizing strategy, called the needed strategy, was found by Huet and Lévy in [HuLé91]. The needed strategy always contracts a needed redex – a redex whose residual is to be contracted in any reduction to normal form. Huet and Lévy showed that any term t not in normal form has a needed redex, and that repeated contraction of needed redexes in t leads to its normal form whenever there is one.

Barendregt et al. [BKKS87] generalized the concept of neededness to the λ-calculus. They studied neededness not only w.r.t. normal forms, but also w.r.t. head-normal forms – a redex is head-needed if its residuals are contracted in each reduction to a head-normal form. They proved correctness of the two needed strategies for computing normal forms and head-normal forms, respectively. In [Mar92], Maranget studied a strategy that computes a weak head-normal form of a term in an OTRS. Normalization w.r.t. another interesting set of ‘normal forms’, that of constructor head-normal forms in constructor OTRSs, is studied by Nöcker [Nök94].

In [GlKh94], the present authors address the question of normalization relative to a desired set of final terms, considering the properties that a set of terms must possess in order for the neededness theory of Huet and Lévy still to make sense. This work is done in the context of orthogonal Expression Reduction Systems (OERS) [Kha92], a form of higher-order rewriting which subsumes Term Rewriting and the λ-calculus. They introduce the notion of neededness w.r.t. a set of reductions Π or a set of terms S. Natural conditions are imposed on S, called stability, that are necessary and sufficient for the following Relative Normalization theorem to hold: each S-normalizable term not in S (not in S-normal form) has at least one S-needed redex, and repeated contraction of S-needed redexes in a term t will lead to an S-normal form of t whenever there is one.

∗This work was supported by the Engineering and Physical Sciences Research Council of Great Britain under grant GR/H41300

Each existing notion of neededness can be given by specifying Π or S. For example, Huet&Lévyneededness is neededness w.r.t. the set of normal forms, Maranget-neededness [Mar92] is neededness w.r.t. all fair reductions, head-neededness is neededness w.r.t. the set of head-normal forms, etc. It is shown also that if a stable S is regular, i.e., if S-unneeded redexes cannot duplicate S-needed ones, then the S-needed strategy is hypernormalizing as well.

In this paper, we further generalize the Huet&Lévy theory, by abstracting from the structure of terms. We study relative normalization in Deterministic Residual Structures (DRSs). DRSs are Abstract Reduction Systems (ARSs), which consist of a set of objects t, s, …, often called terms, and labelled transitions t→^{u}s between objects, where u is a label. Each transition is uniquely labelled. If t→^{u}s and t→^{u}s′, then s = s′. Transitions between the same source and target terms may have different labels. When t→^{u}s, u is said to be a redex of t, reduction of which gives s. A reduction is a sequence of transitions.

A DRS is an ARS which has a residual relation between redexes in the source and target terms of each transition. Redexes of t may be erased by reduction of u, new redexes may be introduced in s, while other redexes of s are considered residuals of redexes in t, as specified by the residual relation. Further, the residual relation is generalized to all reductions, and permutationequivalence on reductions, referred to below as Lévy-equivalence, and the embedding relation, which induces a partial ordering on the reduction space, is introduced, as is done for the λ-calculus in [Lév78, Lév80]. Sufficient conditions needed to define the above concepts in an abstract setting were stated in Gonthier et al. [GLM92] as axiom 0.

Our paper is very close in spirit to [GLM92], where several axioms are imposed on the residual relation making it possible to define an abstract notion of standard reduction and prove an Abstract Standardization Theorem of which the Standardization Theorems in the λ-calculus, orthogonal TRSs [HuLé91] and left-normal CRSs [Klo80] are special cases. The way standardization is understood in that paper requires a nesting relation on redexes in a term, and some axioms giving its important properties. Standard reductions then become some kind of outside-in reductions.

In our Deterministic Residual Structures, we do not introduce a nesting relation on redexes, but are still able to prove the Relative Normalization theorem for all regular stable sets S. We show moreover that the S-needed strategy is hypernormalizing. We only use a modified stability axiom from [GLM92], due to Berry [Ber79]. We show that without the latter axiom the Relative Normalization theorem fails. The method employed to prove the Relative Normalization theorem is similar to that in [Kha88], and is based on the fact that S-needed steps can be pushed before Sunneeded steps, in any reduction, without affecting the number of S-needed steps. The important difference is that in [Kha88] we made heavy use of the notion of descendant of subterms – a refinement of the residual notion for redexes – both in the proofs and in the definition of an alternative notion of neededness – essentiality.

Since for irregular stable S, S-unneeded redexes can duplicate S-needed ones, the above proof method does not work; for the same reason, the S-needed strategy is not hypernormalizing any more. Therefore, to prove Relative Normalization for irregular stable S, we define the Family Structure (FS) as a DRS with a very liberal notion of family relation [Lév78, Lév80] and a contribution relation on families, expressing the notion of (at least one member of) a family to be needed to create another family. For FSs, the proof of the Relative Normalization theorem for all stable S from [GlKh94] works perfectly.

We show that FSs are DRSs that satisfy Berry’s stability axiom, so the previous Relative Normalization theorem (for stable DRSs) is subsumed by this one; however the previous Relative Normalization theorem is also useful since checking for Berry’s stability is much simpler than constructing a sound family relation. For example, it is well known that the λ-calculus [Lév78, Lév80], orthogonal TRSs [Mar], Interaction Systems [AsLa93], and orthogonal CRSs (and ERSs) [Klo80, KeSl89] form FSs, hence stable DRSs. For other higher-order rewriting systems, such as HRSs [Nip93] and HORSs [Oos94, OR94], which do form stable DRSs, to our knowledge, it is not yet known if they form FSs too (though it is very likely that the latter is the case).

For FSs we show that a strategy that only contracts, in an arbitrary order, redexes that belong to S-needed families but which need not be S-needed themselves, is still S-normalizing. As a corollary, any S-needed complete family-reduction, which contracts all members of a family containing an Sneeded redex in a multi-step, is S-normalizing. Similarly to [Lév80], we show that the latter reductions are optimal in the sense that they reach S in the least number of family-reduction steps.

In the next section, we introduce stable DRSs and give some examples. In Section 3, we prove the Relative Normalization theorem for regular stable sets S in an SDRS R, and demonstrate that if S or R is not stable, then the theorem fails. In Section 4, we introduce Family Structures, show that they are stable DRSs, and prove the Relative Normalization theorem for all stable S. Finally, In Section 5, we strengthen the latter result, and prove the Relative Optimality theorem for any FS. Conclusions appear in Section 6.

2 Deterministic Residual Structures

In this section we define Deterministic Residual Structures (DRSs) which are Abstract Reduction Systems (ARSs) satisfying certain properties concerning residuals. The definition and some results about ARSs can be found e.g., in [Klo92]. Our definition is slightly different. An ARS is a twosorted set of objects: the set Ter of terms (ranged over by t, s, o, e) and the set Red of redexes (ranged over by u, v, w), with a partial function →: T er × Red → T er such that for any t ∈ T er there are only a finite number of u ∈ Red such that → (t, u) = s, (written t→^{u}s). A reduction is a sequence t→^{u_{1}}t_{2}→^{u_{2}} . . .. Reductions are denoted by P, Q, N. We write P : t → → s or t → →^{P} s if P denotes a reduction (sequence) from t to s. ∅_{t} denotes the empty reduction starting from t. P u denotes a redex u in the final term ft(P) of P. |P | denotes the length of P. u also denotes the reduction that contracts u. We use F, G to denote sets of redex-occurrences in a term.

DRSs are very similar to Stark’s Determinate Concurrent Transition Systems [Sta89], to Abstract Reduction Systems of [GLM92], and to van Oostrom’s Descendant Rewriting Systems [Oos94]. The main difference from DCTSs is that Stark considers a non-duplicating residual relation. The difference from ARSs of [GLM92] is that we do not have the nesting relation on redexes and the corresponding axioms (but we still have a restricted tool to express the notion of one redex controlling another), and the stability axiom is modified accordingly. The difference from van Oostrom’s DRSs is that in the latter the notion of descendant of any subterm/position of a term is formalized,

[figure: •; v; •; •; u; v/u; •; u/v]

Figure 1: An Elementary Diagram

not only the notion of residual of redexes. We choose Klop’s way of defining DRSs via commutative diagrams because it is intuitively clear and useful in proofs. Klop’s method of constructing diagrams is well described in [Klo80, Bar84].

Definition 2.1 (1) (Deterministic Residual Structure) A Deterministic Residual Structure (DRS) is an Abstract Reduction System R with a residual relation on redexes; and relations + (concatenation), / (residual), ⊔ (square sum), ⊴ (Lévy embedding), ≈_{L} (Lévy-equivalence or permutation-equivalence) on reductions; such that

(a) If t→^{u}s ∈ R and v ⊆ t, then the set v/u of residuals of v under u is a set of redexes of s, where a redex in s may be a residual of only one redex in t under u, and u/u = ∅. The set of residuals of a redex under any reduction is defined by transitivity. A redex of s which is not a residual of any v ⊆ t under u is said to be u-new or created by u.

(b) A development of a set F of redexes in a term t is a reduction P : t → → s that only contracts residuals of redexes from F; the development P is complete if F/P, the set of residuals under P of redexes from F, is empty ∅. The development of ∅ is identified with the empty reduction. F will also denote a complete development of F ⊆ t. All developments are terminating; all coinitial complete developments of the same set of redexes end at the same term; and residuals of a redex under all complete coinitial developments of a set of redexes are the same.

(c) A diagram D(P, Q) for coinitial reductions P : t → → s and Q : t → → e is constructed by joining all elementary diagrams emerging in an attempt to find a common reduct of s and e (see Figure 2); an elementary diagram considers complete developments of pairs of redexes, reducing either redex, then all residuals of the other (see Figure 1). ((b) implies that the diagram can be constructed whatever order of completing the elementary diagrams is used, and the constructed common reduct of s and e is the same [Klo80].) The reduction corresponding to the opposite side of P in D(P, Q) is called a residual of P under Q (the empty developments are omitted), notation P/Q, and similarly for Q.

(d) + is the concatenation relation on reductions; for any coinitial P and Q one defines P ⊔Q = P + Q/P, P ⊴ Q iff P/Q = ∅, and P ≈_{L} Q iff P ⊴ Q and Q ⊴ P.

(2) We call a DRS R stable (SDRS) if the following axiom is satisfied (see Figure 3):

• [stability] If u, v ⊆ t are different redexes, t→^{u}e, t→^{v}s, and u creates a redex w ⊆ e, then the redexes in w/(v/u) are not u/v-residuals of redexes of s, i.e., they are created by u/v.

Proposition 2.1 ([Lév80]):

(1) (P_{1} + P_{2})/Q = P_{1}/Q + P_{2}/(Q/P_{1}), P/(Q_{1} + Q_{2}) = (P/Q_{1})/Q_{2};

P
[figure: ·; ·; ·; ·; ·]
[figure: ·; ·; ·]
[figure: ·; ·; ·; ·]

Q

[figure: ·; ·; ·; ·]
[figure: ·; ·; ·; ·; ·]

Figure 2: Klop Tiling Diagram [figure: t; u; e; w; s; v; u/v; o; v/u; w/(v/u)] Figure 3: Berry’s Stability (2) P ⊔ Q ≈_{L} Q ⊔ P.

(3) If P ≈_{L} Q, then for any redex u in the initial term of P, u/P = u/Q.

(4) P ≈_{L} Q ⇒ N/P ≈_{L} N/Q, for any N coinitial with P and Q.

(5) P ⊴ Q iff there is N such that P + N ≈_{L} Q.

(6) P ≈_{L} P′, Q ≈_{L} Q′ ⇒ P + Q ≈_{L} P′ + Q′, P + Q ≈_{L} P + Q′ ⇒ Q ≈_{L} Q′;

Proposition 2.2 ([Lév80]) ≈_{L} is the least equivalence relation satisfying:

(1) F ⊔ G ≈_{L} G ⊔ F, where F and G are redex sets in the same term.

(2) If Q ≈_{L} Q′, then P + Q + N ≈_{L} P + Q′ + N .

It is easy to verify that the λ-calculus [Lév78], orthogonal TRSs [HuLé91], orthogonal Higher-Order Rewriting Systems (HORSs) [OR94, Oos94], and hence other orthogonal higher-order rewrite systems as well (such as CRSs [Klo80], ERSs [Kha92], and HRSs [Nip93]), and Orthogonal Term Graph Rewriting Systems (OTGRSs) [KKSV93] form DRSs; OTGRSs are equivalent to Maranget’s orthogonal DAG (directed acyclic graphs) rewriting systems, defined via labelled orthogonal TRSs. All these are stable, as can be checked just using an appropriate notion of descendant which assigns the contractum to the contracted redex, as defined in [Kha92] for ERSs – labelling is not necessary. (The descendant notion defined e.g., in [BKKS87] is essentially the residual notion, and is not useful for this purpose.)

3 The Relative Normalization Theorem for regular stable sets

In this section, we recall the notion of stability and regularity for sets of terms in a DRS, and relative notions of neededness as defined in [GlKh94]. We prove that, for any regular stable S in a stable DRS R, an S-normal form of an S-normalizable term can be found by contracting S-needed redexes in it, even if every S-needed step is preceded by a finite number of S-unneeded steps. We show that without the assumption of stability for R, this result breaks down. Further, examples from [GlKh94] show that the stability of S is necessary for the Relative (Hyper)normalization theorem to hold. This shows that the stability of S for a Berry–stable R provides a unique notion of stability for the computation system (R, S). Note that S in our DRSs plays the role of the set of final states for a Transition System.

Definition 3.1 ([GlKh94]) Let Π be a set of reductions and S be a set of terms in a DRS R. We call a redex u in t Π-needed if at least one residual of it is contracted in every reduction of Π, and call it Π-unneeded otherwise. We call a redex u ⊆ t S-needed, written NE_{S}(u, t), if at least one residual of it is contracted in any reduction from t to a term in S, and call it S-unneeded, written UN_{S}(u, t), otherwise. (Thus S-neededness coincides with neededness w.r.t. the set of all S-normalizing reductions.)

Definition 3.2 ([GlKh94]) (1) We call a set S of terms stable if: (a) S is closed under parallel moves: for any t ∉ S, any P : t → → o ∈ S, and any Q : t → → e, the final term of P/Q is in S; and (b) S is closed under unneeded expansion: for any e→^{u}o such that e ∉ S and o ∈ S, u is S-needed.

(2) We call a stable set S regular if S-unneeded redexes cannot duplicate S-needed ones.

Below S (resp. R) will usually denote a (resp. regular) stable set of terms in some DRS. For simplicity, we only consider stable sets S that are closed under reduction; obviously, closure of S under reduction implies its closer under parallel moves.

[figure: t_{0}; v_{0} = P_{1}; t_{1}; t_{n−1}; v_{n−1}; t_{n}; o_{0}; Q_{0}; P′_{1}; o_{1}; Q_{1}; t_{n−1}; Q_{n−1}; P′_{n}; o_{n}; Q_{n}]

Figure 4: Preservation of External Reductions

The most appealing examples of stable sets are the set of normal forms [HuLé91], the set of head-normal forms [BKKS87], the set of weak-head-normal forms (a partial result is in [Mar92]), and the set of constructor-head-normal forms for constructor TRSs [Nök94]. All the above sets are closed under reduction. Clearly, Huet&Levy-neededness [HuLé91] is neededness w.r.t. the set of normal forms. It was shown in [GlKh94] that Maranget’s notion of neededness [Mar92] coincides with neededness w.r.t. the set of all fair reductions (Huet&Levy- and Maranget-neededness coincide for normalizable terms). All the above stable sets are regular. An example of an OTRS with an irregular stable S is given in Remark 3.1.

Definition 3.3 We call P : t → → s external to Q : t → → e if for every elementary diagram D(u, v) in a diagram D(P, Q), whatever order of construction of developments in the elementary diagrams is used, one has u ≠ v. We call P external to a set of redexes F ⊆ t if P doesn’t contract residuals of redexes in F (i.e., iff P is external to the development F). We will say that P is external to u ⊆ t if it is external to {u}.

Lemma 3.1 Let P : t_{0}→^{v_{0}}t_{1}→^{v_{1}} … → t_{n} be external to F = {u_{1}, …, u_{n}} ⊆ t_{0}, and let Q_{0} : t_{0} → → o_{0}.

Then P′ = P/Q_{0} is external to F′ = F/Q_{0}. If P is S-normalizing, then so is P′.

Proof Let P_{i} : t_{0}→^{v_{0}}t_{1}→^{v_{1}} … → t_{i}, Q_{i} = Q_{0}/P_{i}, and P′_{i+1} = v_{i}/Q_{i}, (0 ≤ i < n). Since P is external

to F, we have for each i that v_{i} ∉ F/P_{i}. Therefore, v_{i}/Q_{i} ∩ F/(P_{i} + Q_{i}) = ∅ (since the residuals of different redexes are different). Thus, by Proposition 2.1.(3), v_{i}/Q_{i} ∩ F/(Q_{0} + P′_{1} + … + P′_{i}) = ∅. Hence, P′_{i+1} is external to F′/(P′_{1} + … + P′_{i}). This means that P′ is external to F′. If P is S-normalizing, then so is P′, by the closure of S under parallel moves.

Corollary 3.1 For any stable S, residuals of S-unneeded redexes under any reduction remain S-unneeded.

Lemma 3.2 Let P : t → → s be external to Q : t → → e, in a stable DRS, and let P create redexes W ⊆ s. Then the residuals W/(Q/P) of redexes in W are created by P/Q, and Q/P is external to W. Proof By induction on the number n of elementary diagrams in D(P, Q). The case n = 1 is the axiom [stability]. So let say |P | > 1, i.e., P = u + N with |N| > 0. Then W = W_{u}/N ∪ W_{N}, where W_{u} is the set of redexes created by u, and W_{N} is the set of redexes created by (i.e., along) N. By the induction assumption, Q/u is external to W_{u}, and the redexes in W_{u}/(Q/u) are created by u/Q. By Lemma 3.1, Q/P = (Q/u)/N is external to W_{u}/N. By the induction assumption,

t  [figure: Q] e

[figure: u; Q/u]
[figure: s; N; Q/P = (Q/u)/N]

Figure 5: External Redex Creation

Q/P = (Q/u)/N is external to W_{N} and redexes in W_{N}/(Q/P) are created by N/(Q/u). Hence Q/P is external to W, and since W/(Q/P) = W_{N}/(Q/P) ∪ W_{u}/((Q/u) ⊔ N), redexes in W/(Q/P) are created by P/Q.

Lemma 3.3 Let S be stable, let t ∉ S, t→^{u}e, UN_{S}(u, t), and let w ⊆ e be a u-new redex, in a stable DRS. Then UN_{S}(w, e). Proof If e ∈ S, then every redex in e is S-unneeded; so suppose e ∉ S. UN_{S}(u, t) implies existence of an S-normalizing P : t → → s that does not contract residuals of u. By Lemma 3.2, P/u does not contract residuals of w. Also, P/u is S-normalizing since S is closed under parallel moves. Hence w is S-unneeded.

The following example shows that, for the above lemma to hold, it is necessary that the DRS be stable.

Example 3.1 Let terms in the DRS R be t = I(I(x)), s = I(x), and e = x; redexes in t be u = t and v = I(x), s contain the only redex w = s, and x doesn’t contain a redex; let the reduction relation be given by Red = {t→^{u}s, t→^{v}s, s→^{w}x}, let the residual relation be empty except for empty reductions, for which the residual relation is identity, and let S = {x}. (Obviously, this is not the usual residual relation for orthogonal TRSs; it cannot be, because OTRSs with the usual residual relation are stable DRSs.) Then S is stable and regular, both u and v are S-unneeded, and both create the redex w ⊆ s that is S-needed. Note also that the Relative Hypernormalization theorem (proved below) is not valid for R since t ∉ S is S-normalizable but doesn’t contain an S-needed redex.

Definition 3.4 We call P : t_{0} → t_{1} → … S-(un)needed, written NE_{S}(P), (resp. UN_{S}(P)) if it contracts only S-(un)needed redexes. NE_{S}|P | denotes the number of S-needed steps in P. We call P S-quasi-needed if NE_{S}|P | = ∞ and call it S-semi-needed if it can be expressed as P = P_{1} + P_{2} with NE_{S}(P_{1}) and UN_{S}(P_{2}). In the latter case, we call P_{1} the S-needed part of P and denote by NE_{S}[P], and call P_{2} the S-unneeded part of P and denote by UN_{S}[P].

In the following definition, we describe an algorithm that, for a regular stable R in a DRS, transforms any finite reduction P into an R-semi-needed reduction Lévy-equivalent to P, and any R-quasi-needed reduction Q into an infinite R-needed reduction. The regularity of R is essential for termination of the transformation process, and for preservation of R-quasi-neededness of the reduction under transformation. The latter property is crucial for our method for proving termination of an R-needed reduction starting from an R-normalizable term.

[figure: P_{1}; u; v′; u/v′; v; P_{2}]

Figure 6: Constructing Semi-needed Reductions

Definition 3.5 Let Red be the set of all reductions in an SDRS R, let R be a regular stable set of terms in R, and let Red^{∗} be the set of R-semi-needed reductions. We define a function K : Red → Red^{∗} as follows:

(a) Let P be a finite reduction. K(P) is an R-semi-needed reduction obtained from P in the following way: find in P the first from the left subreduction P_{0} : t→^{u}s→^{v}o such that UN_{R}(u, t) and NE_{R}(v, s). Let P = P_{1} + P_{0} + P_{2}. By Lemma 3.3, v is a residual of a redex v′ ⊆ t, which is Rneeded by Corollary 3.1. Since R is regular, v is the only residual of v′, hence P_{0} and P′_{0} = v′ +u/v′ are both complete developments of the set u, v′ ⊆ t. Now replace P_{0} by P′_{0} in P. Transform the obtained reduction P′ in the same way, and so on, as long as possible. Obviously, the number of R-unneeded steps in P′ preceding v′ is less than the number preceding v in P, and the number of R-needed steps in P and P′ coincide. Therefore, the procedure terminates eventually. The result is K(P). Obviously, P ≈_{L} K(P).

(b) Let NE_{R}|P | < ∞ (|P | = ∞ is possible). P can be expressed as P = P_{1} + P_{2}, where UN_{R}(P_{2}) and the last step in P_{1} is R-needed. Then we take K(P) = K(P_{1}) + P_{2} (that is possible since P_{1} ≈_{L} K(P_{1})). Obviously, K(P) ∈ N^{∗} and P ≈_{L} K(P).

(c) Let NE_{R}|P | = ∞. Suppose that P_{i} is the initial part of P with a length i and Q_{i} is the R-needed part of K(P_{i}), with a length m_{i}. By definition, K(P) is the reduction whose initial part of the length m_{i} coincides with Q_{i} (i = 0, 1, …). It follows from (a)-(b) that if i < j, then Q_{i} is an initial part of Q_{j}, so K(P) is defined correctly. Obviously, NE_{R}(K(P)) and hence K(P) ∈ Red^{∗}.

Lemma 3.4 Let P be a finite or infinite reduction in an SDRS, and let R be regular. (1) NE_{R}|P | = NE_{R}|K(P)| = |NE_{R}[K(P)]| ≤ |P |.

(2) |P | < ∞ iff |K(P)| < ∞.

(3) If P ends at a term in R, then NE_{R}[K(P)] ends at a term in R as well.

(4) If NE_{R}|P | = ∞, then NE_{R}(K(P)). Proof (1), (2), and (4) follow immediately from Definition 3.5; (3) follows from the stability of R — K(P) is R-semi-needed, it ends at R, and the step of K(P) entering R is R-needed.

Corollary 3.2 If a term t ∉ R in an SDRS has an R-normal form, then t has an R-needed Rnormalizing reduction, and any R-normalizing reduction starting from t, with a minimal length, is R-needed.

Lemma 3.5 Let R be a regular stable set of terms in a DRS R, and let t→^{u}s. Then any R-needed redex v ⊆ t different from u has an R-needed residual.

[figure: t_{0}; u_{0}; t_{1}; u_{1}; t_{2}; s_{0}; u = F_{0}; u_{0}/F_{0}; s_{1}; F_{1}; u_{1}/F_{1}; s_{2}; F_{2}]

Figure 7: Preservation of Quasi-needed Reductions

Proof If t is not R-normalizable, then neither is s, and all redexes in t and s are R-needed. So suppose t is R-normalizable (t ∉ R since t contains an R-needed redex), and suppose on the contrary that each residual v_{i} of v in s is R-unneeded. By closure of R under parallel moves, s is R-normalizing too. By Corollary 3.2, there is an R-needed R-normalizing reduction P : s → → o. Since by Corollary 3.1 all residuals of each v_{i} along P are R-unneeded, P is external to all v_{i}. Therefore, u + P is external to v and is R-normalizing – a contradiction, since NE_{R}(v, t).

Lemma 3.6 Let t_{0} have an R-quasi-needed reduction and t_{0}→^{u}s_{0}. Then s_{0} also has an R-quasi-needed reduction. Proof By Lemma 3.4, t_{0} has an infinite R-needed reduction P : t_{0}→^{u_{0}}t_{1}→^{u_{1}} . . .. Let F_{i} = u/(u_{0} + … + u_{i−1}), i = 0, 1, . . .. Using Proposition 2.1 we can construct the diagram in Figure 7. It follows from finiteness of developments that there are infinitely many numbers k such that u_{k} ∉ F_{k} (otherwise there should be a number m such that t_{m}→^{u_{m}}t_{m+1} →^{u_{m+1}} … is an infinite F_{m}-development). By Lemma 3.5, u_{k} ∉ F_{k} and NE_{R}(u_{k}, t_{k}) imply that u_{k} has at least one R-needed F_{k}-residual in s_{k}, i.e. u_{k}/F_{k} contains at least one R-needed step. Hence P/u is R-quasi-needed. Alternative proof Let P : t_{0}→^{u_{0}}t_{1}→^{u_{1}} … contain infinitely many R-needed steps. It is easy to see that, in Figure 7, there are infinitely many numbers k such that NE_{R}(u_{k}, t_{k}) and u_{k} ∉ F_{k}. Indeed, otherwise there would be a number m such that in P_{m} : t_{m}→^{u_{m}}t_{m+1} →^{u_{m+1}} … all contracted R-needed redexes are residuals of u. But this is impossible, since, by Lemma 3.4, K(P_{m}) would be an infinite development. By Lemma 3.5, u_{k} ∉ F_{k} and NE_{R}(u_{k}, t_{k}) imply that u_{k} has at least one R-needed F_{k}-residual in s_{k}, i.e., u_{k}/F_{k} contains at least one R-needed step. Hence P/u is R-quasi-needed.

Theorem 3.1 (Relative Hypernormalization) Let R be a regular stable set of terms in a stable DRS R, and let t ∉ R be a term in R. Then

(1) t contains at least one R-needed redex.

(2) t has an R-normal form iff it does not possess a reduction in which infinitely many times R-needed redexes are contracted. Proof (1) By Definition 3.1 if t is not R-normalizing, and by Corollary 3.2 otherwise. (2) (⇒) Let t → →^{P} s ∈ R. Suppose on the contrary that there is an R-quasi-needed Q starting from t. Then by Lemma 3.6 Q/P is R-quasi-needed as well – a contradiction, since all terms of Q/P are in R, by the closure of R under reduction, and therefore Q/P must be R-unneeded. (⇐) By (1), one can repeatedly contract R-needed redexes in t, unless a term in R is reached; the latter is inevitable since t doesn’t have an infinite R-needed reduction.

f(a)  \overline{}g(a, a)
[figure]
g(a, b)  g(b, a)
[figure]
[figure: f(b); g(b, b)]

Figure 8: Need for Closure under parallel moves

In [GlKh94], some counterexamples are presented to show that the stability of S is necessary for the Huet&Lévy theory of normalization to remain valid. For example, if one takes S = {I(x), x} in the TRS with only one rule I(x) → x, then S is closed under reduction, hence under parallel moves too, but is not closed under unneeded expansion: t = I(I(x)) can be reduced to I(x) by contracting either I-redex. As a consequence, neither redex is S-needed in t, which is not in Snormal form and has one. To show that closure under unneeded expansion is not enough, and that closure under parallel moves is also necessary, take R = {f(x) → g(x, x), a → b, b → a} and S = {g(a, b)}. Since the reduction in R preserves the height of a term and the property to be a ground term, only the terms in the diagram in Figure 8 are S-normalizable. Therefore, it is clear that S is closed under normalization, i.e., the reduct of any S-normalizable term remains so. It is easy to see that, in f(a) and f(b), all the redexes are S-needed; hence f(a) → f(b) → f(a) → … is an infinite S-needed reduction that never reaches S (there are many others). One can check that S is closed under unneeded expansion. Thus the reason for the failure of the normalization theorem is that S is not closed under parallel moves – P : f(a) → g(a, a) → g(a, b) is S-normalizing, but ft(P ⊔ Q) = g(b, b) ∉ S, where Q : f(a) → f(b). Further, it is shown in [GlKh94] that if S is stable, but not regular, then the S-needed strategy need not be hypernormalizing any more (see the following remark). Hence, Example 3.1 shows that the above Relative Hypernormalization theorem is the most general possible normalization result for DRSs.

Remark 3.1 If S is not regular, then Lemma 3.4 doesn’t hold. Indeed, consider the example from [GlKh94]: take OTRS R = {f(x) → h(f(x), f(x)), a → b} and take for S the set of terms not containing occurrences of a. It is easy to check that S is stable, but is not regular, since the outermost redex in t = f(a) is S-unneeded, while the innermost one is S-needed. Then P : f(a) → h(f(a), f(a)) → h(f(b), f(a)) → h(f(b), h(f(a), f(a))) → h(f(b), h(f(b), f(a))) → … is S-quasi-needed, while Q = NE_{S}[K(P)] : f(a) → f(b) is S-normalizing, and P/Q = f(b) → h(f(b), f(b)) → h(f(b), h(f(b), f(b))) → … is S-unneeded, thus not S-quasi-needed any more. Because of that, the proof of Lemma 3.6 fails, and the S-needed strategy need not be hypernormalizing when S is not regular (P repeatedly contracts S-needed redexes in an S-normalizable term, and is infinite).

4 Relative Normalization in Family Structures

In order to generalize the Relative Normalization theorem to all stable sets in DRSs, we introduce Family structures (FSs) by defining a notion of family in a DRS, and by imposing some axioms on the contribution relation on families. This enables us to repeat the proof of Relative Normalization theorem in [GlKh94] for all FSs, and makes explicit the properties of family relation needed to develop an abstract theory of optimal normalization.

Definition 4.1 (Family Structure) A Family Structure (FS for short) is a DRS with the relations ≃_{z} (zig-zag family) and ≃ (family) on redexes with histories, and the relation ↪ (contributes) on coinitial families (as defined below) such that:

(1) For any co-initial reductions P and Q, the redex Qv in the final term of Q (read as v with history Q) is called a copy of a redex P u if P ⊴ Q, i.e., P + Q/P ≈_{L} Q, and v is a Q/P -residual of u; the zig-zag relation ≃_{z} is the symmetric and transitive closure of the copy relation [Lév80]. A family relation ≃ is an equivalence relation among redexes with histories containing ≃_{z}. A family (relative to a term t) is the class of all redexes with co-initial histories (starting from t) that are in the family relation; families are ranged over by ϕ, ψ, . . ..

(2) The relations ≃ and ↪ satisfy the following:

• [contribution] ϕ ↪ ϕ′ iff for any P u ∈ ϕ′, P contracts at least one redex in the family ϕ.

• [creation] if e → →^{P} t→^{u}s and u creates a redex v ⊆ s, then F am(u) ↪ F am(v) (more precisely, F am(P u) ↪ F am((P + u)v), where F am( ) denotes the family of its argument.

• [termination] Any reduction that contracts redexes of a finite number of families is terminating.

One can check that all the existing definitions of family relation in the literature [Lév78, KeSl89, Mar92, AsLa93] satisfy the above axioms. Hence our definition is consistent. Note that we do not use the property below as an axiom, though it is satisfied by all existing family notions. We expect that it can be proved from the other FS axioms (see also Section 6). Another reason is that the do not need it in our proof of the Relative Normalization theorem.

• [extraction] Let Con(ϕ) = {ϕ_{i} | ϕ_{i} ↪ ϕ} be the cone of ϕ. Then there is P u ∈ ϕ such that P only contracts redexes in the contributor families ϕ_{i} (that redexes of every such a family is contracted in P follows from [contribution]).

The reason for considering more notions of family than just the zig-zag is that we want to be more flexible and able to consider a large class of sharing mechanisms as legal; there are sharing mechanisms that are strictly larger than zig-zag, e.g., the one in [AsLa93].

Proposition 4.1 • [irreflexivity] ϕ ↛ ϕ.

• [transitivity] If ϕ ↪ ϕ′ and ϕ′ ↪ ϕ′′, then ϕ ↪ ϕ′′.

• [cone] ϕ ↪ ψ ⇒ Con(ϕ) ⊂ Con(ψ) (i.e., Con(ϕ) ⊆ Con(ψ) and Con(ϕ) ≠ Con(ψ)).

• [finiteness] For any family ϕ, Con(ϕ) is finite, and Con(∅_{t}u) = ∅ for any u ⊆ t.

• [antisymmetry] If Con(ϕ) = Con(ψ) and ϕ ≠ ψ, then ϕ ↛ ψ (and ψ ↛ ϕ). Proof [irreflexivity], [transitivity], and [finiteness] follow immediately from [contribution]. [cone] follows from [irreflexivity] and [transitivity]. [antisymmetry] follows from [cone].

Definition 4.2 [Lév80] Let Φ be a set of families relative to t. A reduction P : t → → s is a development of Φ if F AM(P) ⊆ Φ, where F AM(P) denotes the set of families (whose member redexes are) contracted in P. A development P of Φ is complete if ft(P) does not contain redexes from Φ.

We have the following abstract form of the Generalized Finite Developments Theorem [Lév80].

[figure: x; ·; v; ·]
[figure: u_{2}; u_{1}]
·  · [figure: w; \underline{u′_{2a}}] ·
[figure: u′_{1}; u′_{2}; u′_{2b}]
[figure: ·; u; v_{1}; ·; ∅; \underline{∅}; ·]

Figure 9: Independence of the axiom [termination]

Proposition 4.2 (Finite Family Developments Theorem)

(1) Any development of a finite set Φ of co-initial families is terminating.

(2) All complete developments of a finite set Φ of co-initial families are Lévy-equivalent. Proof (1) is the axiom [termination]; (2) Same as in [Lév80]. If P and Q are Φ-developments, then so are P ⊔ Q and Q ⊔ P by ≃_{z}⊆≃, and if P and Q are complete, P = P ⊔ Q ≈_{L} Q ⊔ P = Q by Proposition 2.1.

The axioms [creation] and [contribution], together with the DRS axiom about developments, do not imply [termination]. Consider the ARS illustrated in Figure 9, where the redex x creates u and v; u_{1} and u′_{2a} create w; u/v = {u_{1}, u_{2}}; u_{1}/u_{2} = u′_{1}, u_{2}/u_{1} = u′_{2}; u′_{2}/w = {u′_{2a}, u′_{2b}}; w/u′_{2} = ∅, u′_{2a}/u′_{2b} = ∅, u′_{2b}/u′_{2a} = u′_{2}. All the us are residuals of u, hence belong to the same family U; therefore, all contracted ws belong to the same family too, say W. There are two other families X = {x} and V = {v}, and we have X ↪ V, U and U ↪ W. Since the only infinite reduction goes through the cycle infinitely many times, and each time the contracted w is created by u′_{2a}, all developments in the figure are terminating. It remains to note that the other requirements on developments, and the two contribution axioms are satisfied too.

Lemma 4.1 Any FS R is a stable DRS. Proof We want to show that if u, v ⊆ t are different redexes, t→^{u}e, t→^{v}s, and u creates a redex w ⊆ e, then the redexes in w/(v/u) are not u/v-residuals of redexes of s (see Figure 1). By axioms [creation] and [contribution], for any redex w′ ⊆ s, Con(F am(w′)) = ∅ if w′ is not a new redex, and Con(F am(w′)) = {F am(v)} otherwise; and Con(F am(w)) = {F am(u)}. Hence the redexes in o = ft(v/u) and s are in different families, and the lemma follows (since ≃_{z}⊆≃).

Lemma 4.2 Let S be stable, t ∉ S, t→^{u}t′, UN_{S}(u, t), and let u′ ⊆ t′ be a u-new redex, in an FS R. Then UN_{S}(u′, t′). Proof By Lemma 3.3 and Lemma 4.1.

Now we can generalize the Relative Normalization Theorem, proved in [GlKh94] for orthogonal Expression Reduction Systems [Kha92], to all FSs. We allow for arbitrary stable sets S, not only regular ones as for the Relative Hypernormalization theorem.

t  [figure: P] s
[figure: t_{i}; Q_{i}; P_{i}]

[figure: t_{i+1}; u_{i}; P_{i+1}]
[figure]

Figure 10: Termination of Needed Reduction

Theorem 4.1 (Relative Normalization) Let S be a stable set of terms in a Family Structure R. (1) Any S-normalizable term t in R not in S-normal form contains an S-needed redex.

(2) If t is S-normalizable, then any S-needed reduction starting from t eventually terminates at a term in S. Proof (1) Let P : t → → s′ → s→^{u}e be an S-normalizing reduction with s ∉ S. By the stability of S, u is S-needed. By Corollary 3.1 and Lemma 4.2, it is either created by or is a residual of an S-needed redex of s′, and (1) follows by repeating the argument.

(2) Let P : t → → s be an S-normalizing reduction and Q : t→^{u_{0}}t_{1}→^{u_{1}} … be an S-needed reduction.

Further, let Q_{i} : t→^{u_{0}}t_{1}→^{u_{1}} … →^{u_{i−1}}t_{i} and P_{i} = P/Q_{i} (i ≥ 1) (see Figure 10). By ≃_{z}⊆≃, F AM(P_{i}) ⊆

F AM(P). Since Q is S-needed and P_{i} is S-normalizing (by the closure of S under parallel moves), at least one residual of u_{i} is contracted in P_{i}. Therefore, again by ≃_{z}⊆≃, F am(u_{i}) ∈ F AM(P_{i}). Hence F AM(Q) ⊆ F AM(P) and Q is terminating by Proposition 4.2.(1).

Lemma 4.3 Let S be a stable set of terms in an FS R, and let t→^{u}s. Then any S-needed redex v ⊆ t different from u has an S-needed residual in s. Proof Same as the proof of Lemma 3.5, but using Theorem 4.1 instead of Corollary 3.2.

5 The Relative Optimality Theorem

In this section, we define weakly S-needed redexes, and show that their contraction in an Snormalizable term t leads to an S-normal form of t. This generalizes the result of Lévy [Lév80] stating that needed family-reduction is normalizing, and is useful for strictness analysis. We also generalize Lévy’s Optimality Theorem [Lév80] to all stable sets S in any Family Structure.

Definition 5.1 Let P : t→^{u_{0}}t_{1}→^{u_{1}}t_{1} … →^{u_{n−1}}t_{n} in an FS R, and let S be a set of terms of R. We call u ∈ t_{i} weakly S-needed w.r.t. t→^{u_{0}}t_{1}→^{u_{1}}t_{1} … → t_{i} if u is in the family of an S-needed redex occurring in some t_{j}. A reduction is weakly S-needed if each redex contracted in it is (w.r.t. the initial reduction).

Theorem 5.1 Let S be a stable set of terms in a Family Structure R, and t be an S-normalizable term in R. Then any weakly S-needed reduction starting from t is terminating.

Proof Let P : t → → s be an S-normalizing reduction and Q : t→^{u_{0}}t_{1}→^{u_{1}} … be a weakly S-needed reduction. Further, let Q_{i} : t→^{u_{0}}t_{1}→^{u_{1}} … →^{u_{i−1}}t_{i} and P_{i} = P/Q_{i} (see again Figure 10). Since Q is weakly S-needed, for each i, there is an S-needed redex u′_{i} in some t_{j} that is in the same family as u_{i}. Since at least one residual of u′_{i} is contracted in P_{j} (P_{j} is S-normalizing by the closure of S under parallel moves) and ≃_{z}⊆≃, F AM(Q) ⊆ F AM(P). Since P is finite, Q is terminating by the axiom [termination].

The above theorem allows one to propagate S-neededness information, obtained from earlier terms, along the reduction, and to contract safely (without a danger of missing an S-normal form whenever it exists) any residual of an S-needed redex, even if it is no longer S-needed.

Definition 5.2 A multistep reduction P : t_{0} → → t_{1} → → … → → t_{n} is called a family-reduction if each P_{i} : t_{i} → → t_{i+1} is a development of a set F_{i} of redexes belonging to the same family. ∥P ∥ will denote the number of multisteps in P. The family-reduction P is complete if each P_{i} is the complete development of a maximal set of redexes of t_{i} belonging to the same family. A family-reduction P is called S-needed if each F_{i} contains at least one S-needed redex (i.e., if the (single-step) reduction corresponding to P is weakly S-needed).

Corollary 5.1 Let S be a stable set of terms in a Family Structure R, and t be an S-normalizable term in R. Then any S-needed family-reduction staring from t is eventually S-normalizing.

Lemma 5.1 Every family is contracted at most once in any complete family-reduction. Proof Let P_{n} : t_{0} → →^{F_{0}} t_{1} → →^{F_{1}} … → →^{F_{n−1}} t_{n} be a complete family-reduction. We show by induction on n = ∥P ∥ that (a)_{n}: all families contracted in P_{n} are different; and (b)_{n}: there is no redex in t_{n} whose family has been contracted in P_{n}. The case n = 0 is clear. Further, (a)_{n} follows immediately from (a)_{n−1} and (b)_{n−1}. Again by (a)_{n−1} and (b)_{n−1}, and by the completeness of P_{n}, all redexes in t_{n} that are residuals of redexes of t_{n−1} are in families that have not been contracted before. By [creation], for the family ϕ of a new redex in t_{n}, we have F am(F_{n−1}) ↪ ϕ; by (a)_{n−1}, (b)_{n−1}, and [contribution], F am(F_{n−1}) ↛ F am(F_{i}), for any i ≤ n − 1. Hence Con(F am(F_{i})) ≠ Con(ϕ), and (b)_{n} follows.

Theorem 5.2 (Relative Optimality) Let S be a stable set of terms in a Family Structure R, and t be an S-normalizable term in R. Then any S-needed complete family-reduction starting from t is S-optimal in the sense that it reaches an S-normal form of t in a minimal number of family-reduction steps. Proof Similar to the proof of the optimality theorem for the λ-calculus in [Lév80]. Let P : t → → s be an S-normalizing family-reduction and Q : t → → e be an S-needed complete family-reduction. It follows from the proof of Theorem 5.1 that F AM(Q) ⊆ F AM(P). Hence, by Lemma 5.1, ∥Q∥ = Card(F AM(Q)) ≤ Card(F AM(P)) ≤ ∥P ∥, where Card(F AM(Q)) denotes the number of families in F AM(Q).

6 Conclusions and future work

We have proved two abstract versions of Relative Normalization theorem: one in DRSs for regular stable sets R, and another in FSs for all stable S. Needless to say that our first proof is the simplest existing proof among those that use the notion of residual, though it covers all the existing normalization results, except for the one in [GlKh94]. It is remarkable that our proofs does not use the notion of standard reduction – recall that the original proof of the Normalization theorem of the λ-calculus in Curry&Feys [CuFe58] uses the Standardization theorem, and the proofs of the normalization of the needed strategy in [HuLé91] and [BKKS87] use the fact that standard normalizing reductions are the longest among needed reductions. The proofs of the normalization of the needed (essential) strategy in [Kha88, Kha93] do not use the Standardization theorem either, but they are based on the notion of descendant of subterms rather than that of residual of redexes, which is a very syntactic notion, therefore much more difficult to axiomatize.

The proofs of the normalization of needed strategy for orthogonal CRSs by Kennaway and Sleep [KeSl89] and for orthogonal DAG rewriting by Maranget [Mar91, Mar92] use an even stronger termination argument – termination of developments of any finite set of co-initial families. They both used suitable labelling systems to define notions of family, and their labelled OCRS and OTRS are Family Structures if the contribution relation is defined by axiom [contribution]. Our second proof can be seen as a generalization of that proof method, which was used already by Lévy in [Lév78, Lév80].

Our first theorem covers both above results and our proof is much simpler because it doesn’t use any notion of family. An interesting question is whether our second theorem can also be proved for stable DRSs, i.e., without family axioms, but some much weaker axioms. One way to do this is to guarantee the axiom [termination], and to show that, if in an SDRS one defines the contribution relation according to [contribution], then [creation] is satisfied if the zig-zag is taken for the family relation. However, this is non-trivial, and is left for a future research.

As for the axiom [extraction], in the case when the residual relation is non-duplicating (as, e.g., in Stark’s DCTSs [Sta89]) or when only complete family-reductions are considered, [extraction] follows from the Relative Normalization theorem for FSs. Indeed, in the notation of [extraction], if ϕ is a family relative to a term t, it is possible to define the pair (R_{ϕ}, S_{ϕ}), such that terms in R_{ϕ} are of the form (Q, s) such that s ∈ R and Q : t → → s in R; rewrite steps in R_{ϕ} are some of those induced by R (avoiding those that cause erasure of redexes in ϕ); the residual relation is that induced by R, and S_{ϕ} is such that all steps that contribute to ϕ become S_{ϕ}-needed. Proof of [extraction] in the general case also goes beyond the scope of this paper.

Acknowledgements

We thank J. R. Kennaway, J.-J. Lévy, L. Maranget, V. van Oostrom, and M. R. Sleep for useful comments.

References

[AsLa93] Asperti A., Laneve C. Interaction Systems I: The theory of optimal reductions. Mathematical Structures in Computer Science, vol. 11, Cambridge University Press, 1993, p. 1-48.

[Bar84] Barendregt H. P. The Lambda Calculus, its Syntax and Semantics. North-Holland, 1984.

[BKKS87] Barendregt H. P., Kennaway J. R., Klop J. W., Sleep M. R. Needed Reduction and spine strategies for the lambda calculus. Information and Computation, v. 75, no. 3, 1987, p. 191-231.

[Ber79] Berry G. Modéles complétement adéquats et stables des λ-calculs typés. Thèse de l’Université de Paris VII, 1979.

[CuFe58] Curry H. B., Feys R. Combinatory Logic. vol. 1, North-Holland, 1958.

[DeJo90] Dershowitz N., Jouannaud J.-P. Rewrite Systems. In: J. van Leeuwen ed. Handbook of Theoretical Computer Science, Chapter 6, vol. B, 1990, p. 243-320.

[GlKh94] Glauert J.R.W., Khasidashvili Z. On Relative Normalization in Orthogonal Expression Reduction Systems. In: Proc. of the 4^{th} International Workshop on Conditional (and Typed) Term Rewriting Systems, CTRS’94, Jerusalem, 1994. To appear in Springer LNCS series. (Available as ftp://ftp.sys.uea.ac.uk/pub/glauert/CTRS.ps.gz)

[GLM92] Gonthier G., Lévy J.-J., Melliès P.-A. An abstract Standardisation theorem. In: Proc. of the 7^{th} Annual IEEE Symposium on Logic in Computer Science, LICS’92, Santa Cruz, California, IEEE Computer Society Press, 1992, p. 72-81.

[HuLé91] Huet G., Lévy J.-J. Computations in Orthogonal Rewriting Systems. In: Computational Logic, Essays in Honor of Alan Robinson, J.-L. Lassez and G. Plotkin, eds. MIT Press, 1991.

[KeSl89] Kennaway J. R., Sleep M. R. Neededness is hypernormalizing in regular combinatory reduction systems. Preprint, School of Information Systems, University of East Anglia, Norwich, 1989.

[KKSV93] Kennaway J. R., Klop J. W., Sleep M. R, de Vries F.-J. Event structures and orthogonal term graph rewriting. In: M. R. Sleep, M. J. Plasmeijer, and M. C. J. D., eds. Term Graph Rewriting: Theory and Practice. John Wiley, 1993.

[Kha88] Khasidashvili Z. β-reductions and β-developments of λ-terms with the least number of steps. In: Proc. of the International Conference on Computer Logic COLOG’88, Tallinn 1988, Springer LNCS, v. 417, P. Martin-Löf and G. Mints, eds. 1990, p. 105–111.

[Kha92] Khasidashvili Z. The Church-Rosser theorem in Orthogonal Combinatory Reduction Systems. Report 1825, INRIA Rocquencourt, 1992.

[Kha93] Khasidashvili Z. Optimal normalization in orthogonal term rewriting systems. In: Proc. of the 5^{th} International Conference on Rewriting Techniques and Applications, RTA’93, Springer LNCS, vol. 690, C. Kirchner, ed. Montreal, 1993, p. 243-258.

[Klo80] Klop J. W. Combinatory Reduction Systems. Mathematical Centre Tracts n. 127, CWI, Amsterdam, 1980.

[Klo92] Klop J. W. Term Rewriting Systems. In: S. Abramsky, D. Gabbay, and T. Maibaum eds. Handbook of Logic in Computer Science, vol. II, Oxford University Press, 1992, p. 1-116.

[Lév78] Lévy J.-J. Réductions correctes et optimales dans le lambda-calcul, Thèse de l’Université de Paris VII, 1978.

[Lév80] Lévy J.-J. Optimal reductions in the Lambda-calculus. In: To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, Hindley J. R., Seldin J. P. eds, Academic Press, 1980, p. 159-192.

[Mar91] Maranget L. Optimal derivations in weak λ-calculi and in orthogonal Term Rewriting Systems. In: Proc. of the 17^{th} ACM Symposium on Principles of Programming Languages, POPL’91, p. 255-269.

[Mar92] Maranget L. La stratégie paresseuse. Thèse de l’Université de Paris VII, 1992.

[Nip93] Nipkow T. Orthogonal higher-order rewrite systems are confluent. In: Proc. of the 1^{st} International Conference on Typed Lambda Calculus and Applications, TLCA’93, Springer LNCS, vol. 664, Bazem M., Groote J.F., eds. Utrecht, 1993, p. 306-317.

[Nök94] Nöcker E. Efficient Functional Programming. Compilation and Programming Techniques. Ph.D. Thesis, Catholic University of Nijmegen, 1994.

[Oos94] Van Oostrom V. Confluence for Abstract and Higher-Order Rewriting. Ph.D. Thesis, Free University of Amsterdam, 1994.

[OR94] Van Oostrom V., van Raamsdonk F. Weak orthogonality implies confluence: the higherorder case. In: Proc. of the 3^{rd} International Conference on Logical Foundations of Computer Science, ‘Logic at St. Petersburg’, LFCS’94, Springer LNCS, vol. 813, Narode A., Matiyasevich Yu. V. eds. St. Petersburg, 1994. p. 379-392.

[Sta89] Stark E. W. Concurrent transition systems. Theoretical Computer Science, vol. 64, 1989, p. 221-270.