Discrete Normalization and Standardization in Deterministic Residual Structures

Zurab Khasidashvili and John Glauert

School of Information Systems, UEA Norwich NR4 7TJ England zurab@sys.uea.ac.uk, jrwg@sys.uea.ac.uk Tel: +44 1603 59 26 71 Fax: +44 1603 59 33 44 ^{⋆}

Abstract. We prove a version of the Standardization Theorem and the Discrete Normalization Theorem in stable semi-linear Deterministic Residual Structures, which are Abstract Reduction Systems with axiomatized residual relation. The latter theorem gives as a corollary a Gross-Knuth style algorithm for construction of reductions Lévy-equivalent to a given, finite or infinite, reduction. This and other results of this paper add to the understanding of Lévyequivalence of reductions, and consequently, Lévy’s reduction space.

1 Introduction

Long ago, Curry and Feys [CuFe58] proved that repeated contraction of leftmost-outermost redexes in any normalizable λ-term eventually yields its normal form, even if the term possesses infinite reductions as well. The reason is that such redexes are needed in every normalizable term t, i.e., they are contracted in every normalizing reduction starting from t. Based on this observation, Huet and Lévy defined a general normalizing strategy, called the needed strategy, for Orthogonal Term Rewriting Systems (OTRSs). They 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] studied neededness w.r.t. normal forms as well as w.r.t. head-normal forms, in the λ-calculus, proving correctness of the two needed strategies for computing normal forms and head-normal forms, respectively. Maranget [Mar92] 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].

Khasidashvili defined a similar normalizing strategy, called the essential strategy, for the λcalculus [Kha88] and OTRSs [Kha93]. The strategy contracts essential redexes – the redexes that have descendants (not residuals) under any reduction. Sekar and Ramakrishnan [SeRa90] study a normalizing strategy which in each multi-step contracts a necessary set of redexes – a set at least one member of which is contracted in every normalizing reduction. A different approach to normalization in not-necessarily orthogonal rewrite systems is developed in Kennaway [Ken89] and Antoy&Middeldorp [AnMi94]. Antoy et al. [AEH94] designed a needed narrowing strategy. Gardner [Gar94] described a complete way of encoding neededness information using a type assignment system. Kennaway et al. [KKSV93] studied needed strategy for infinitary OTRSs.

In [GlKh94], the present authors found natural conditions on a set S of terms, called stability, that are necessary and sufficient for the following Relative Normalization (RN for short) 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. Roughly, S is stable if it is closed under reduction (this condition can be relaxed

⋆ This work was supported by the Engineering and Physical Sciences Research Council of Great Britain under grant GR/H 41300

slightly) and any step u entering S is S-needed. 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.

In [GlKh96], the authors further generalized the theory of relative normalization by abstracting from the structure of terms. They study relative normalization in Deterministic Residual Structures (DRSs), and Deterministic Family Structures (DRSs). DRSs are Abstract Reduction Systems (ARSs) where the residual relation on redexes is axiomatized in a way that enables one to define permutationequivalence on reductions; DFSs are DRSs where in addition Lévy’s notion of redex-family is also axiomatized. They proved the RN theorem for stable DRS, for regular stable sets R of final terms, and for DFSs for all stable sets S of final terms. Here a stable set S is regular if S-unneeded redexes cannot duplicate S-needed ones.

Here we study reductions from a term t to an arbitrary term s, assuming such a reduction exists. If the set {s} is stable, such as when s is a normal form, then existing theory can be applied. Otherwise, if the reduction graph G_{s} of s is stable and regular, then the task can be reduced to construction of a minimal (w.r.t. Lévy’s ordering ⊴ on reductions) G_{s}-normalizing reduction [GlKh95], since it must end at s. However, as we already know [GlKh94], G_{s} need not be stable, mainly because of syntactic accidents [Lév80]. For example, the graph {I(x), x} of s = I(x), in the TRS with the rule I(x) → x, is not stable, since t = I(I(x)) can be reduced to s by contracting either redex. Neither

of the two redexes in t is G_{s}-needed, and neither of the two reductions u : t → →^{I(I(x))}s and v : t → →^{I(x)} s is G_{s}-minimal – we have u ⋬ v, v ⋬ u, and u ≉_{L} v.

A constructive approach is to develop a neededness theory relative to particular reductions P : t → → s, or more precisely, relative to Lévy-equivalence classes ⟨P ⟩_{L} of reductions P, which are elements of Lévy’s reduction space ordered by ⊴. (Hence the name – discrete normalization.) We cannot aim at developing a needed strategy constructing a reduction from t to s because a redex in t contracted in every reduction from t to s may not exist, as is the case for the terms t = I(I(x)) and s = I(x).^{2} Furthermore, the task of construction of a reduction Lévy-equivalent to a given one makes sense also for infinite reductions.

First of all, for any given non-empty reduction P : t → → in a DRS R, finite or infinite, we prove existence of P -needed redexes in t, i.e., redexes whose at least one residual is contracted in every reduction in ⟨P ⟩_{L}. (Under an ‘infinite’ reduction we mean a reduction of the length ω.) We need the DRS to be stable [GlKh96] – redexes cannot arise from unrelated sources. Only when P is finite, we use the acyclicity property of DRSs – distinct redexes cannot mutually erase one another.

Next, for any co-initial Q and P with Q ⊴ P, we define the P -needed variant of Q. The Q-needed variant of Q, i.e., the self-needed variant of Q, written as SE(Q), then contracts redexes which are Q-needed and Q-erased (Q-erased are redexes that do not have residuals in some later terms of Q). We show existence of SE(Q) for any Q : t → → by showing that at least one of Q-needed redexes in t is Q-erased. For this we need the DRS to be in addition semi-linear – for any P : t → → , P -unneeded steps in P cannot duplicate P -needed redexes. This condition is however not very restrictive, since all known orthogonal rewrite systems are semi-linear stable DRSs.

We show that SE(Q) is self-essential in the sense that ‘omission’ of any step in SE(Q) would result into a reduction which is no more Lévy-equivalent to SE(Q). Because of that property, selfessential (and, equivalently, self-needed) reductions play the role of standard reductions in DRSs, since we do not impose any nesting relation on redexes in DRSs, and cannot speak on ‘outsidein’ reductions, as is done in [GLM92]. (Because of this, on the other hand, our DRSs cover more transition systems than those considered in [GLM92]) We show that SE(Q) ⊴ Q, and that the converse needs to be true only when Q is finite. This means that, surprisingly, if Q is infinite, construction of a reduction in ⟨Q⟩_{L} needs contraction of Q-unneeded redexes as well. Therefore, we have the Standardisation Theorem for stable semi-linear DRSs, and conclude that Infinitary Standardization Theorem cannot be proved, whichever existing notion of standardization, even in

