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 ^{⋆}

Abstract. We prove a version of the Standardization Theorem and the Discrete Normalization Theorem in stable Deterministic Residual Structures, Abstract Reduction Systems with axiomatized notions of residual, which model orthogonal rewrite systems. The latter theorem gives a strategy for construction of reductions Lévy-equivalent (or permutation-equivalent) to a given, finite or infinite, regular (or semi-linear) reduction, based on the neededness concept of Huet and Lévy. This and other results of this paper add to the understanding of Lévy-equivalence of reductions, and consequently, Lévy’s reduction space. We demonstrate how elements of this space can be used to give denotational semantics to known functional languages in an abstract manner.

1 Introduction

Long ago, Curry and Feys [CuFe58] proved that repeated contraction of leftmostoutermost 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, 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. This seminal work has been extended in many directions.

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. Kennaway and Sleep [KeSl89] generalized the needed strategy to orthogonal Combinatory Reduction systems (CRSs) of Klop [Klo80]. 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, the essential strategy, for the λ-calculus [Kha88], OTRSs [Kha93], and Orthogonal Expression Reduction Systems (OERS) [Kha94], a form of higher-order rewriting similar to Klop’s CRSs

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

(which subsumes Term Rewriting and the λ-calculus) [Kha92]. Sekar and Ramakrishnan [SeRa93] study a normalizing strategy which in each multi-step contracts a necessary set of redexes. A different approach to normalization is developed in Kennaway [Ken89] and in Antoy and 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, in the λ-calculus. Kennaway et al. [KKSV95] studied needed strategies for infinitary OTRSs.

In [GlKh94], the present authors found natural conditions on a set S of terms, in an OERS, 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 slightly) and any step u entering S is S-needed.

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), which are Abstract Reduction Systems (ARSs) where the residual relation on redexes is axiomatized in a way that enables one to define permutation-equivalence on reductions. They proved the RN theorem for stable DRS, for regular 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 (which consists of terms to which s is reducible) is stable and regular, then the task can be reduced to construction of a minimal, or rather a least (w.r.t. Lévy’s ordering ⊴ on reductions) G_{s}-normalizing reduction [GlKh94a], 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}-least – 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 (constructed according to some strategy), 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.

In this paper we indeed develop a neededness theory relative to particular semilinear, or regular, reductions, which enables us to characterize reductions in ⟨P ⟩_{L} for any such reduction P : t → → , finite or infinite, in stable DRSs. (By an ‘infinite’ reduction we mean a reduction of length ω.) We obtain two main results: the

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

Standardization Theorem, and the Discrete Normalization Theorem. The first states that every finite semi-linear reduction P can, in some canonical way, be transformed into a standard or self-essential reduction SE(P) Lévy-equivalent to P, where selfessentiality means that ‘omission’ of a step in SE(P) would yield a reduction no longer Lévy-equivalent to P. We also show that for infinite semi-linear reductions P, standard reductions Lévy-equivalent to P need not exist. This concept of standardization is the best approximation to the outside-in left-to-right concept of standardization [Bar84, Klo80], since we do not have any nesting reduction imposed on redexes, unlike ARSs of [GLM92], and there is no concept of ‘left’ or ‘right’ occurrences in DRSs. However, our standard reductions can be used successfully as canonical representatives in their Lévy-equivalence classes, without being unique representatives. The Discrete Normalization (DN) theorem states that for any P, repeated simultaneous contraction of all P -erased redexes yields a reduction in ⟨P ⟩_{L}, and if P is semi-linear and finite, then contraction of P -needed P -erased redexes eventually terminates by constructing a reduction in ⟨P ⟩_{L}. Here a redex is P -needed if at least one residual of it is contracted by any reduction in ⟨P ⟩_{L}, and is P -erased if it does not have residuals in some later term of P. P is semi-linear if its P -unneeded steps do not duplicate P -needed redexes. In orthogonal (acyclic) syntactic rewrite systems, all reductions are semi-linear.

