Relative Normalization in Deterministic Residual Structures

John Glauert and Zurab Khasidashvili

School of Information Systems, UEA Norwich NR4 7TJ England jrwg@sys.uea.ac.uk, zurab@sys.uea.ac.uk ^{⋆}

Abstract. This paper generalizes the Huet and Lévy theory of normalization by neededness to an abstract setting. We define Stable Deterministic Residual Structures (SDRS) and Deterministic Family Structures (DFS) by axiomatizing some properties of the residual relation and the family relation on redexes in an Abstract Rewriting System. We present two proofs of the Relative Normalization Theorem, one for SDRSs for regular stable sets, and another for DFSs for all stable sets of desirable ‘normal forms’. We further prove the Relative Optimality Theorem for DFSs. We extend this result to deterministic Computation Structures which are deterministic Event Structures with an extra relation expressing self-essentiality.

1 Introduction

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

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

This work has been extended in several directions. Barendregt et al. [BKKS87], Maranget [Mar92], and Nöcker [Nök94] study neededness w.r.t. head-normal forms, weak head-normal forms, and constructor head-normal forms, respectively. Sekar and Ramakrishnan [SeRa90] study normalization via necessary set of redexes. Kennaway et al. [KKSV96] study a needed strategy for infinitary OTRSs. A different approach to normalization is developed in Kennaway [Ken89] and Antoy and Middeldorp [AnMi94]. Antoy et al. [AEH94] design a needed narrowing strategy.

In [GlKh94], the present authors address the question of normalization relative to a desired set of final terms, considering the properties that a set of terms must possess in order for the neededness theory of Huet and Lévy still to make sense. This work is

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

done in the context of orthogonal Expression Reduction Systems (OERS) [Kha92], a form of higher-order rewriting which subsumes Term Rewriting and the λ-calculus. Natural conditions are imposed on S, called stability, that are necessary and sufficient for the following Relative Normalization (RN) 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 such redexes will lead to an S-normal form whenever there is one. It is shown also that if a stable S is regular, i.e., if S-unneeded redexes cannot duplicate S-needed ones, then the S-needed strategy is hypernormalizing as well.

In this paper, we further generalize the theory by abstracting from the structure of terms. We study relative normalization in Deterministic Residual Structures (DRSs). A DRS is an Abstract Reduction Systems (ARSs) which has a residual relation between redexes in the source and target terms of each transition. Redexes of t may be erased by reduction of u, new redexes may be introduced in s, while other redexes of s are considered residuals of redexes in t, as specified by the residual relation. Further, the residual relation is generalized to all reductions, and permutationequivalence on reductions, referred to below as Lévy-equivalence, and the embedding relation, which induces a partial ordering on the reduction space, is introduced, as is done for the λ-calculus in [Lév78, Lév80]. Sufficient conditions needed to define the above concepts in an abstract setting were stated in [Sta89, GLM92].

In [Sta89], Stark defines Concurrent Transition Systems (CTSs) and uses them to develop a model of concurrent computation, studying ways of building machine networks with concurrent machines as basic objects. On the other hand, Gonthier et al. [GLM92] were interested in studying more syntactic properties, such as standardization, of orthogonal rewrite systems in an abstract setting. The way standardization is understood in that paper requires a nesting relation on redexes in a term, and some axioms giving its important properties. Standard reductions then become some kind of outside-in reductions. However, the [GLM92] axioms are rather restrictive, since even orthogonal DAGs [Mar91, Mar92, KKSV93] do not satisfy them as pointed out by R. Kennaway.

Our DRSs are more refined than CTSs, since in the latter the residual relation is non-duplicating. We do not impose a nesting relation on redexes, but are still able to prove the RN theorem for all regular stable sets S. (We actually prove the Relative Hypernormalization theorem.) We use a form of Berry’s stability axiom [Ber79] and show that without this axiom the theorem fails. The proof method employed is similar to that in [Kha88, Kha93], and is based on the fact that S-needed steps in a reduction can be pushed before S-unneeded steps without affecting the number of S-needed steps. The important difference is that [Kha88, Kha93] uses the syntactic notion of descendants of subterms – a refinement of the residual notion for redexes – which is much harder to axiomatize.