2 However, ‘normalization via necessary sets’ approach of [SeRa90] may be useful here.

orthogonal TRSs.

To study discrete normalization, we extend the notion of fairness of computation to the notion of P -fairness or ⟨P ⟩_{L}-fairness for any finite or infinite P. We define P -fair reductions to be the reductions that contract only P -erased redexes and erase all such redexes. Fair reductions are then fair w.r.t. strongly cofinal reductions, i.e., reductions which are maximal w.r.t. ⊴. We show that P -fair reductions are exactly reductions in ⟨P ⟩_{L}. Therefore, a Gross-Knuth like strategy which in each multi-step contracts all P -erased redexes in every term yields reductions Lévy-equivalent to P. If (and only if) P is finite, we moreover show that contraction of P -needed P -erased redexes (sequentially) eventually yields a reduction in ⟨P ⟩_{L}. However, even if P is finite, contraction of arbitrary P -needed redexes (which need not be P -erased) may result in a reduction that is strictly greater (w.r.t. ⊴) than P; therefore, a ‘P -needed strategy’ need not be ‘P -normalizing’. When P is normalizing or fair, then our Discrete Normalization Theorem becomes the Normalization theorem, and gives the familiar Gross-Knuth algorithm for construction of fair reductions, respectively.

The paper is organized as follows. In the next section, we recall the definition of DRSs. In Section 3, we study relative properties of discrete neededness, essentiality and erasure, and show existence of P -needed redexes for any finite or infinite P in a stable DRS. Section 4 is devoted to the standardization and related results, which are used in Section 5 to prove the Discrete Normalization Theorem, the main result of this paper. Conclusions appear in Section 6.

2 Deterministic Residual Structures

In this section we recall Deterministic Residual Structures (DRSs), introduced in [GlKh96] but largely based on [Lév80]. DRSs are Abstract Reduction Systems (ARSs) with axiomatized notions of residual.

The definition and some results about ARSs can be found e.g., in [Klo92]. Our definition is slightly different. An ARS is a triple A = (Ter,Red,→) where Ter is a set of terms, ranged over by t, s, o, e; Red is a set of redexes (or redex occurrences), ranged over by u, v, w; and →: Red → (T er × T er) is a function such that for any t ∈ T er there is only a finite set of u ∈ Red such that → (u) = (t, s), written t→^{u}s. This set will be known as the redexes of term t, where u ∈ t denotes that s is a member of the redexes of t and U ⊆ t denotes that U is a subset of the redexes. Note that → is a total function, so one can identify u with the triple 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. |P | denotes the length of P. P ≤ Q denotes that P is an initial part of Q. ∅_{t} denotes the empty reduction starting from t. We use U, V, W to denote sets of redexes of a term.

DRSs are similar to Stark’s Determinate Concurrent Transition Systems [Sta89], to Abstract Reduction Systems of Gonthier et al. [GLM92], and to van Oostrom’s Descendant Rewriting Systems [Oos94]. The main difference from DCTSs is that Stark considers a non-duplicating residual relation (and we do not distinguish a start state). The difference from ARSs of [GLM92] is that we do not have a nesting relation on redexes and the corresponding axioms, 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, not only the notion of residual of redexes.

Definition 2.1 (Deterministic Residual Structure) A Deterministic Residual Structure (DRS) is a pair R = (A, /), where A is an ARS and / is a residual relation on redexes relating redexes in the source and target term of every reduction t→^{u}s ∈ A, such that for v ∈ t, the set v/u of residuals of v under u is a set of redexes of s; a redex in s may be a residual of only one redex in t under u, and u/u = ∅. If v has more than one u-residual, then u duplicates v. If v/u = ∅, then u erases v. A redex of s which is not a residual of any v ∈ t under u is said to be created by u. The set of residuals of a redex under any reduction is defined by transitivity.

A development of a set U of redexes in a term t is a reduction P : t → → that only contracts residuals of redexes from U; the development P is complete if U/P, the set of residuals under P of redexes from U, is empty ∅. Development of ∅ is identified with the empty reduction. U will also denote a complete development of U ⊆ t. The residual relation satisfies the following two axioms, called Finite Developments (FD) [GLM92] and acyclicity (which appears as axiom (4) in [Sta89]):

• [FD] All developments are terminating; all co-initial complete developments of the same set of redexes end at the same term; and residuals of a redex under all complete co-initial developments of a set of redexes are the same.

• [acyclicity] Let u, v ∈ t, let u ≠ v, and let u/v = ∅. Then v/u ≠ ∅.

The properties of the residual relation are all standard, and we refer to [HuLé91, Lév78, Lév80, Sta89] for details. Hence, we assume that, in a DRS R, the residual relation on redexes is extended to all co-initial reductions as follows: (P_{1}+P_{2})/Q = P_{1}/Q+P_{2}/(Q/P_{1}) and P/(Q_{1}+Q_{2}) = (P/Q_{1})/Q_{2}, and that Lévy-equivalence or permutation-equivalence is defined as the smallest relation on co-initial reductions satisfying: U + V/U ≈_{L} V + U/V and Q ≈_{L} Q′ ⇒ P + Q + N ≈_{L} P + Q′ + N, where U and V are complete developments of redex sets in the same term. Further, one defines P ⊴ Q iff P/Q = ∅, and can show that P ≈_{L} Q iff P ⊴ Q and Q ⊴ P; and P ⊴ Q iff Q ≈_{L} P + N for some N. The above relations can equivalently be defined also using Klop’s method of commutative diagrams. We will often use Klop’s diagrams in definitions and proofs. The method is well described in [Klo80, Bar84].

In practice, we are only interested in stable DRSs where a given redex cannot arise from two unrelated sources:

Definition 2.2 [GlKh96] A DRS is stable if the following axiom is satisfied:

• [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.

[figure: t; u; e; w; s; v; u/v; o; v/u; w/(v/u)]

The essence of stability is better understood via Lemma 2.2 below which expresses the preservation of externality during redex creation. For syntactic systems externality is a natural concept relating to overlap between components of terms involved in reduction steps. In an abstract setting it expresses the absence of shared (residuals of) redexes.

Definition 2.3 ([GlKh96]) • Let u ∈ U ⊆ t and P : t → → . We call P external to U (resp. u) if P does not contract residuals of redexes in U (resp. residuals of u).

• Let P : t_{0} → →^{P_{i}} t_{i}→^{u_{i}}t_{i+1} → → and Q : t_{0} = s_{0} → →^{Q_{j}} s_{j}→^{v_{j}}s_{j+1} → → . We call P external to Q if for any

i, j, u_{i}/(Q_{j}/P_{i})∩v_{j}/(P_{i}/Q_{j}) = ∅ (see the diagram, where U_{i,j} = u_{i}/(Q_{j}/P_{i}) and V_{i,j} = v_{j}/(P_{i}/Q_{j})).

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

[figure: Q′_{j}; P_{i}/Q_{j}; Q_{j}/P_{i}; U_{i,j}]

[figure: v_{j}; V_{i,j}]

[figure]

Obviously, P is external to the set U iff it is external to any development of U, and is external to a redex u iff it is external to the reduction contracting u.

Lemma 2.1 ([GlKh96]) Let P : t → → s be external to a complete development of F ⊆ t, in a DRS, and let Q : t → → o, then P/Q is external to F/Q.

Lemma 2.2 (External redex-creation) ([GlKh96]) 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.

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 [Klo80, Kha92, Nip93], and Orthogonal Term Graph Rewriting Systems (OTGRSs)

[KKSV93] form DRSs; OTGRSs are equivalent to Maranget’s orthogonal DAG (Directed Acyclic Graph) rewriting systems, defined via labelled orthogonal TRSs. All these are stable, and can be shown so without using any notion of labelling.

We extend some of the earlier notions to infinite reductions, denoted by t → → ∞.

Definition 2.4 • Let P : t → → ∞ and Q : t → → s. Then P/Q is the reduction whose initial parts are residuals of initial parts of P under Q.

• If u ∈ t, then u/P = ∅ if u/P′ = ∅ for some finite initial part P′ of P.

• If at least one of co-initial N and N′ is infinite, then one defines N ⊴ N′ or equivalently N/N′ = ∅ if, for any redex v contracted in N, v/(N′/N_{1}) = ∅, where N = N_{1} + v + N_{2}. N and N′ are Lévy-equivalent, N ≈_{L} N′, if N ⊴ N′ and N′ ⊴ N. (One checks easily that ⊴ is a partial order, and ≈_{L} is an equivalence relation.)

3 Existence of Discretely Needed Redexes

In this section, we characterise some properties of a redex with respect to possible reductions in a DRS. In particular, we define P -needed redexes, for any reduction P, and then prove existence of P -needed redexes for any P in a stable DRS.

3.1 Discrete Notions of Neededness and Essentiality

We define P -needed, P -essential, and P -erased redexes, for any reduction P, and study their (relative) properties.

Definition 3.1 • Let P : t → → and u ∈ t, in a DRS. We call u erased in P or P -erased if u/P = ∅. We say that P discards u if P is external to u and erases it [GlKh95].

• We call u P -needed, written NE_{P} (u, t), if there is no Q ≈_{L} P that is external to u, and call it P -unneeded, UN_{P} (u, t), otherwise. We call u P -essential, ES_{P} (u, t), if there is no Q ≈_{L} P that discards u, and call it P -inessential, IE_{P} (u, t), otherwise.

We extend these concepts to reductions co-initial with those containing u as a redex of one of its terms.

• Let Q : t → → , P : t → →^{P′} s → → , and u ∈ s. We say NE_{Q}(u, s) if NE_{Q/P′}(u, s). We call P

Q-needed if so is every redex contracted in P. We call P self-needed if it is P -needed. The other concepts above are extended in the same way.

Note that P -neededness, P -erasure, and P -essentiality do not depend on the choice of a reduction in the class ⟨P ⟩_{L} of reductions Lévy-equivalent to P – so one can speak of ⟨P ⟩_{L}-neededness, ⟨P ⟩_{L}- essentiality and ⟨P ⟩_{L}-erasure, respectively.

Lemma 3.1 Let u ∈ t → →^{P} , in a DRS.

(1) If u is P -erased and P -essential, then it is P -needed.

(2) If u is P -needed, then it is P -essential.

Proof. (1) Suppose on the contrary that UN_{P} (u, t), i.e., ∃Q ≈_{L} P: Q is external to u. Since u/P = ∅, we have u/Q = ∅, i.e., Q discards u – a contradiction, since ES_{P} (u, t). (2) If u is P -inessential, then there is Q ≈_{L} P that discards u; thus Q is external to u, and u is P -unneeded – a contradiction.

Lemma 3.2 Let u ∈ t → →^{P} . Then u is P -erased iff (α) every residual of u along any Q ≈_{L} P is either Q-needed or Q-inessential.

Proof. (⇒) Let u be P -erased, and suppose on the contrary that u doesn’t satisfy (α), i.e., there are Q = Q′ + Q′′ ≈_{L} P and u′ ∈ u/Q′ such that u′ is Q′′-unneeded and Q′′-essential. Hence, there is Q^{∗} ≈_{L} Q′′ that is external to u′ (since u′ is Q′′-unneeded) and u′/Q^{∗} ≠ ∅ (since u′ is Q′′-essential). Hence, by CR for residuals, u/P = u/(Q′ + Q^{∗}) ≠ ∅ – a contradiction. (⇐) By induction on the length of P. Obviously, P cannot be empty, so let P = v + P′. Since u satisfies (α), so does every v-residual of u. By the induction assumption, (u/v)/P′ = ∅. Hence u/P = ∅.

Note that P -needed redexes need not be P -erased in a DRS with a duplicating residual relation. We show this using an OTRS, an example of a DRS, defined using a rule set R = {f(x) → x, g(x) → x}, with the usual residual relation, and using subterms to label redexes. Consider:

P : t = f(g(x)) → h(g(x), g(x)) → h(x, g(x))

Here g(x) ∈ t is P -needed, but not P -erased. Note also that P -essential redexes need not be P - needed. For:

P : u = f(g(x)) → f(x)

in R = {f(x) → x, g(x) → x}, redex u is not P -needed , but it is P -essential. However, for the redexes contracted in P (not the redexes whose residuals are contracted in P), P -neededness and P -essentiality do coincide:

Lemma 3.3 Let P : s → → t→^{u}e → → , in a DRS. Then NE_{P} (u, t) iff ES_{P} (u, t).

Proof. It is enough to consider the case when u is the first step in P. (⇒) From Lemma 3.1.(2). (⇐) From Lemma 3.1.(1), since u is erased in P.

Corollary 3.1 A reduction P in a DRS is self-needed iff it is self-essential.

3.2 Neededness in Deterministic Residual Structures

We now embark on proving existence of P -needed redexes for any P : t → → in a stable DRS, using the notion of redex-chains, which we introduce for this purpose.

The idea of our proof for finite P is simple, and resembles that for normalizing reductions [GlKh96]. We show that the last step of P is P -needed, and that any P -needed redex in a non-initial term of P is either a residual of such a redex in the preceding term, or is created by contraction of a P -needed redex; therefore the redex in t ‘responsible’ for the last step of P is needed.

When P is infinite, we show existence of a redex in u ∈ t which is responsible for at least one redex in every term of P, and show that at least one such redex is P -needed.

Lemma 3.4 Let P : s → → t→^{u}e → →^{P^{∗}} , in a stable DRS, and let v ∈ e be created by u. If u is P -unneeded (resp. P -inessential), then so is v.

[figure: s; t; u; e; P^{∗}; P]

[figure: Q′_{t}; ∅; Q′_{e}]

[figure: Q_{t}; Q_{e}]

Proof. If u is P -unneeded, then it is P -inessential by Lemma 3.3. Hence there is Q_{t} ≈_{L} u + P^{∗} that discards u. By Lemma 2.2, Q_{e} = Q_{t}/u is external to v, and by Definition 2.4 Q_{e} ≈_{L} P^{∗}. Hence v is P -unneeded. In order to show that v is P -inessential, it is enough to show that v/Q_{e} = ∅. We will show that v/Q′_{e} = ∅, where Q′_{e} = Q′_{t}/u and Q′_{t} ≤ Q_{t} is finite and such that u/Q′_{t} = ∅. Indeed, if on the contrary v/Q′_{e} ≠ ∅, then by Lemma 2.2 the redexes in v/Q′_{e} must be created by u/Q′_{t}, which is not possible since u/Q′_{t} = ∅.

Below we use the fact that Lévy-equivalent reductions P, Q : t → → s are Hindley-equivalent, written P ≈_{H} Q, i.e., for any u ∈ t, u/P = u/Q.

Lemma 3.5 Let P : s → → t→^{u}e → →^{P^{∗}} , and let v ∈ e be a u-residual of w ∈ t. If w is P -unneeded (resp. P -inessential), then so is v.

Proof. Since w is P -unneeded, there is Q_{t} ≈_{L} u + P^{∗} that is external to w (see the picture for Lemma 3.4). Hence u/Q_{t} = ∅ (since u/(u + P^{∗}) = ∅) and Q_{e} = Q_{t}/u ≈_{L} P^{∗} by Definition 2.4. By Lemma 2.1 Q_{e} is external to v. Thus v is P -unneeded too. If moreover w is P -inessential, then say Q_{t} ≈_{L} u + P^{∗} discards it, and let Q′_{t} ≤ Q_{t} be finite and such that w/Q′_{t} = ∅. Then v/(Q′_{t}/u) = ∅ since Q′_{t} ≈_{H} u + Q′_{t}/u, i.e., Q_{e} discards v, and v is P -inessential.

Lemma 3.6 Let P : t→^{u}e → →^{P^{∗}} , let NE_{P} (v, t) (resp. ES_{P} (v, t)). If v ≠ u, then v has at least one u-residual v′. If v′ is the only u-residual of v, then NE_{P} (v′, e) (resp. ES_{P} (v′, e)).

Proof. If on the contrary v/u = ∅, then P would discard v, contrary to NE_{P} (v, t) (resp. ES_{P} (v, t)). If v′ is the only u-residual of v then if v′ was P^{∗}-unneeded (P^{∗}-inessential), there would be Q_{e} ≈_{L} P^{∗} that is external to v′ (resp. that discards v′). Then u+Q_{e} would be external to (resp. would discard) v – a contradiction.

Now we define the notion of redex-chains, which enable us to trace back the origins of redexes in earlier terms in a reduction:

Definition 3.2 let P : t_{0} → →^{u_{0}} t_{1} → →^{u_{1}} → → and let v_{i} ∈ t_{i} be such that either v_{i+1} is a u_{i}-residual of v_{i}, or v_{i} = u_{i} and u_{i} creates v_{i+1}. Then we call the sequence Γ = v_{0}, v_{1}, … a chain in P or a P -chain or a P -chain of v_{0}. We call v_{j} a (P −)successor of v_{i} if there is at least one creation in the chain v_{i}, v_{i+1}, …, v_{j}, i.e., u_{k} = v_{k} for at least one i ≤ k < j. We call v_{i} the predecessor of v_{j} if v_{j} is a successor or a residual of v_{i} (obviously, every redex in t_{j} has exactly one predecessor in every t_{i} with i < k). The degree of Γ, written deg(Γ), is the number of creations in Γ.

Lemma 3.7 Let Γ be a P -chain, in a stable DRS, and let v ∈ Γ be P -needed (resp. P -essential). Then so is every predecessor of v in Γ.

Proof. By Lemmas 3.4 and 3.5.

Lemma 3.8 Let P : t → → s, and let v ∈ s be a P -successor of u ∈ t, in a stable DRS. Then u is P -needed.

Proof. Let v belong to a P -chain Γ of u with a positive degree, and suppose on the contrary that there is Q ≈_{L} P that is external to u. Let P : t → →^{P′} o→^{w}e → →^{P^{∗}} s, where w is the last member of Γ that is contracted in P and creates the next member of Γ (see the diagram). Since Q is external to u, Q′ = Q/P′ is external to w by Lemma 2.1 and Lemma 2.2. By definition of w, it creates a redex v′ ∈ e whose residual is v. Since Q^{∗} = Q/(P′ + w) ≈_{L} P^{∗} and therefore v is Q^{∗}-residual of v′ as well, we have by Lemma 2.2 that, along Q′ + w/Q′, v is created by w/Q′. But this is impossible since w/Q′ = ∅ – a contradiction.

[figure: t; P′; o; e; P^{∗}; s; s; Q; ∅; s; Q′; ∅; s; Q^{∗}; ∅; s; ∅]

Lemma 3.9 Let u ∈ t_{0} → →^{P} t_{k}, and let P be external to u, in a DRS. Then u ≉_{L} P.

Proof. Let P : t_{0}→^{v_{0}}t_{1}→^{v_{1}} … → t_{k}. We show that P/u = ∅ implies u/P ≠ ∅ by induction on the number of elementary diagrams in Klop’s diagram D(u, P) of u and P. It follows from Definition 2.3 that the top and left edges of all sub-diagrams of D(u, P) are external reductions, therefore the induction principle is sound. So let P/u = ∅. If |P | = 1, i.e., P = v_{0}, we have u/v_{0} ≠ ∅ by [acyclicity]. So let |P | > 1, let P : t_{0} → →^{Q} t_{k−1} →^{v_{k−1}}t_{k}, and let U = u/Q (see the diagram). By the induction assumption, U ≠ ∅. So let U = U′ + u′, where u′ is the last (non-empty) step of U, and let V = v_{k−1}/U′. Again by the induction assumption, u′/V ≠ ∅. Hence u/P ≠ ∅.

[figure: t_{0}; Q; t_{k−1}; v_{k−1}; t_{k}]

[figure: U′; V]
[figure: s; u; ∅; s; u′; ∅; s]

Lemma 3.10 Let P : t → → s→^{u}o, in a DRS. Then u is P -needed.

Proof. By Lemma 3.9, there is no Q : s → → o such that Q is external to u and Q ≈_{L} u. Hence u is u-needed, i.e., P -needed.

We turn to properties of infinite reductions.

Lemma 3.11 For any infinite P : t → → ∞ in a DRS, there is at least one u ∈ t that has a chain of infinite degree along P.

Proof. If every redex in t had only chains of finite degrees, then there will be a term s in P such that in the tail P′ of P starting from s there will not be redex creation, i.e., P′ would be an infinite development – contradicting [FD].

Lemma 3.12 Let P : t → → ∞ and let u have an infinite P -chain Γ, in a stable DRS. Then ES_{P} (u, t). If moreover deg(Γ) > 0, then NE_{P} (u, t).

Proof. Suppose on the contrary that IE_{P} (u, t). Then there is a Q ≈_{L} P that discards u. Hence there is a finite Q′ < Q that discards u. Thus there are P′ < P and N′ such that Q′ + N′ ≈_{L} P′. Let Γ′ be the part of Γ corresponding to P′. If deg(Γ′) = 0, then Γ′ consists of residuals of u, and Q′ cannot discard u since Q′ + N′ ≈_{L} P′ and u/P′ ≠ ∅; and if deg(Γ′) > 0, Q′ cannot discard u since u is P′-needed by Lemma 3.8 – a contradiction. Thus ES_{P} (u, t). Now assume deg(Γ) > 0. Then a successor v of u in Γ is contracted in P. As we have already shown, ES_{P} (v, t) since v has an infinite chain as well. Hence, by Lemma 3.3, v is P -needed, and u is P -needed by Lemma 3.7.

Theorem 3.1 Let P : t → → be a non-empty reduction in a stable DRS. Then t contains a P -needed redex.

Proof. If P is finite, then by Lemma 3.10 its last step is P -needed, and its predecessor in t is P - needed by Lemma 3.7. If P is infinite, then by Lemma 3.11 there is a redex u ∈ t that has an infinite chain Γ of a positive degree, and NE_{P} (u, t) by Lemma 3.12.

4 Standardization

In orthogonal ‘syntactic’ rewrite systems, if a reduction P : t → → s discards a redex u ∈ t, then one easily constructs a Q ≈_{L} P that discards u and doesn’t contract redexes inside u (see e.g., [GlKh94]), and clearly such a Q discards all redexes in the arguments of u. In DRSs, where we do not have a nesting relation on redexes, the above property can be approximated by saying that ‘P -inessential redexes cannot duplicate P -essential ones’ (obviously, P -inessential redexes cannot erase P -essential ones). It follows from Lemma 3.3 that the [semi-linearity] axiom introduced below and used essentially in our standardization procedure expresses the above property of orthogonal rewrite systems, and is a slightly weaker condition.

Definition 4.1 We call a DRS R semi-linear if it satisfies the following axiom:

• [semi-linearity] Let P : t→^{u}s → → in R. If u is P -unneeded, then u does not duplicate P -needed redexes in t.

Below, if not otherwise stated, we only consider semi-linear stable DRSs. Obviously, linear systems (having a non-duplicating residual relation) are trivially semi-linear.

Theorem 4.1 Let P : t → → be a non-empty reduction in a stable semi-linear DRS. Then t contains a P -erased P -needed redex; for example, the P -needed redex in t whose residual is contracted first among residuals of P -needed redexes in t.

Proof. Let P : t = t_{0}→^{u_{0}}t_{1}→^{u_{1}} …, and let u_{i} be the first among the contracted residuals of P -needed redexes in t_{0}. By Theorem 3.1, t_{0} contains a P -needed redex, and at least one residual of each P - needed redex in t_{0} is contracted in P; thus the redex u_{i} as above exists. Let u_{i} be the residual of v ∈ t_{0}. By Lemma 3.5 and Lemma 3.4, every u_{j} with j < i is P -unneeded. By [semi-linearity] and Lemma 3.6, u_{i} is the only residual of v in t_{i}, and is P -needed. Hence v is P -erased (and P -needed).

Note that for any finite P : t → → s, P -needed redexes all of whose residuals along P remain P -needed, are P -erased, since s does not contain ∅-needed redexes.

Definition 4.2 (1) Let P : t → → and Q ⊴ P. The P -needed variant of Q, written SE_{P} (Q), is defined as follows: let v ∈ t be such that it is P -needed and its residual is contracted in Q first among P -needed residuals of P -needed redexes in t. Then SE_{P} (Q) = v + SE_{P/v}(Q/v). If there is no such a redex in t, then SE_{P} (Q) = ∅.

(2) We call SE_{P} (P) the self-needed variant of P and denote it by SE(P).

Obviously, a reduction P is self-needed iff SE(P) = P.

Lemma 4.1 Let P, Q : t → → , in a DRS. Then Q is P -erased iff Q ⊴ P.

Proof. Immediate from Definition 3.1.

Lemma 4.2 Let Q ⊴ P. Then SE_{P} (Q) is a P -erased P -needed reduction, and its length coincides with the number of P -needed steps in Q.

Proof. Let Q : t = t_{0} → →^{Q_{i}} t_{i}→^{u_{i}}t_{i+1} → →^{Q_{i+1}^{∗}}, and let u_{i_{0}}, u_{i_{1}}, … be all the P -needed steps in Q (i_{0} < i_{1} <

…). Since u_{i_{0}} is the first P -needed step in Q, it follows from Lemma 3.5 and Lemma 3.4 that u_{i_{0}} is a residual of some P -needed redex v_{0} ∈ t_{0}, and u_{i_{0}} is the only residual of v_{0} by [semi-linearity].^{3} Hence v_{0} is P -erased. Thus SE_{P} (Q) = v_{0} + SE_{P/v_{0}}(Q/v_{0}) where v_{0} is P -needed and P -erased. Similarly, we show that SE(P) : t_{0} = s_{0}→^{v_{0}}s_{1}→^{v_{1}}s_{2} → → , where u_{i_{j}} is the first P′_{j}-needed step in Q′_{j} = Q/(v_{0} + v_{1} + … + v_{j−1}), where P′_{j} = P/(v_{0} + v_{1} + … + v_{j−1}), and u_{i_{j}} is the only residual of some P -erased P -needed redex v_{j} ∈ s_{j} along Q′_{j}. (Note that P_{j} ≈_{L} P, so P_{j}-neededness coincides with P -neededness.) Hence the lemma.

[figure: t_{0} = s_{0}; Q_{i_{j}}; t_{i_{j}}; u_{i_{j}}; t_{i_{j}+1}; Q_{i_{j}+1}^{∗}; Q′_{0} = Q]

[figure: s_{j}; t_{i_{j}}; ∅; u_{i_{j}}; t_{i_{j}+1}; Q_{i_{j}+1}^{∗}; Q′_{j}]

[figure: s_{j+1}; v_{j}; t_{i_{j}}; u_{i_{j}}; ∅; t_{i_{j}+1}; ∅; Q_{i_{j}+1}^{∗}; Q′_{j+1}]

v_{j+1}

Lemma 4.3 (1) If P is finite, then so is SE(P), and P ≈_{L} SE(P).

(2) If |P | = ∞, then so is SE(P), and SE(P) ⊴ P, but P ≈_{L} SE(P) need not hold.

3 Here we also use the fact that Q ⊴ P, so that every finite initial part of Q can be considered as being an initial part of P, up to ≈_{L}, and lemmas 3.5 and 3.4 apply; recall that discrete neededness is invariant under ≈_{L}.

Proof. By Lemma 4.2, SE(P) is P -erased, and SE(P) ⊴ P by Lemma 4.1. Let P : t_{0} → →^{P_{i}} t_{i}→^{u_{i}}t_{i+1} → → and let u_{i_{0}}, u_{i_{1}}, … be all P -needed steps in P (i_{0} < i_{1} < …). Then, as shown in the proof of Lemma 4.2, SE(P) : t_{0} = s_{0}→^{v_{0}}s_{1}→^{v_{1}}s_{2} → → , where u_{i_{j}} is the first P′_{j}-needed step in P′_{j} = P/(v_{0} + v_{1} + … + v_{j−1}), and u_{i_{j}} is a residual of v_{j} along P′_{j} (see also the above diagram; take Q = P).

(1) Let u_{i_{0}}, u_{i_{1}}, …, u_{i_{k−1}} be all P -needed steps in P. Then SE(P) : t_{0} = s_{0}→^{v_{0}}s_{1}→^{v_{1}}s_{2} … →^{v_{k−1}}s_{k}

and s_{k} does not contain P/SE(P)-erased P/SE(P)-needed redexes by Definition 4.2. Hence, by Theorem 4.1, P/SE(P) = ∅. Thus in this case P ≈_{L} SE(P).

(2) Let P be infinite. It follows from the proof of Theorem 4.1 that P contracts infinitely many P -needed redexes. Thus SE(P) is infinite by Lemma 4.2. In order to show that P ≈_{L} SE(P) need not hold, consider the OTRS R = {r_{1} : f(x) → g(h(x)), r_{2} : g(x) → f(h(x)), r_{3} : h(x) → a} and the reductions P : f(x) → g(h(x)) → g(a) → f(h(a)) → f(a) → g(h(a)) → g(a) → … and Q : f(x) → g(h(x)) → f(h(h(x))) → g(h(h(h(x)))) → . . .. Then it is easy to check that Q = SE(P), but P/Q ≠ ∅.

Corollary 4.1 For any finite P, Q, P ≈_{L} Q iff SE(P) ≈_{L} SE(Q).

Lemma 4.4 Let Q be P -needed and Q ⊴ P. Then Q is Q-needed.

Proof. Suppose on the contrary that Q has a Q-unneeded step, say u, and let Q = Q′ + u + Q′′. By Lemma 3.3, u is Q-inessential, i.e., there is N ≈_{L} u + Q′′ that discards u. Let N′ ≤ N be finite and discard u. Since Q ⊴ P, it follows that N ⊴ P′, where P′ = P/Q′. Hence P′ ≈_{L} N′ + N′′ for some N′′. This means that u is P′-inessential, hence P -inessential, and is P -unneeded by Lemma 3.1.(2)

– a contradiction.

Corollary 4.2 If Q ⊴ P, then SE_{P} (Q) is self-needed, and hence self-essential.

Proof. By Lemma 4.2 and Lemma 4.1, SE_{P} (Q) ⊴ P and SE_{P} (Q) is P -needed. Hence SE_{P} (Q) is self-needed by Lemma 4.4, and is self-essential by Corollary 3.1.

It is easy to see that standard reductions, in the sense of [GLM92], are self-essential. In fact, the notion of self-essential reduction is the best approximation to the notion of standard reduction for DRSs, and it captures the essence of standardization in many respects. Therefore:

Definition 4.3 We call a reduction in a DRS standard if it is self-essential.

Before proving the Standardization theorem, we need a few simple lemmas concerning fair reductions.

Definition 4.4 A reduction P : t_{0} → t_{1} → … in a DRS is fair if every redex in any t_{i} is P - erased [Klo92]. We call P strongly cofinal if, for any Q : t_{0} → → , Q ⊴ P.

Lemma 4.5 Let u ∈ t → →^{P} in a DRS. If P is fair, then so is P/u.

Proof. Since P is fair, u/P = ∅, i.e., u/P′ = ∅ for some finite P′ where P = P′ + P^{∗}. Thus P/u = P′/u + P^{∗}, and the lemma follows from the fact that for any N = N′ + N^{∗}, N is fair iff N^{∗} is also.

Lemma 4.6 A reduction P in a DRS is fair iff it is strongly cofinal.

Proof. Let P : t_{0} → →^{P_{i}} t_{i}→^{u_{i}}t_{i+1} → →^{P_{i+1}^{∗}} and Q : t_{0} = s_{0} → →^{Q_{j}} s_{j}→^{v_{j}}s_{j+1} → →^{Q_{j+1}^{∗}}. (⇒) We need to show that

Q ⊴ P. Indeed, by Lemma 4.5, P/Q_{j} is fair (for all appropriate j), and hence u_{j}/(P/Q_{j}) = ∅, i.e., Q ⊴ P. (⇐) If P is strongly cofinal, then P_{k} + w_{k} ⊴ P for any w_{k} ∈ t_{k}, i.e., w_{k} ⊴ P_{k}^{∗}. Thus every redex in P is P -erased, and P is fair.

Definition 4.5 Let u ∈ t, in a DRS. We call u inessential if there is P : t → → that discards u, and call it essential otherwise.

Lemma 4.7 Let u ∈ t and let P : t → → be strongly cofinal, in a DRS. Then u is inessential iff it is P -inessential.

Proof. (⇒) Since u is inessential, there is Q : t → → s that discards u. Hence, for any strongly cofinal N : s → → , Q + N discards u and is strongly cofinal. Hence u is P -inessential (since P ≈_{L} Q + N). (⇐) Immediate.

Theorem 4.2 (Standardization) For any finite reduction P in a stable semi-linear DRS, SE(P) is a standard reduction Lévy-equivalent to P. If P is infinite, a standard reduction Lévy-equivalent to it need not exist.

Proof. If P is finite, then P ≈_{L} SE(P) by Lemma 4.3, and SE(P) is self-essential by Corollary 4.2. Now let P be infinite, and take P and Q as in the example of Lemma 4.3. First note that P is fair, hence is strongly cofinal by Lemma 4.6. Therefore, any self-essential reduction Lévy-equivalent to P must be essential by Lemma 4.7, and must be infinite because P is so. But the argument of any redex in R is inessential: the reduction f(t) → g(h(t)) → g(a) discards the argument t of the r_{1}-redex f(t), hence IE(t, f(t)); and similarly for r_{2}- and r_{3}-redexes. Therefore, Q is the only infinite essential reduction in R. And we already know that P ≉_{L} Q.

We complete this section by a lemma used in the next section.

Lemma 4.8 Let P : t → → s be external to u ∈ t, in a DRS. Then, for any Q ≈_{L} P, SE(Q) is external to u.

Proof. By Definition 4.2, SE(Q) is Q-needed. But by Lemma 3.5 all residuals of u along SE(Q) are Q-unneeded. Hence SE(Q) is external to u.

Lemma 4.9 Let P : t→^{u}t′ → →^{P′} s, let v ∈ t, let u ≠ v, and let v be P -needed (resp. P -essential). Then v has at least one P -needed (resp. P -essential) u-residual in t′.

Proof. Suppose v/u = {v_{1}, …, v_{k}}, and suppose on the contrary that UN_{P} (v_{i}, P′) (resp. IE_{P} (v_{i}, P′)) for all 1 ≤ i ≤ k (k ≥ 1 by Lemma 3.6). Thus, for every i, there is P_{i} ≈_{L} P′ that is external to (resp. that discards) v_{i}. By Lemma 4.8, SE(P′) is external to all v_{i}, and u + SE(P′) is external to v (resp. and discards v since u + P_{i} ≈_{H} u + P′) – a contradiction, since P ≈_{L} u + SE(P′) and v is P -needed (resp. P -essential).

5 Discrete Normalization

This section is entirely devoted to proving the main result of the paper – the Discrete Normalization Theorem.

Definition 5.1 Let P, Q : t → → . We call Q P -fair if Q contracts only P -erased redexes, and every P -erased redex in any term of Q is erased in Q as well.

Lemma 5.1 Let P, Q : t → → , let P = u + P′, let Q′ = Q/u, and let Q be P -fair. Then Q′ is P′-fair (see the diagram).

Proof. Obviously Q is P -fair implies Q is P -erased. By Definition 2.4, P ⊴ Q implies P′ ⊴ Q′. Hence P′ is Q′-erased by Lemma 4.1. It remains to show that any P′-erased redex w′ in some term of Q′ is erased in Q′ too. Since u is P -erased, it is Q-erased by the assumption (Q is P -fair). So let Q^{∗} ≤ Q be finite and erase u, let Q = Q^{∗} + Q_{1}^{∗}, and let Q^{′∗} = Q^{∗}/u; hence Q′ = Q^{′∗} + Q_{1}^{∗}. We can assume that Q^{∗} is chosen so that w′ is in some term of Q^{′∗}. Let W′ be the set of residuals of w′ in the final term o of Q^{′∗}. Since w′ is P′-erased, so is W′ (i.e., W′/(P′/Q^{′∗}) = ∅). Since P/Q^{∗} ≈_{L} P′/Q^{′∗}, W′ is P -erased too. Since Q is P -fair by the assumption, W′ is erased in Q as well, i.e., W′/Q_{1}^{∗} = ∅. Hence W′ is erased in Q′, and so is w′.

[figure: u; P′]

[figure: o; Q^{∗}; ∅; o ⊇ W′; Q^{′∗} ∋ w′]

[figure: Q; Q_{1}^{∗}; Q′; Q_{1}^{∗}]

Lemma 5.2 Let P : t→^{u}e → → s and let Q : t → → ∞ be P -erased and P -needed. Then u + Q/u ⊴ P and it contracts infinitely many P -erased P -needed redexes.

Proof. We have Q ⊴ P by Lemma 4.1, and u + Q/u ⊴ P follows. Let Q : t = t_{0}→^{v_{0}}t_{1}→^{v_{1}} …, and let Q_{i} : t = t_{0}→^{v_{0}}t_{1}→^{v_{1}} … → t_{i}. If v_{i} ∉ u/Q_{i}, then it follows from Lemma 4.9 that v_{i} has at least one P -needed u/Q_{i}-residual, and that v_{i}/(u/Q_{i}) contracts at least one P -needed redex. Suppose on the contrary that there is only a finite number of such i. Then there is a k such that t_{k}→^{v_{k}}t_{k+1} →^{v_{k+1}} … is an (infinite) u/P_{k}-development. But this is impossible by [FD] – a contradiction.

Theorem 5.1 (Discrete Normalization) In semi-linear stable DRSs:

(1) Let P, Q : t → → . Then P ≈_{L} Q iff Q is P -fair. In particular, any multi-step reduction Q : t = t_{0} → → t_{1} → → … that contracts in parallel all P -erased redexes in every t_{i} is Lévy-equivalent to P.

(2) If P is finite, then any reduction t → → that contracts P -erased P -needed redexes eventually terminates in a reduction Lévy-equivalent to Q, even if a finite number of P -erased P -unneeded redexes, and only such, are also contracted.

(3) If Q contracts only P -erased P -needed redexes, and every such a redex is erased in it, then Q ⊴ P, but P ≈_{L} Q need not hold when P is infinite.

Proof. (1) (⇒) Let P ≈_{L} Q. Then Q/P = ∅, and Q is P -erased by Lemma 4.1. For any Q′ < Q,

P/Q′ ≈_{L} Q′′, where Q : t → →^{Q′} s → →^{Q′′} . Hence any P -erased redex u ∈ s is Q-erased too, i.e., Q is P - fair. (⇐) Q/P = ∅ follows from Lemma 4.1. So we have to show that P/Q = ∅. Let P = u+P′. Then since every P -erased redex of Q is erased in Q, we have that u/Q = ∅. By Lemma 5.1, Q′ = Q/u is P′-fair. Hence, we can show similarly that if P′ = u′ + P′′, then u′/Q′ = ∅, and so on. Thus P/Q = ∅. The rest of (1) is immediate.

(2) Suppose on the contrary that there is a P -erased reduction Q : t → → that contracts infinitely many P -erased P -needed redexes. Then, by Lemmas 4.2 and 5.2, there is an infinite P -erased P - needed reduction starting from s, i.e., an infinite ∅-erased ∅-needed reduction starting from s – a contradiction.

(3) Q ⊴ P follows from Lemma 4.1. The example in the proof of Lemma 4.3 is a counterexample for P ⊴ Q.

Let us call a reduction P self-neededly fair if no redex in a term of P has a P -needed P - erased residual in every subsequent term. Then it follows from the example of Lemma 4.3 that even self-neededly fair P -needed P -erased reductions need not be Lévy-equivalent to P. So (1) of Theorem 5.1 cannot be improved by considering self-neededly fair sequential reductions instead of multi-step reductions.

Finally, note that if the DRS is linear (i.e, non-duplicating), then the self-needed variant SE(P) of any finite reduction P is an optimal (i.e., shortest) reduction Lévy-equivalent to P. To show this, let P = u + P′ be self-needed, let Q ≈_{L} P, and assume that P′ is shortest in its Lévy-class. Then |Q/u| ≤ |Q| − 1 since exactly one residual of u is contracted in Q, and |P | ≤ |Q| follows from the induction assumption.

6 Conclusions and Future Work

We have proved an abstract Discrete Normalization theorem which gives an algorithm for constructing reductions Lévy-equivalent to a finite or infinite reduction P. The special cases which have already been studied are when P is normalizing or fair, and correspond to reductions maximal w.r.t ⊴. We introduce a number of concepts and constructs which are technically interesting in their own rights.

Both the axiomatic approach to the study of syntax of rewriting and other transition systems and the study of the theory of normalization by neededness can be continued in many directions, some of which are already mentioned in related papers [GlKh94, GlKh96, GlKh95]. Here we mention only two very closely related problems.

We have not addressed here the question of how to find efficiently P -needed P -erased redexes which are contracted in reductions Q ≈_{L} P, and a syntactic theory similar to the strong sequentiality theory [HuLé91, KlMi90] needs to be developed for discrete normalization.

Finally, one could try to develop a theory of normalization relative to sets Π of finite or infinite reductions which would unify discrete normalisation with the finitary relative normalisation of [GlKh96]. Thus by taking the set of all S-normalizing reductions for stable sets S of final terms, or taking a Lévy-equivalence class of reductions for Π, one would get the Relative and Discrete Normalization theorems, respectively.

References

[AnMi94] Antoy S. and Middeldorp A. A Sequential Reduction Strategy. In Proc. of the 4^{th} International Conference on Algebraic and Logic Programming, ALP’94, Madrid, Springer LNCS. vol. 850, p. 168-185, 1994.

[AEH94] Antoy S., Echahed R., Hanus M. A needed narrowing strategy. In: Proc. of the 21^{st} ACM Symposium on Principles of Programming Languages, POPL’94, Portland, Oregon, 1994.

[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.

[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.

[Gar94] Gardner P. Discovering needed reductions using type theory. In: Proc. of the 2^{nd} International Symposium on Theoretical Aspects of Computer Software, TACS’94, Springer LNCS, v. 789, M. Hagiya, J. C. Mitchell, eds. Sendai, 1994, p. 555-574.

[GlKh94] Glauert J.R.W., Khasidashvili Z. Relative Normalization in Orthogonal Expression Reduction Systems. In: Proc. of the 4^{th} International workshop on Conditional (and Typed) Term Rewriting Systems, CTRS’94, Springer LNCS, vol. 968, N. Dershowitz, N. Lindenstrauss, eds. Jerusalem, 1994, p. 144-165.

[GlKh96] Glauert J.R.W., Khasidashvili Z. Relative normalization in deterministic residual structures. In: Proc. of the 19^{th} International Colloquium on Trees in Algebra and Programming, CAAP’96, Springer LNCS, 1996, to appear. (Available as ftp://ftp.sys.uea.ac.uk/pub/glauert/CAAP.ps.gz)

[GlKh95] Glauert J.R.W., Khasidashvili Z. Minimal and optimal relative normalization in orthogonal Expression Reduction Systems. (Available as ftp://ftp.sys.uea.ac.uk/pub/glauert/MinOpt.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.

[Ken89] Kennaway J.R. Sequential evaluation strategy for parallel-or and related reduction systems. Annals of Pure and Applied Logic 43, 1989, p.31-56.

[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.

[KKSV93] Kennaway J. R., Klop J. W., Sleep M. R, de Vries F.-J. Transfinite reductions in orthogonal term graph rewriting. Information and Computation, To appear.

[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.

[Kha94] Khasidashvili Z. On higher order recursive program schemes. In: Proc. of the 19^{th} International Colloquium on Trees in Algebra and Programming, CAAP’94, Springer LNCS, vol. 787, S. Tison, ed. Edinburgh, 1994, p. 172-186.

[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.

[KlMi90] Klop J.W., Middeldorp A. Sequentiality in Orthogonal Term Rewriting Systems. Journal of Symbolic Computation 12, p. 161-195, 1991.

[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.

[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, Katholic 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 higher-order 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.

[SeRa90] Sekar R.C., Ramakrishnan I.V. Programming in Equational Logic: Beyond Strong Sequentiality. Proc. of the 5^{th} IEEE Symposium on Logic in Computer Science, LICS’95, Philadelphia, 1990. p. 230-242.

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

This article was processed using the L^{A}TEX macro package with LLNCS style