Since every functional programming language is given by a (very often orthogonal) syntactic rewrite system R and a deterministic strategy F (e.g. the lazy, call-by-name, and several eager strategies in the λ-calculus), the value of a term (program) t is defined via its computation according to F. In semantics, values of terms are usually defined via some kind of finite or infinite trees, such as Böhm-trees [Bar84], constructed from symbols from the alphabet and a special constant ⊥ to denote undefined (in some sense) terms. The strategies F compute these trees. So, our DN theorem characterizes computations of a term which converge to its value, where value can be defined in various ways. We will describe an abstract approach to semantics of orthogonal rewrite systems, showing how the conventional tree semantics of such systems can be recovered without any assumption of syntax, using Lévy’s reduction space which we study here.

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. 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. Section 6 is devoted to semantics of DRSs. Conclusions appear in Section 7. More details can be found in [KhGl96].

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.

A definition and a survey of results about ARSs can be found in [Klo92]. Our definition is slightly different, and follows that of Hindley [Hin64]. 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 u 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. (Klop’s ARSs are pairs (T er, →), and do not allow one to distinguish transitions with the same source and target terms.) 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, and write P : t → → if P denotes a (finite or infinite) reduction starting from t. |P | denotes the length of P. P + Q denotes the concatenation of P and Q. P ≤ Q denotes that P is an initial part of Q. We use U, V, W to denote sets of redexes of a term.

DRSs descend from Stark’s Determinate Concurrent Transition Systems (DCTSs)

[Sta89] and Abstract Reduction Systems of Gonthier et al. [GLM92]. Unlike DCTSs, the residual relation in DRSs may be duplicating, and unlike ARSs of [GLM92], we do not have a nesting relation on redexes. Several refined concepts of abstract rewriting are studied in [Oos94, Mel96, Raa96]. DRS are intended to model all orthogonal term and graph rewrite systems, both first and higher-order, such as [Lév80, HuLé91, Klo80, Kha92, Nip93, Lam90, Kat90, SPE93, Oos94, AsLa96, Raa96], and other conflict-free transition systems with a reasonable level of abstraction, while say ARSs of [GLM92] do not cover e.g., orthogonal term graph rewriting systems [SPE93].

Definition 2.1 ([GlKh96]) (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 ≠ ∅.

Note that [acyclicity] re-introduces some kind of ‘nesting’ relation on redexes, but we do not even require this relation to be transitive.

As in [Lév80, HuLé91, Sta89], the residual relation on redexes in a DRS R is extended to all co-initial finite 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 Lévy- 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. Intuitively, P ≈_{L} Q means that P can be obtained from Q by a number of permutations of adjacent steps, therefore ‘Q and P do the same work’; and P ⊴ Q means that P does less work than Q, the difference being Q/P, so P + Q/P ≈_{L} Q. Unlike [Lév80, HuLé91], we do not consider complete developments of sets of residuals of a redex as multi-steps, so P/Q is only unique up to the choice of particular complete developments of such sets. (However, P/Q is defined more precisely than up to ≈_{L}.) The above relations can equivalently be defined also using Klop’s method of commutative diagrams [Klo80, Bar84]. We will often use Klop’s diagrams in proofs.

Lévy-equivalence extends to infinite reductions, denoted by t → → ∞, as follows. First, for any u ∈ t → →^{P} , define u/P = ∅ if u/P′ = ∅ for a finite initial part P′ of P. Now, for any P, Q : t → → , define P/Q = ∅, or equivalently P ⊴ Q, if for any redex v contracted in P, say P = P′ + v + P′′, v/(Q/P′) = ∅; and define P ≈_{L} Q iff P ⊴ Q and Q ⊴ P. P/Q is only defined for finite Q, as the reduction whose initial parts are residuals of initial parts of P under Q.

Here 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, SDRS, if the following axiom is satisfied:

• [stability] Let t→^{u}e, t→^{v}s, u ≠ v, and let u create 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.

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: s_{j}; Q_{j}; P_{i}/Q_{j}; Q_{j}/P_{i}; U_{i,j}]

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

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. Note that a reduction external to one complete development of U need not be external to all developments of U, and in general, externality is not invariant under ≈_{L}. For, consider a TRS R = {a → a′, f(x) → b, g(x) → c}, a term t = f(g(a)), and reductions P : t→^{a}f(g(a′))→^{f}b, Q : t→^{a}f(g(a′))→^{g}f(c), and N : t→^{g}f(c). Then we have Q ≈_{L} N, P is external to N, but not to Q; and P is not external to U = {a, g(a)}.

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