Since for irregular stable S, S-unneeded redexes can duplicate S-needed ones, the above proof method does not apply for all DRS; for the same reason, the S-needed strategy is no longer hypernormalizing. We define a Deterministic Family Structure (DFS) as a DRS with a very liberal notion of family relation [Lév78, Lév80] and a contribution relation on families, expressing the notion of (at least one member of) a family to be needed to create another family. For DFSs, the proof of the RN theorem for all stable S from [GlKh94] works perfectly.

An advantage of the first RN theorem is that checking for Berry’s stability is much simpler than constructing a sound family relation. For example, the λcalculus [Lév78, Lév80], orthogonal TRSs [Mar92], Interaction Systems [AsLa93], and orthogonal CRSs (and ERSs) [Klo80, KeSl89] form DFSs It seems very likely that other orthogonal higher-order rewriting systems, such as HRSs [Nip93] and HORSs [Oos94, OR94], which do form stable DRSs, form DFSs as well, although, to our knowledge, this is not yet known.

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

Using the family axioms, we give an Event Structure (ES) [Win80] semantics to DRSs, by considering redex-families as events. We define Deterministic Computation Structures (DCS) as Deterministic Prime ESs with an extra relation α ⊳ e to express the fact that an event e is inessential for a set of events α, a configuration. This enables us to define Lévy-equivalence on prime deterministic ESs. For DCSs, the theory of relative normalization can be applied.

The paper is organized as follows. In the next section, we introduce stable DRSs and give some examples. In Section 3, we prove the RN theorem for regular stable sets S in an SDRS R, and demonstrate that if R is not stable, then the theorem fails. In Section 4, we introduce DFSs, compare them with stable DRSs, and prove the RN theorem for all stable S. In Section 5, we strengthen the latter result, and prove the Relative Optimality theorem for any DFS. Finally, in Section 6, we extend the obtained results to Event Structures. Conclusions appear in Section 7.

2 Deterministic Residual Structures

In this section we define Deterministic Residual Structures (DRSs) which are Abstract Reduction Systems (ARSs) satisfying certain properties concerning residuals. The definition and some results about ARSs can be found e.g., in [Klo92]. Our definition is slightly different.

Definition 2.1 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. 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. We use U, V, W to denote sets of redexes of a term.

DRSs are similar to Stark’s Determinate Concurrent Transition Systems (DTCS) [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 requires a non-duplicating residual relation, and distinguishes 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.2 (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. Intuitively, P ⊴ Q expresses that Q does more work than P, and Q/P is the part of Q that remains from it after P. The above relations can equivalently be defined also using Klop’s method of commutative diagrams. The method is well described in [Klo80, Bar84].

Definition 2.3 We call a DRS R stable (SDRS) 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 (see the diagram).

Intuitively, stability means that a redex cannot arise from two unrelated sources. This property has a natural extension to many-step reductions, where ‘unrelated’ is formalized by the notion of external. For syntactic systems externality is a natural

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

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.4 • 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}) = ∅.

[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}/(Q_{j}/P_{i})]