Lemma 2.2 (Stability Lemma) ([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.

As with the Stability Lemma, the following lemma extends the [acyclicity] property from one step external reductions to arbitrary finite external reductions.

Lemma 2.3 (Acyclicity Lemma) ([GlKh96a, KhGl96]) Let P, N be co-initial finite reductions in a DRS, and let P be external to N. Then N ≉_{L} P.

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 finite 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 = ∅, or equivalently, if u/Q = ∅ for any Q ≈_{L} P. We say that P discards u if P is external to u and erases it [GlKh94a].

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

Clearly, P -neededness, erasure, and essentiality do not depend on the choice of a reduction in ⟨P ⟩_{L} = {Q | Q ≈_{L} 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) → h(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.1 Let u ∈ t → →^{P} , in a DRS.

(1) If u is P -needed, then it is P -essential, but the converse need not hold.

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

(3) If P contracts a redex v, then v is P -needed iff it is P -essential.

Proof. Easy consequence of Definition 3.1. (Or see [KhGl96].)

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

3.2 Properties of Discrete Neededness and Essentiality

We now embark on proving existence of P -needed redexes for any finite P : t → → s in a stable DRS. The idea of our proof 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 P -needed.

Proposition 3.1 Let P : s → → t→^{u}e → →^{P^{∗}} , in a stable DRS.

(1) Let u create v ∈ e, and let UN_{P} (u, t). Then so is v.

(2) Let UN_{P} (w, t) and let v ∈ e be its u-residual. Then UN_{P} (v, e).

(3) Let NE_{P} (v, t), and let v ≠ u. Then v has at least one u-residual v′, and if it is the only u-residual of v, then NE_{P} (v′, e).

Proof. (1) By Lemma 3.1.(3), UN_{P} (u, t) ⇒ IE_{P} (u, t). Hence there is Q_{t} ≈_{L} u + P^{∗} that discards u. By Lemma 2.2, Q_{e} = Q_{t}/u is external to v. Further, Q_{e} ≈_{L} P^{∗}. Hence UN_{P} (v, e).

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

(2) Since w is P -unneeded, there is Q_{t} ≈_{L} u + P^{∗} that is external to w (see the picture for (1)). Hence u/Q_{t} = ∅ (since u/(u+P^{∗}) = ∅). Further, Q_{e} = Q_{t}/u ≈_{L} P^{∗}. By Lemma 2.1 Q_{e} is external to v. Thus UN_{P} (v, e).

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

The above proposition, as well as Lemma 5.3, is valid for P -(un)neededness replaced by P -(in)essentiality. We omit proofs (to be found in [KhGl96]) since the corresponding statements are not needed for the main results of this paper.

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

Proof. By Lemma 2.3, 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.

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

Proof. Let P : t = t_{0}→^{u_{0}}t_{1}→^{u_{1}} … →^{u_{n−1}}t_{n} = s, and let v_{0}, …, v_{n−1} be such that v_{i} ∈ t_{i},

v_{n−1} = u_{n−1}, and either v_{i} ≠ u_{i} and v_{i+1} is a u_{i}-residual of v_{i}, or v_{i} = u_{i} and u_{i} creates v_{i+1}. By Lemma 3.2, v_{i−1} is P -needed, and so are all v_{i} by Proposition 3.1.(1)-(2). Thus v_{0} ∈ t is P -needed.

4 Standardization

In orthogonal acyclic ‘syntactic’ rewrite systems, if a redex u erases or duplicates another redex v, then v is ‘below’ u, and v cannot duplicate or erase u. Therefore, if a reduction P : t → → s discards a redex u ∈ t, then one easily constructs a Q ≈_{L} P that discards u and does not 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). We will only need the following slightly weaker (by Lemma 3.1) property:

Definition 4.1 We call P : t → → , or equivalently ⟨P ⟩_{L}, regular or semi-linear if, for any Q ≈_{L} P, P -unneeded steps of Q do not duplicate P -needed redexes.

Note that our [acyclicity] axiom is too weak to exclude irregular reductions from SDRSs. Consider simply the ARS given by the graph of a term t containing two redexes t→^{u}o and t→^{v}s, such that v/u = ∅, u/v = {u_{1}, u_{2}}, and contraction of u_{1} and u_{2} in either order yields o. Then, for P = u, NE_{P} (u, t), UN_{P} (v, t), but v duplicates u.

Lemma 4.1 Let P be regular and let Q ⊴ P, in a DRs. Then P/Q is regular.

Proof. Immediate, since for any redex in ⟨P/Q⟩_{L}, P - and P/Q-neededness coincide.

Theorem 4.1 Let P : t → → s be a non-empty regular reduction in a stable 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}} … → t_{n} = s, 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 Proposition 3.1.(1)-(2), every u_{j} with j < i is P -unneeded. By regularity of P and Proposition 3.1.(3), 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 (canonical) 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).

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

Proof. Let Q : 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 Proposition 3.1.(1)-(2) 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 regularity of P.^{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} (Q) : 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 P -erased P -needed redex v_{j} ∈ s_{j} along Q′_{j} (see the figure). (Note that P′_{j} ≈_{L} P, so P′_{j}-neededness coincides with P -neededness.) Hence SE_{P} (Q) ⊴ Q.

[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}]

It is easy to see that standard reductions, in the sense of [Bar84, HuLé91, Klo80, 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 (see [KhGl96a] for the use of self-essential standard reductions in an abstract optimality theory). Therefore:

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 Proposition 3.1.(1)-(2) applies.

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

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

Proof. By Lemma 4.2, SE(P) ⊴ P and is finite. Let P : t_{0} → →^{P_{i}} t_{i}→^{u_{i}}t_{i+1} → → t_{n} and u_{i_{0}}, …, u_{i_{k−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}} … →^{v_{k−1}}s_{k}, 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 diagram for Lemma 4.2; take Q = P). Further, s_{k} does not contain P/SE(P)- erased P/SE(P)-needed redexes by Definition 4.2. By Lemma 4.1 and Lemma 4.2, P/SE(P) is regular. By Theorem 4.1, P/SE(P) = ∅, i.e., P ≈_{L} SE(P). Hence SE(P) is self-needed by Lemma 4.2, thus self-essential by Corollary 3.1.

The following example shows that if P is infinite, P ≈_{L} SE(P) need not hold. Consider the OTRS R = {f(x) → g(h(x)), g(x) → f(h(x)), 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), it is the only P -essential reduction, but P/Q ≠ ∅.

This should not be understood as implying that needed reductions are not useful in the study of transfinite reductions in OTRSs [KKSV95] – needed-fair reductions strongly converge to infinite normal forms. The reduction P above is divergent. In [KKSV95], reductions that do not converge strongly are considered meaningless, while here we study normalization relative to any reduction.

5 Discrete Normalization

This section is devoted to proving the main result of the paper – the Discrete Normalization Theorem. First a simple lemma, which is immediate from Definition 3.1.

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

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.2 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. Further, P ⊴ Q implies P′ ⊴ Q′. Hence P′ is Q′-erased by Lemma 5.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′; P]

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

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

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

Proof. Let v/u = {v_{1}, …, v_{k}}, and suppose on the contrary that UN_{P} (v_{i}, P′) for all i = 1, …, k (k ≥ 1 by Proposition 3.1.(3)). Thus, for every i, there is P_{i} ≈_{L} P′ that is external to v_{i}. P′ is regular by Lemma 4.1. Hence, by Lemma 4.2, SE(P′) is P′- needed, and by Proposition 3.1.(2) all residuals of v_{i} along SE(P′) are P′-unneeded. Hence SE(P′) is external to all v_{i}, and u + SE(P′) is external to v, contradiction, since P ≈_{L} u + SE(P′) by the Standardization theorem, and NE_{P} (v, t).

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

Proof. By Lemma 5.1, Q ⊴ P, hence u + Q/u ⊴ P. Let Q : t = t_{0}→^{v_{0}}t_{1}→^{v_{1}} … and Q_{i} : t = t_{0}→^{v_{0}}t_{1}→^{v_{1}} … → t_{i}. If v_{i} ∉ u/Q_{i}, then by Lemma 5.3 v_{i} has at least one P - needed u/Q_{i}-residual, and v_{i}/(u/Q_{i}) contracts at least one P -needed redex. Suppose on the contrary that there are 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/Q_{k}-development, contradiction.