[figure: v_{j}; v_{j}/(P_{i}/Q_{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 Let P : t → → s be external to Q : t → → e, in an SDRS, 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 (see the diagram). Proof By induction on the number n of elementary diagrams in Klp’s diagram D(P, Q) of P and Q. The case n = 1 is the axiom [stability]. It follows from Definition 2.4 that the top and left edges of all sub-diagrams of D(P, Q) are external reductions, therefore we can assume the lemma is proved for all subdiagrams of D(P, Q). So let |P | > 1, i.e., P = u + N with |N| > 0 . Then W = W_{u}/N ∪ W_{N}, where W_{u} is the set of redexes created by u, and W_{N} is the set of redexes created by (i.e., along) N. By the induction assumption, Q/u is external to W_{u}, and the redexes in W_{u}/(Q/u) are created by u/Q. By Lemma 3.1, Q/P = (Q/u)/N is external to W_{u}/N. By the induction assumption, Q/P = (Q/u)/N is external to W_{N} and redexes in W_{N}/(Q/P) are created by N/(Q/u). Hence Q/P is external to W, and since W/(Q/P) = W_{N}/(Q/P) ∪ W_{u}/((Q/u) ⊔ N), redexes in W/(Q/P) are created by P/Q.

As already mentioned, all orthogonal first and higher order rewrite systems are stable DRSs, and so are orthogonal graph rewriting systems [KKSV93, Mar92].

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

3 Relative Normalization for regular stable sets

In this section, we prove that, for any regular stable set of terms S in a stable DRS R, an S-normal form of an S-normalizable term can be found by contracting S-needed redexes in it, even if every S-needed step is preceded by a finite number of S-unneeded steps. We show that without the assumption of stability for R, this result breaks down. Further, examples from [GlKh94] show that the stability of S is necessary for the Relative Normalization theorem to hold. This shows that the stability of S for a Berry–stable R provides a unique notion of stability for the computation system (R, S).

Definition 3.1 ([GlKh94]) Let S be a set of terms in a DRS R. We call a redex u ∈ t S-needed, written NE_{S}(u, t), if at least one residual of it is contracted in any reduction from t to a term in S, and call it S-unneeded, written UN_{S}(u, t), otherwise.

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

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

A stable set need not be closed under reduction – Q/P in the definition above may contain terms not in S, but closure under parallel moves requires that the final term is. Stability and regularity coincide in non-duplicating systems. Below S will usually denote a stable set of terms in some DRS. R will denote a regular stable set. For simplicity, we only consider stable sets that are closed under reduction; obviously, closure under reduction implies closure under parallel moves.

The most appealing examples of stable sets are normal forms [HuLé91], headnormal forms [BKKS87], weak-head-normal forms in an OTRS (a partial result is in [Mar92]), and constructor-head-normal forms for constructor TRSs [Nök94]. All the above sets are closed under reduction, and are regular. Other examples include weak-head-normal forms (up to garbage-collection, modulo a congruence) in Yoshida’s λf-calculus (an environment calculus) [Yos93] and the set of answers in call-by-need λ-calculus of Ariola et al. [AFMOW94]; both are conditional rewrite systems. An example of an OTRS with an irregular stable S is given in Remark 3.1.

We begin the proof by showing that S-unneeded redexes cannot create S-needed ones, and that residuals of S-unneeded redexes remain unneeded. When S is regular, this enables us to construct a S-needed variant of any S-normalizing reduction.

Lemma 3.1 Let P : t_{0}→^{v_{0}}t_{1}→^{v_{1}} … → t_{n} be external to U = {u_{1}, …, u_{n}} ⊆ t_{0}, and

let Q_{0} : t_{0} → → o_{0}. Then P′ = P/Q_{0} is external to U′ = U/Q_{0}. If P is S-normalizing, then so is P′.

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

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

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

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

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

The following example shows that, in the above lemma, stability of the DRS is necessary.

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

Definition 3.3 We call P : t_{0} → t_{1} → … S-(un)needed, written NE_{S}(P), (resp. UN_{S}(P)) if it contracts only S-(un)needed redexes. We call P S-quasi-needed if it contracts infinitely many S-needed redexes, and call it S-semi-needed if it can be expressed as P = P_{1} + P_{2} with NE_{S}(P_{1}) and UN_{S}(P_{2}). In the latter case, we call P_{1} the S-needed part of P (P_{1} can be infinite, in which case P_{2} = ∅).

We now describe an algorithm that, for a regular stable R in a DRS R, transforms any finite or infinite reduction P into an R-semi-needed reduction K(P). The algorithm is as follows: find in P the leftmost subreduction P_{0} : t→^{u}s→^{v}o such that UN_{R}(u, t) and NE_{R}(v, s). Let P = P_{1} + P_{0} + P_{2}. By Lemma 3.2, v is a residual of a redex v′ ∈ t, which is R-needed by Corollary 3.1. Since R is regular, v is the only residual of v′, hence P_{0} and P′_{0} = v′ + u/v′ are both complete developments of the set u, v′ ∈ t, thus P_{0} ≈_{L} P′_{0}. Now replace P_{0} by P′_{0} in P. Transform the obtained reduction P′ in the same way, and so on, as long as possible. Obviously, by regularity of R, the number of R-unneeded steps in P′ preceding v′ is less than the number preceding v in P, and the number of R-needed steps in P and P′ coincide.

Lemma 3.3 Let P be a finite or infinite reduction in an SDRS, and let R be regular.

(1) If P ends at a term in R, then K(P) is a finite S-semi-needed reduction whose S-needed part ends at a term in R as well.

(2) If P is S-quasi-needed, then K(P) is an infinite S-needed reduction. Proof (1) Since the transformation doesn’t change the number of R-needed steps in P, it follows that K(P) is R-semi-needed, and it ends at R since K(P) ≈_{L} P. The step of K(P) entering R is the last R-needed step of K(P) by stability of R.

(2) Immediate from the construction of K(P).

Next we show that, unless it is contracted, an R-needed redexes has at least one R-needed residual. Therefore, residuals of R-quasi-needed reductions remain so. It follows that an R-normalizable term cannot possess an R-quasi-needed reduction.

Lemma 3.4 Let R be a regular stable set of terms in a DRS R, and let t→^{u}s. Then any R-needed redex v ∈ t different from u has an R-needed residual. Proof If t is not R-normalizable, then neither is s, and all redexes in t and s are R-needed. So suppose t is R-normalizable (t ∉ R since t contains an R-needed redex), and suppose on the contrary that each residual v_{i} of v in s is R-unneeded. By closure of R under parallel moves, s is R-normalizing too. By Lemma 3.3.(1), there is an R-needed R-normalizing reduction P : s → → o. Since by Corollary 3.1 all residuals of each v_{i} along P are R-unneeded, P is external to all v_{i}. Therefore, u + P is external to v and is R-normalizing – a contradiction, since NE_{R}(v, t).

Lemma 3.5 Let t_{0} have an R-quasi-needed reduction and t_{0}→^{u}s_{0}. Then s_{0} also has an R-quasi-needed reduction (see diagram). Proof By Lemma 3.3, t_{0} has an infinite R-needed reduction P : t_{0}→^{u_{0}}t_{1}→^{u_{1}} . . .. Let U_{i} = u/(u_{0} + … + u_{i−1}), i = 0, 1, . . .. It follows from finiteness of developments that there are infinitely many numbers k such that u_{k} ∉ U_{k} (otherwise there should be a number m such that t_{m}→^{u_{m}}t_{m+1} →^{u_{m+1}} … is an infinite U_{m}-development). By Lemma 3.4, u_{k} ∉ U_{k} and NE_{R}(u_{k}, t_{k}) imply that u_{k} has at least one R-needed U_{k}-residual in s_{k}, i.e. u_{k}/U_{k} contains at least one R-needed step. Hence P/u is R-quasi-needed.

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

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

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

(2) t has an R-normal form iff it does not possess a reduction in which infinitely many times R-needed redexes are contracted. Proof (1) By Definition 3.1 if t is not R-normalizing, and by Lemma 3.3 otherwise.

(2) (⇒) Let t → →^{P} s ∈ R. Suppose on the contrary that there is an R-quasi-needed Q starting from t. Then by Lemma 3.5 Q/P is R-quasi-needed as well – a contradiction, since all terms of Q/P are in R, by the closure of R under reduction, and therefore Q/P must be R-unneeded. (⇐) By (1), one can repeatedly contract Rneeded redexes in t, unless a term in R is reached; the latter is inevitable since t doesn’t have an infinite R-needed reduction.

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

4 Relative Normalization in Deterministic Family Structures

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

Definition 4.1 (Deterministic Family Structure) A DFS F is a triple F = (R, ≃, ↪), where R is a DRS; ≃ is an equivalence relation on redexes with histories; and ↪ is the contribution relation on co-initial families, defined as follows:

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

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

• [initial] Let u, v ∈ t and u ≠ v, in R. Then F am(∅_{t}u) ≠ F am(∅_{t}v).

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

• [creation] if e → →^{P} t→^{u}s and u creates v ∈ s, then F am(P u) ↪ F am((P + u)v).

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

One can check that all the existing definitions of family relation in the literature [Lév78, KeSl89, Mar92, AsLa93] satisfy the above axioms. Hence our definition is consistent. The reason for considering more notions of family than just the zig-zag is that we want to be more flexible and able to consider a large class of sharing mechanisms as legal; there are sharing mechanisms that are strictly larger than zig-zag, e.g., the one in [AsLa93].

Let us call Cone(ϕ) = {ϕ_{i} | ϕ_{i} ↪ ϕ} the cone of ϕ. It follows immediately from the family axioms that:

Proposition 4.1 In any DFS F:

• [irreflexivity] ϕ ↛ ϕ.

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

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

The following example shows that, in a DRS with ≃ and ↪, [initial], [creation] and [contribution] do not imply [termination].

Example 4.1 Consider the ARS given by Figure (a) below, where the redex x creates u and v; u_{1} and u′_{2a} create w; v/u = v′; u/v = {u_{1}, u_{2}}; u_{1}/u_{2} = u′_{1}, u_{2}/u_{1} = u′_{2}; u′_{2}/w = {u′_{2a}, u′_{2b}}; w/u′_{2} = ∅, u′_{2a}/u′_{2b} = ∅, u′_{2b}/u′_{2a} = u′_{2}. All the us are residuals of u, hence belong to the same family U. Similarly, v and v′ must be in the same family too, say V. Further, take X = {x}, take for W the set of all contracted ws (with histories), and define the contribution relation on X, U, V, W by X ↪ V, U and U ↪ W. Since the only infinite reduction goes through the cycle infinitely many times, and each time the contracted w is created by u′_{2a}, all developments in the figure are terminating. It remains to note that [FD] and the other family axioms but [termination] are satisfied too. Note that the DRS is stable.

Lemma 4.1 Any DFS F is a stable DRS.

Proof We want to show that if u, v ∈ t are different redexes, t→^{u}e, t→^{v}s, e → →^{v/u} o, and u creates a redex w ∈ e, then the redexes in w/(v/u) ∈ o are not u/v-residuals of redexes of s. By axioms [creation] and [contribution], for any redex w′ ∈ s, Cone(F am(w′)) = ∅ if w′ is not a created redex, and Cone(F am(w′)) = {F am(v)} otherwise; and Cone(F am(w)) = {F am(u)}. Hence the redexes in w/(v/u) and s are in different families by [initial], and the lemma follows (since ≃_{z}⊆≃).

[figure: x; ·; v; ·; t; u; e; w; o^{∗}]
[figure: u_{2}; u_{1}]
[figure: ·; ·; w; \underline{u′_{2a}}; ·; s; v; u′; o; v′]
[figure: u′_{1}; u′_{2}; u′_{2b}; w^{∗}]
[figure: ·; u; v′; ·; ∅; \underline{∅}; ·; o^{∗}; w′; ∅; o^{∗}; ∅]

(a)  (b)

The following example shows that a DRS with ≃ and ↪ relations satisfying all DFS axioms but [initial] need not be stable.

Example 4.2 Consider the DRS given by Figure (b) above, where w and w′ are created by u and v, respectively, u/v = u′, v/u = v′, w/v′ = w′/u′ = w^{∗}. Then the sets U = {u, u′, v, v′} and W = {w, w′, w^{∗}} with the contribution relation U ↪ W do satisfy the DFS axioms except for [initial], but the underlying DRS is not stable.

Lemma 4.2 Let S be stable, t ∉ S, t→^{u}t′, UN_{S}(u, t), and let u′ ∈ t′ be a redex created by u, in a DFS F. Then UN_{S}(u′, t′). Proof By Lemma 3.2 and Lemma 4.1.

Now we can generalize the RN theorem, proved in [GlKh94] for orthogonal ERSs [Kha92], to all DFSs. We now allow for arbitrary stable sets S.

Below F AM(P) denotes the set of families (whose member redexes are) contracted in P.

Theorem 4.1 (Relative Normalization) Let S be a stable set of terms in a Deterministic Family Structure F, and let t ∉ S be S-normalizable. Then

(1) t contains an S-needed redex.

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

(2) Let P : t → → s be an S-normalizing reduction and Q : t→^{u_{0}}t_{1}→^{u_{1}} … be an S-needed reduction. Further, let Q_{i} : t→^{u_{0}}t_{1}→^{u_{1}} … →^{u_{i−1}}t_{i} and P_{i} = P/Q_{i} (i ≥ 1) (see the diagram below). By ≃_{z}⊆≃, F AM(P_{i}) ⊆ F AM(P). Since Q is S-needed and P_{i} is S-normalizing (by the closure of S under parallel moves), at least one residual of u_{i} is contracted in P_{i}. Therefore, again by ≃_{z}⊆≃, F am(u_{i}) ∈ F AM(P_{i}). Hence F AM(Q) ⊆ F AM(P) and Q is terminating by [termination].

Note that we have not used the acyclicity axiom in the proofs. However, it is necessary and sufficient to insure that the set of normal forms is stable. Note also that only by using Theorem 4.1 can we prove the analogue of Lemma 3.4 for all stable S.

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

5 The Relative Optimality Theorem

In this section, we define weakly S-needed redexes, and show that their contraction in an S-normalizable term t leads to an S-normal form of t. We also generalize Lévy’s Optimality theorem [Lév80] to all stable sets S in any DFS.

Definition 5.1 We call a family ϕ relative to t S-needed if any reduction from t to a term in S contracts at least one member of ϕ. We call redexes in S-needed families weakly S-needed.

Theorem 5.1 Let S be a stable set of terms in a Deterministic Family Structure F, and t be an S-normalizable term in F. Then any weakly S-needed reduction starting from t is terminating. Proof By [termination], since there is only a finite number of S-needed families relative to t.

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

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

Corollary 5.1 Let S be a stable set of terms in a DFS F. Then any S-needed family-reduction starting from an S-normalizable term is eventually S-normalizing.

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

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

6 Relative Normalization in Event Structures

In this section, we give an Event Structure semantics to DFSs. Smoothness of the interpretation justifies our choice of family axioms. We also generalize the RN theorems to ESs by giving the reverse translation. To this end, we equip ESs with an extra operation ⊳ expressing redundancy of events, thereby enhancing the match between DFSs and corresponding ESs.

A Prime Event Structure (PES) [Win80] is a triple E^{≤} = (E, Con, ≤), where E is a set of events, ranged over by e, e_{1}, …; the consistency predicate Con is a nonempty set of subsets of E, denoted by X, Y, …; and the causal dependency relation ≤ is a partial order on E, such that {e} ∈ Con, Y ⊆ X ∈ Con ⇒ Y ∈ Con, X ∈ Con∧∃e′ ∈ X.e ≤ e′ ⇒ X ∪{e} ∈ Con, and {e′ | e′ ≤ e} is finite for any e ∈ E.

In this paper we only consider deterministic structures, DPESs, where no event can prevent others from occurring, and therefore the consistency predicate is the powerset of E, and will be omitted. Configurations (or states) of E^{≤} are left-closed subsets α, β, … of E, i.e., subsets {α ⊆ E | e ∈ E ∧ e′ < e ⇒ e′ ∈ α}. It is immediate from Proposition 4.1 that:

Theorem 6.1 For any DFS F_{t} = (R_{t}, ≃, ↪), where R_{t} is a (sub)DRS whose term domain is the graph of a term t (i.e., the set of terms to which t is reducible), E\underline{↪} ; F_{t} = (F AM(t), \underline{↪}) is a DPES, where ϕ\underline{↪}ψ means that ϕ ↪ ψ or ϕ = ψ.

Definition 6.1 Let E = (E, ≤) be a DPES with an extra relation ⊳⊆ F Conf(E) × E, where F Conf(E) is the set of finite configurations of E, satisfying the following axioms:

• α ⊳ e ∧ α ⊆ β ∈ F Conf(E) ⇒ β ⊳ e;

• α ∪ {e′} ⊳ e′ ∧ α ∪ {e′} ⊳ e ⇒ α ⊳ e. Then we call C = (E, ⊳) a Deterministic Computation Structure (DCS). We read α ⊳ e as: ‘e is α-inessential’. On F Conf(C) = F Conf(E), we define Lévy-equivalence by:

• α ≈_{L} β iff SE(α) = SE(β), where SE(α) = {e ∈ α | α ⋫ e} is the set of self-essential events of α.

In E\underline{↪} ; F_{t}, the configurations are sets F AM(Q) of complete family-reductions Q. Define F AM(Q) ⊳_{t} ϕ iff there are (finite) complete family-reductions P, N ≈_{L} Q such that ϕ ∉ F AM(P) and ϕ ∈ F AM(N). Then ⊳_{t} satisfies the above ⊳-axioms. So we can actually speak of translation of F_{t} into a DCS C_{F_{t}} = (E_{F_{t}}, ⊳_{t}). Obviously, P ≈_{L} P′ implies SE(F AM(P)) = SE(F AM(P′)). The converse can also be proved using the acyclicity axiom.

Definition 6.2 To a DCS C = (E, ⊳), we associate a DRS R_{C} as follows:

• The terms of R_{C} are Lévy-equivalence classes ⟨α⟩_{L}, ⟨β⟩_{L}, … of finite configurations of C;

• The reduction relation of R_{C} consists of sets of pairs of terms u = (⟨α⟩_{L}, ⟨β⟩_{L}), where β = α ∪ {e}; (Note that u = ∅ iff ⟨α⟩_{L} = ⟨β⟩_{L} iff β ⊳ e.)

• The residual relation is defined as follows: if u = (⟨α⟩_{L}, ⟨α ∪ {e}⟩_{L}) and v = (⟨α⟩_{L}, ⟨α ∪ {e′}⟩_{L}), then u/v = (⟨α ∪ {e′}⟩_{L}, ⟨α ∪ {e′, e}⟩_{L}). (Thus u/v = ∅ iff ⟨α ∪ {e′}⟩_{L} ≈_{L} ⟨α ∪ {e′, e}⟩_{L}.)

Note that Stark’s encoding of DPESs into DCTSs [Sta89], which are DRSs as well, would (or at least may) interpret configurations that are different as sets (but may be the same semantically) as different states. For example, consider the DPES, corresponding to the rewrite system {f(x) → c, a → b} with the graph of t =

f(a) as the set of terms, whose events are t→^{a}f(b) and t →^{f(a)}c (the steps f(b) →^{f(b)}c

and t →^{f(a)}c represent the same event); and whose configurations are α = {f(a)}, β = {a}, and γ = {a, f(a)}. Then Stark’s encoding would consider α, β and γ as different configurations, while we can identify α with γ, which is more natural if the information that α ⊳ a is provided.

One can verify that R_{C} is indeed a DRS. The translation of DCSs into DRSs enables us to extend the theory of relative normalization from DRSs to DCSs, and in particular, to DPESs (since DPESs are DCSs with the empty ⊳ relation).

Theorem 6.2 Let S be a stable set of finite configurations in a Deterministic Computation Structure. Then execution of S-needed events leads to configurations in S, even if a finite number of S-unneeded events are executed as well.

7 Conclusions and future work

We have proven two abstract versions of the RN theorem: one in stable DRSs for regular stable sets R, and another in DFSs for all stable S. We believe that our first proof is the simplest existing proof among those using the residual notion, though it covers all the existing normalization results, except for the one in [GlKh94], which is covered by our second RN theorem. It is remarkable that, unlike the proofs in [CuFe58, HuLé91, BKKS87], our proof does not use the notion of standard reduction. Similar proofs for orthogonal CRSs in [KeSl89] and for orthogonal DAGs in [Mar91, Mar92] use an even stronger termination argument, expressed by the [termination] axiom; they used suitable labelling systems to define notions of family. Our second proof can be seen as a generalization of that proof method, which was used already by Lévy in [Lév78, Lév80]. It would be interesting to investigate whether it is possible to prove our second theorem already for stable DRSs, i.e., without family axioms, but possibly some much weaker axioms.

Obviously, our family axioms are too weak to prove certain properties of families which arise from using labelling notions, and studying its refinements certainly seems useful. Nevertheless, our axioms are powerful enough to build the normalization and optimality theory, and to bridge DRSs with Event Structures (thereby defining a denotational semantics for DRSs). Indeed, in DFSs it is possible to do much more – e.g., study infinitary normalization, define the notion of independence of computations, and turn Lévy’s reduction space into a Vector Space, etc. This is the subject of forthcoming papers. Some extra axioms on duplication behaviour are needed, but no nesting relation is necessary, so many machine models are still covered.

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

References

[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 the 4^{th} International Conference on Algebraic and Logic Programming, ALP’94, Madrid, Springer LNCS. vol. 850, p. 168-185, 1994.

[AFMOW94] Ariola Z.M., Felleisen M., Maraist J., Odersky M., Wadler P. A Call-By-Need Lambda Calculus. In: Proc. POPL’95, 1995.

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

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

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

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

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

[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, ed. Jerusalem, 1994, p. 144-165.

[GLM92] Gonthier G., Lévy J.-J., Melliès P.-A. An abstract Standardisation theorem. In: Proc. LICS’92, Santa Cruz, California, 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. Report. University of East Anglia, 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. van Eekelen, eds. Term Graph Rewriting: Theory and Practice. John Wiley, 1993.

[KKSV96] Kennaway J. R., Klop J. W., Sleep M. R, de Vries F.-J. Transfinite reductions in orthogonal term graph rewriting. Inf. and Comp., 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. RTA’93, Springer LNCS, vol. 690, C. Kirchner, ed. Montreal, 1993, p. 243-258.

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

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

[Lév78] Lévy J.-J. Réductions correctes et optimales dans le lambda-calcul, Thèse de

l’Université de Paris VII, 1978.

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

[Mar91] Maranget L. Optimal derivations in weak λ-calculi and in orthogonal Term Rewriting Systems. In: Proc. POPL’91, p. 255-269.

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

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

[Nök94] Nöcker E. Efficient Functional Programming. Compilation and Programming

Techniques. Ph.D. Thesis, Catholic University of Nijmegen, 1994.

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

[OR94] Van Oostrom V., van Raamsdonk F. Weak orthogonality implies confluence: the higher-order case. In: Proc. of the 3^{rd} International Conference on Logical Foundations of Computer Science, 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.

[Win80] Winskel G. Events in Computation. Ph.D. Thesis, Univ. Edinburgh, 1980.

[Yos93] Yoshida N. Optimal reduction in weak λ-calculus with shared environments. In Proc. of ACM Conference on Functional Programming Languages and Computer Architecture, FPCA’93, Copenhagen, 1993, p. 243-252.

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