Theorem 5.1 (Discrete Normalization) Let P : t → → , in a stable DRS.

(1) 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évyequivalent to P.

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

Proof. (1) (⇒) Let P ≈_{L} Q. Then Q/P = ∅, and Q is P -erased by Lemma 5.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 5.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.2, 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 = ∅.

(2) Let P : t→^{u}o → → s. Suppose there is a P -erased reduction Q : t → → that contracts infinitely many P -needed redexes. By Lemma 4.2 SE_{P} (Q) is an infinite P - needed P -erased reduction, and by Lemma 5.4, SE_{P} (Q)/u is a P -erased reduction with infinitely many P -needed steps, starting from o. Similarly, one shows that there is an infinite P -erased P -needed, i.e., ∅-erased ∅-needed, reduction starting from s, contradiction.

The DN theorem implies that ⟨P ⟩_{L} contains only a finite number of standard reductions, for any finite semi-linear P. It also implies termination of known standardization algorithms (which transform finite reductions into standard ones) [Bar84, HuLé91, Klo80, GLM92, Oos96], since our standardization concept is the most liberal one known in the literature.

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 demonstrating failure of standardization for infinite reductions 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 allowing self-neededly fair sequential reductions instead of multi-step reductions.

Finally, note that, in a non-duplicating SDRS, for any finite semi-linear P, SE(P) a shortest reduction in ⟨P ⟩_{L}. To show this, let SE(P) = u + P′, Q ≈_{L} P, and assume that P′ is shortest in ⟨P′⟩_{L}. Then |Q/u| ≤ |Q| − 1 since exactly one residual of u is contracted in Q, and |SE(P)| ≤ |Q| follows from the induction assumption |P′| ≤ |Q/u|.

6 Denotational Semantics

Lisper [Lis96] defined semantics for an ARS A = (T er, Red, →)^{4} as follows: let C = (C, ⊑, ⊥) be a cpo and let f : T er → C be a monotone function, meaning that t → s implies f(t) ⊑ f(s). Then semantics of a term t ∈ T er w.r.t. f in C, S(t, f, C), is the set of least upper bounds ⊔f(P), such that there is no co-initial Q such that P <_{m} Q and ⊔f(P) ⊏ ⊔f(Q), where, for any P : t → t_{1} → t_{2} → …, f(P) = f(t), f(t_{1}), f(t_{2}), …, and ⊔f(P) denotes the least upper bound of f(P) in C; and P <_{m} Q means that every term of P can be reduced to a term in Q. Elements of S(t, f, C) are values of t in C, w.r.t. f.

The most commonly used cpos as semantics for syntactic rewrite systems are those of tree cpos T = (T_{⊥}^{∞}, ⪯, ⊥), where T_{⊥}^{∞} consists of finite and infinite trees labelled by symbols from the rewrite alphabet and the distinguished constant symbol ⊥ which represents undefined or meaningless terms; and ⪯ is the ordering induced by ⊥ ⪯ s for any s ∈ T_{⊥}^{∞}. The tree cpo was first defined for Recursive Program Schemes by Nivat [Niv75], and was later extended to the λ-calculus by Lévy [Lév76] (the so called Lévy-Longo trees or Lazy-trees [Lon83, AbOn93]) and Barendregt [Bar84] (the Böhm trees); and to TRSs by Boudol [Bou85]. In Nivat’s and Boudol’s semantics, undefined are terms which cannot be reduced to a root stable form – a term that cannot be reduced to a redex. In Böhm semantics, λ-terms not having a head-normal form (hnf) are considered meaningless, and Lévy defines meaningless to be λ-terms that do not have neither hnfs nor weak hnfs (which are simply abstractions λxt). Reasonable concepts of meaningless terms in (infinitary) TRSs and the λ-calculus are studied in [KOV96].

Lisper’s definition of abstract semantics allows one to describe all the above tree semantics, but is not suitable for all known interpretations, and we generalize it slightly by taking f to be a function from the set of all reductions in A to C. Such

4 More precisely, ARSs used in [Lis96] are Klop’s ARSs [Klo92].

an f is monotone if for any reduction P : t → →^{P′} s→^{u}o in A, f(P′) ⊑ f(P) in C. So the information increases (w.r.t. ⊑, in C) as the computation progresses, and the whole history of the computation is taken into account. We define every ⊑-maximal element in the set {⊔f(P) | P : t → → } (which need not be ⊑-maximal in C) to be a value of t. We will call this semantics the maximal semantics.

Lévy’s reduction space L = (L, ⊴), where L is the set of all Lévy-equivalence classes of reductions in a DRS R, is also a cpo (the bottom element is irrelevant). And the interpretation f on reductions in R defined by f(P) = ⟨P ⟩_{L} is obviously monotone. If we take R = (A, /) where terms of A = (T er, Red, →) are (finite) λterms with constant ⊥; Red is the set of β-redex occurrences; and → is defined by: t→^{u}_{β}s if u ∈ t is a β-redex having a hnf, and t→^{u}_{⊥}s otherwise (where t→^{u}_{⊥}s means that s is obtained from t by replacing u with ⊥); and take as the residual relation the one induced by that of the λ-calculus, then the maximal semantics of R in L (w.r.t. f above) is exactly the Böhm semantics of the λ-calculus. The Nivat, Boudol and Lévy’s semantics can be recovered similarly, by taking appropriate R and →_{⊥}.

Alternatively, we can define all redexes inside meaningless redexes to be meaningless, and consider only ordinary meaningful-fair reductions, i.e., reductions without ⊥-steps in which no meaningful redex has a meaningful residual in every subsequent term. In all above four cases, there is (exactly one, up to ≈_{L}) ⊴-minimal meaningfulfair reduction starting from a term t (such reductions contract only meaningful redexes), and these reductions can be taken as representations of corresponding semantic trees.

Note that, unlike the maximal semantics, not-necessarily fair reductions are used to define denotational semantics in the latter case. And the DN theorem gives a characterization of reductions computing the values of terms in all the above cases.

7 Conclusions and Future Work

We have proven an abstract Discrete Normalization theorem. It gives a strategy for constructing reductions Lévy-equivalent to a finite or infinite reduction P (which need not be normalizing or fair). We introduced a number of concepts and constructs, such as standardization, which are technically interesting in their own rights.

We have not addressed here the question of how to find efficiently discretely needed redexes, and a syntactic theory similar to the strong sequentiality theory [HuLé91, KlMi90] needs to be developed for discrete and relative normalization.

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

Finally, development of a needed narrowing theory in [AEH94] suggests that the abstract theory of neededness can be extended to cover narrowing and possibly other proof procedures. Non-deterministic systems must also be considered, and Boudol’s work [Bou85] extending [HuLé91] to non-orthogonal TRSs can be used as the basis.

Acknowledgments We thank J.R. Kennaway, V. Van Oostrom and M.R. Sleep for useful comments. The diagrams were drawn using P. Taylor’s diagram package.

References

[AbOn93] Abramsky S., Ong C.-H. L. Full abstraction in the lazy lambda calculus. Inf.& Comp., 105:159-267, 1993.

[AEH94] Antoy S., Echahed R., Hanus M. A needed narrowing strategy. In: Proc. of POPL’94, Portland, Oregon, 1994.

[AnMi94] Antoy S. and Middeldorp A. A Sequential Reduction Strategy. In Proc. of ALP’94, Springer LNCS, vol. 850, p. 168-185, 1994.

[AsLa96] Asperti A., Laneve C. Interaction Systems II: the practice of optimal reductions. TCS, 159(2):191-244, 1996.

[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. Inf.& Comp., 75(3):191-231, 1987.

[BeLé79] Berry G., Lévy J.-J. Minimal and optimal computations of recursive programs.

JACM 26, 1979, p. 148-175.

[Bou85] Boudol G. Computational semantics of term rewriting systems. In: Algebraic methods in semantics. Nivat M., Reynolds J.C., eds. Cambr. Univ. Press, 1985, p. 169-236.

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

[Gar94] Gardner P. Discovering needed reductions using type theory. In: Proc. of 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 CTRS’94, Springer LNCS, vol. 968, N. Dershowitz, N. Lindenstrauss, eds. Jerusalem, 1994, p. 144-165.

[GlKh94a] Glauert J.R.W., Khasidashvili Z. Minimal and optimal relative normalization in Expression Reduction Systems. Report SYS-C94-06, UEA, Norwich, 1994.

[GlKh96] Glauert J.R.W., Khasidashvili Z. Relative normalization in deterministic residual structures. In [CAAP’96], p. 180-195.

[GlKh96a] Glauert J.R.W., Khasidashvili Z. Relative normalization in stable deterministic residual structures. Report SYS-C96-01, UEA, Norwich, 1996.

[GLM92] Gonthier G., Lévy J.-J., Melliès P.-A. An abstract Standardisation theorem. In: Proc. of LICS’92, IEEE Computer Society Press, 1992, p. 72-81.

[Hin64] Hindley R.J. An abstract form of the Church-Rosser theorem I. JSL, 34(4):545-560, 1969.

[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, p. 394-443.

[Kat90] Kathail V. Optimal Interpreters for Lambda-calculus based functional languages, PhD thesis, MIT, 1990.

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

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

[KKSV95] Kennaway J. R., Klop J. W., Sleep M. R, de Vries F.-J. Transfinite reductions in orthogonal term rewriting. Information and Computation, 119(1):18-38, 1995.

[KOV96] Kennaway J.R., van Oostrom V., de Vries F.J. Meaningless terms in rewriting. In: Proc. of the 5^{th} International Conference on Algebraic and Logic Programming, ALP’96, Aachen, 1996. To Appear.

[Kha88] Khasidashvili Z. β-reductions and β-developments of λ-terms with the least number of steps. In: Proc. of the Int. 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 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 CAAP’94, Springer LNCS, vol. 787, S. Tison, ed. Edinburgh, 1994, p. 172-186.

[KhGl96] Khasidashvili Z., Glauert J.R.W. Discrete normalization and standardization in stable deterministic residual structures. Report SYS-C96-02, UEA, Norwich, 1996.

[KhGl96a] Khasidashvili Z., Glauert J.R.W. Zig-zag and extraction families in nonduplicating stable Deterministic Residual Structures. Submitted for publication. (Available at ftp://ftp.sys.uea.ac.uk/pub/zurab/)

[CAAP’96] Kirchner H., editor. Proc. of the 19^{th} International Colloquium on Trees in

Algebra and Programming, CAAP’96, Springer LNCS, vol. 1059, 1996.

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

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

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

[Lam90] Lamping J. An algorithm for optimal lambda calculus reduction. In: Proc. of POPL’90, 1990, p.16-30.

[Lév76] Lévy J.-J. An algebraic interpretation of the λβK-calculus; and an application of

a labelled λ-calculus. TCS 2(1):97-114, 1976. [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.

[Lis96] Lisper B. Computing in unpredictable environments: semantics, reduction strategies, and program transformations. In [CAAP’96], p. 165-179.

[Lon83] Longo G. Set theoretic models of lambda calculus: theories, expansions and isomorphisms. Annals of pure and applied logic, 24:153-188, 1983.

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

[Mel96] Melliès P.-A. Description Abstraite des Systèmes de Réécriture. Thèse de l’Université Paris 7, 1996.

[Nip93] Nipkow T. Orthogonal higher-order rewrite systems are confluent. In: Proc. of TLCA’93, Springer LNCS, vol. 664, Bazem M., Groote J.F., eds. 1993, p. 306-317.

[Niv75] Nivat M. On the interpretation of recursive polyadic program schemes. Symposia Mathematica, 15:255-281, 1975.

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

[Oos96] Van Oostrom V. Higher order families. In: Proc. of RTA’96. To appear.

[Raa96] Van Raamsdonk F. Confluence and normalisation for higher-order rewriting. Ph.D. Thesis, CWI Amsterdam, 1996.

[SeRa93] Sekar R.C., Ramakrishnan I.V. Programming in Equational Logic: Beyond Strong Sequentiality. Information and Computation, 104(1):78-109, 1993.

[SPE93] Sleep M. R., Plasmeijer M. J., van Eekelen M. C. J. D., eds. Term Graph Rewriting: Theory and Practice. John Wiley, 1993, p.141-156.

[Sta89] Stark E. W. Concurrent transition systems. TCS, 64(3):221-270, 1989.

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