An Abstract Theory of Optimal Evaluation ⋆

Zurab Khasidashvili

NTT Basic Research Laboratories Atsugi, Kanagawa, 243-01, Japan zurab@theory.brl.ntt.co.jp

John Glauert

School of Information Systems, UEA Norwich NR4 7TJ, UK jrwg@sys.uea.ac.uk

Abstract

This paper generalizes the Huet and Lévy theory of normalization by neededness and Lévy’s optimality theory to an abstract setting. We define Stable Deterministic Residual Structures (SDRS) and Deterministic Family Structures (DFS) by axiomatizing the residual and family relations in an Abstract Reduction 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’, and prove a Relative Optimality Theorem for DFSs. We further introduce and study a concept of implementation of DFSs. We show that for any DFS, its implementation is a non-duplicating DFS with zig-zag as the family relation, where zig-zag is simply the symmetric and transitive closure of the residual relation on redexes with histories. Optimal family-reductions in a DFS become needed reductions in the non-duplicating implementation DFS. We show that sharing formalized by our concept of a family is compositional: the sharing in a DFS can be decomposed into a weaker sharing, such as zig-zag, and a sharing in the implementation of the latter. These results arise from a study of the family relation in non-duplicating SDRSs. We show that zig-zag forms a family-relation in every non-duplicating SDRS, and that it is the only separable family relation in such SDRSs. To prove this, we develop an abstract extraction procedure, and to show that the family concepts defined via zig-zag and via extraction yield the same relation.

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

Preprint submitted to Elsevier Preprint 3 July 1998

1 Introduction

In order to achieve optimal evaluation of λ-terms, Lévy introduced a notion of redex-family to capture the concept of redexes of the ‘same origin’. The hope was that it would be possible to mimic multi-step reductions, which contract whole families in a term, by reduction of some graph representation, in which every multi-step would be represented by contraction of a single graph redex [50,51]. It is necessary to consider graph representations since Barendregt et al [9] showed that there exists no one-step optimal recursive β-reduction strategy on λ-terms. An optimal graph implementation has indeed been achieved by Lamping [49] and Kathail [30]. Maranget [52] generalized Lévy’s optimality theory to orthogonal Term Rewriting Systems (TRSs), Gonthier et al [23] simplified Lamping’s technique, and Asperti and Laneve generalized both Lévy’s optimality theory and Gonthier’s implementation to Interaction Systems, which cover most of the languages with a constructordestructor discipline [4,5]. More recently, van Oostrom generalized the optimality theory to the whole class of orthogonal Higher-Order Rewriting Systems (HORSs) [62], and Guerrini developed a general theory of sharing-graph rewriting [25].

Lévy introduced the family concept in three different ways: via an appropriate notion of labelling, via extraction, and by zig-zag. He showed that they all yield the same concept, in the λ-calculus. The same holds for all orthogonal HORSs R if all three family concepts are defined in the refinement of R which decomposes every original R-step into first-order, or TRS, step and a number of substitution steps [62]. However, the zig-zag family can be defined directly in R, and this yields a different, and weaker, family concept [4]. Independently, though much earlier, Kennaway and Sleep [32] defined a concept of labelling for orthogonal Combinatory Reduction Systems (CRSs), which covers orthogonal TRSs and Interaction Systems, improving Klop’s original labelling system for CRSs [46]. Their labelling is different from both Maranget’s labelling for orthogonal TRSs [52] and Asperti-Laneve’s labelling for Interaction Systems [4].

In addition to this variety of family concepts, alternative graph rewriting algorithms have been developed for optimal implementation of orthogonal rewriting systems, such as Term Graph Rewriting [33], Jungle Rewriting [27], and many others, inspired by Wadsworth’s pioneering work on graph-based implementation of the λ-calculus [69]. The challenge is to develop an abstract notion of family general enough to cover all the existing notions, but refined enough to support proofs of normalization and optimality results. Usefulness and feasibility of such a theory was pointed out early on by Berry and Lévy in [12]: ‘Thus a unifying or axiomatized point of view should be adopted to preserve the syntactic results of this paper. This seems possible along the lines of O’Donnell [60] and Rosen [66]. Furthermore, the axiomatized approach should include the λ-calculus where much of the syntactic part of this paper is valid’.

This work is the first step towards developing an axiomatic theory of optimality. We define a Deterministic Family Structure (DFS) as a Deterministic Residual Structure (DRS) with axiomatized family and contribution relations. The family relation in a DFS is simply an equivalence relation containing zig-zag, and the contribution relation expresses causal dependencies among families and is formalized in terms of creation of redexes. All existing family relation definitions in the literature [50,46,32,53,4,62] satisfy our DFS axioms. A DRS in turn is an Abstract Reduction System (ARS) which has a residual relation between redexes in the source and target terms of each transition t→^{u}s. 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 (many-step) reductions, and permutation-equivalence on reductions, referred to below as Lévy-equivalence, and the Lévy-embedding relation, is introduced, as is done for the λ-calculus in [50,51]. Sufficient conditions needed to define permutation equivalence in an abstract setting were stated by Stark [68] (independently from Lévy [50,51], for the case when the residual relation is non-duplicating), and by Gonthier et al. [24].

We first address the problem of normalization in DRSs. 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. For example, it is well known that the leftmost-outermost strategy is normalizing in the λ-calculus [16]. For Orthogonal TRSs, a general normalizing strategy, called the needed strategy, was found by Huet and Lévy [29]. 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. (They also defined strongly sequential orthogonal TRSs where a needed redex can be computed effectively in every reducible term. We will not discuss this topic here.)

This fundamental work on neededness has been extended in several directions. Barendregt et al. [10], Maranget [53], Nöcker [59] and Middeldorp [57] studied neededness w.r.t. head-normal forms, weak head-normal forms, constructor head-normal forms, and root-stable forms, respectively. Sekar and Ramakrishnan [67] studied normalization via necessary sets of redexes. Kennaway et al. [34] studied a needed strategy for infinitary orthogonal TRSs. A different approach to normalization is developed in Kennaway [31] and Antoy and Middeldorp [2]. Antoy et al. [1] designed a needed narrowing strategy. Gardner [17] described a complete way of encoding neededness information using a type assignment system.

In [18,22], the present authors addressed the question of normalization relative to a desired set of final terms, considering the properties that a set S of terms must possess in order for the neededness theory of Huet and Lévy still to make sense. This work is done in the context of orthogonal Expression Reduction Systems (ERSs) [36], a form of higher-order rewriting which subsumes Term Rewriting and the λ-calculus. Natural conditions were 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 (that is, not in S-normal form) has at least one S-needed redex, and repeated contraction of such redexes always leads to an S-normal form. 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, and minimal (w.r.t. the Lévy-embedding relation) S-normalizing reductions exist.

Here we further generalize the theory by abstracting from the structure of terms. We study relative normalization in DRSs. Despite their highly abstract nature, a counterpart of the stability property of Berry [11] and Winskel [71] enables us to prove the RN theorem for all regular stable sets S. (We actually prove the Relative Hypernormalization theorem.) We show that without this stability axiom the theorem fails. The proof method employed is similar to that in [35,37] (it was discovered by the author independently from [29]), 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.

Since for irregular stable S, S-unneeded redexes can duplicate S-needed ones, the above proof method does not apply for all stable DRS (SDRSs); for the same reason, the S-needed strategy is no longer hypernormalizing. However, the DFS axioms (in particular, a strong termination axiom [FFD]) ensure that any S-normalizing reduction can be transformed into an S-needed Snormalizing one by pushing S-needed steps forward, and that all S-needed reductions are eventually terminating (at a term in S). Furthermore, for DFSs we show that a strategy that contracts, in an arbitrary order, redexes that belong to S-needed families, but which need not be S-needed themselves, is still S-normalizing. As a corollary, any S-needed complete family-reduction, which in any term contracts all members of a family containing an S-needed redex in a multi-step, is eventually S-normalizing. Using the same method as in [51], we show that the latter reductions are also optimal in the sense that they reach S in a least number of family-reduction steps.

In order to provide an abstract criterion for correctness of a graph implementation of complete-family reductions, we introduce an abstract concept of Lévy-implementation: With a DFS we associate a non-duplicating DRS, called its implementation, whose steps exactly correspond to complete familyreduction steps in the original DFS. For example, implementation DRSs can model sharing-graph implementations of Lévy’s complete family-reductions in the λ-calculus (modulo ‘book-keeping’ steps which in general can be prohibitively expensive [6]). It is not difficult to show that needed (w.r.t. a stable set of results) reductions in the implementation DRS correspond exactly to needed complete family-reductions in the original DFS, implying that the former DRS indeed implements optimal computations in the latter DFS, in the sense of Lévy [50,51].

Further, we show that the family relation in the implementation DRS induced by the original DFS coincides with zig-zag, which is the weakest family sharing (by our definition of families). Note that a family relation in a (non-duplicating or duplicating) DRS need not coincide with zig-zag. An example is Asperti and Laneve’s concept of family for Interaction Systems [4], where unlike the λcalculus a single redex can create multiple members of a family which cannot be related by zig-zag (without employing the internal structure of reduction steps). In non-duplicating DRSs, we call such families non-separable.

Actually, we show that the sharing concept formalized in DFSs is (de)compositional: any sharing can be decomposed into a weaker sharing and a nonseparable sharing in the non-duplicating DRS implementing that weaker sharing. To this end, we investigate the family relation in non-duplicating DFSs. We show that zig-zag forms a family-relation in every non-duplicating SDRS, and that it is the only separable family relation in such SDRSs. These results are obtained by defining an abstract extraction procedure for non-duplicating SDRSs and showing that zig-zag coincides with our extraction-family relation. The technical contribution here is the simplicity of our construction which avoids irrelevant syntactic complications, such as those related to the topdown and left-to right nature of the conventional concept of standardization.

The paper is organized as follows. In the next section, we introduce SDRSs and prove some fundamental lemmas concerning (mutually) external reductions. 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 SDRSs, and prove the Relative Normalization and Optimality theorems for any stable set S of results. Section 5 gives a characterization of zig-zag relation via extraction in nonduplicating SDRSs, used in Section 6 to prove that, in every non-duplicating SDRS, zig-zag is a family relation, and moreover, is the unique separable family-relation. In Section 7 we define and study implementation DRSs, and show the (de)compositionality of sharing. Conclusions appear in Section 8.

It should be remarked that it is not the aim of this paper to provide a comprehensive abstract theory of normalization and optimality that can readily be applied to particular (syntactic) systems covered by SDRSs and DFSs. In particular, it cannot replace the syntactic studies of normalization and optimality in the literature (part of which was mentioned above): some of our axioms are non-trivial to verify for particular systems, and we do not cover all aspects of the subject. Rather, we try to bring out and analyze some of the main principles and methods on which the theory of normalization and optimality is based. And although our abstract framework is very general, our results and proofs are far from trivial and do save considerable work for particular systems.

The results of this paper have been reported in [20,21,41,45]. Some results are taken from [39,40]

2 Deterministic Residual Structures

In this section we define Deterministic Residual Structures (DRSs) which are Abstract Reduction Systems (ARSs) satisfying certain properties concerning residuals. Residuals of redexes were first introduced and studied by Church and Rosser in the λI-calculus [14].

The definition and some results about ARSs can be found e.g., in [47,28]. Our definition is slightly different, and follows that of Hindley [26].

Definition 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. (Klop’s ARSs [47] 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. |P | denotes the length of P. P + Q denotes composition (or concatenation) of P and Q. We use U, V, W to denote sets of redexes of a term.

DRSs are similar to Determinate Concurrent Transition Systems (DTCS) of Stark [68], to Abstract Reduction Systems (ARSs) of Gonthier et al. [24], and to van Oostrom’s orthogonal Descendant Rewriting Systems [61]. The main difference from DCTSs is that Stark requires a non-duplicating residual relation, and distinguishes a start state. Unlike ARSs of [24], we do not have a nesting relation on redexes and the corresponding axioms, and the stability axiom is modified accordingly. Instead, we study properties of conflict-free transition and reduction systems based on the duplication and erasure effect of executed transitions on the others, and develop a theory that is applicable to systems with nested transitions too. The difference from van Oostrom’s orthogonal 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; and the [weak acyclicity] axiom below is not required there. Closely related abstract reduction systems are studied in [54,65].

Definition 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, and if moreover v ≠ u, then u discards v. A redex of s which is not a residual of any v ∈ t under u is said to be u-new or created by u. The set v/P of residuals of v under any reduction P is defined by transitivity.

A development of U ⊆ t is a reduction P : t → → that only contracts residuals of redexes from U; it is complete if U/P = ∪_{u∈U} u/P = ∅. 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:

[FD] ( Finite Developments [24]) All developments are terminating; all complete developments of U ⊆ t end at the same term; and residuals of a redex v ∈ t under all complete developments of U are the same.

[weak acyclicity] ([68]) Let u, v ∈ t, u ≠ v, and u/v = ∅. Then v/u ≠ ∅.^{1}

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 along u/v.

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

One can verify that all orthogonal (first or higher-order, see e.g., [65]) term rewriting systems, such as the λ-calculus, form DRSs. These systems are stable, and can be shown so just using an appropriate notion of descendant which assigns the contractum to the contracted redex – labelling is not necessary. Further, orthogonal Term Graph Rewriting Systems [33], which are equivalent to orthogonal DAG (Directed Acyclic Graph) rewriting systems defined

1 This axiom is called [acyclicity] in [20], and is axiom (4) in [68].

via labelled orthogonal TRSs [52,53], are DRSs but they do not satisfy all the nesting axioms of [24]. Similarly, Interaction Nets [48] form DRSs (when restricted to finite nets), and they do not have or need any nesting order on redexes (as nets are undirected, and possibly cyclic, graphs).

The properties of the residual relation in orthogonal systems are all standard [29,50,12,51,13,68,54], and we only review quickly the main constructions used in this paper. In a DRS R, Lévy-equivalence or permutation-equivalence is defined as the smallest relation on co-initial finite 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 sets of redexes in the same term. 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 Q/(P_{1} + P_{2}) = (Q/P_{1})/P_{2}. Further, the Lévy-embedding relation on coinitial finite reductions, ⊴_{L}, is defined by: P ⊴_{L} Q iff P/Q = ∅. One can show that P ≈_{L} Q iff P ⊴_{L} Q and Q⊴_{L} P and that P ⊴_{L} Q iff Q ≈_{L} P +N for some N. Intuitively, P ⊴_{L} Q expresses that Q does more work than P, and Q/P is the part of Q that remains after P has been done. Finally, one can prove the following strong Church-Rosser theorem for DRSs: For all co-initial finite reductions P and Q in a DRS, P ⊔ Q ≈_{L} Q ⊔ P, where P ⊔ Q abbreviates P + Q/P.

To show that the above definitions are sound, it is convenient to consider multi-step reductions, where a multi-step contracts simultaneously, or in parallel, a set of redexes in a term; thus a multi-step can be seen as a complete development of a set of redexes, and it is conventional to switch freely between multi-steps and complete developments. Now for example correctness of the above definition of residuals for reductions can be proved by induction on the number of multi-steps in P_{1}, P_{2} and Q, where steps in these reductions are viewed as multi-steps contracted singleton sets of redexes. These induction is equivalent to induction on multi-diagrams, which are diagrams of the form:

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

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

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

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

where each arrow represents a multistep, and each inner square is yielded by the equation U + V/U ≈_{H} V + U/V, where U and V as well as U/V and V/U are multi-steps. Here ≈_{H} is Hindley-equivalence, which is defined for finite co-initial reductions as follows: P ≈_{H} P′ iff they end at the same term and for any redex u in the initial term, the residuals of u under P and under P′ are the same redexes. The induction principle is then to infer a property for such a multi-diagram from properties of its proper sub-diagrams. For example, the correctness of definitions (P_{1} +P_{2})/Q = P_{1}/Q+P_{2}/(Q/P_{1}) and Q/(P_{1} +P_{2}) = (Q/P_{1})/P_{2} can be inferred from the following multi-diagram:

[figure: ·; P_{1}; ·; P_{2}; ·; ·; Q; P_{1}/Q; ·; Q/P_{1}; P_{2}/(Q/P_{1}); ·; Q/(P_{1} + P_{2})]

However, it is not necessary to switch to multi-steps in order to provide a sound induction principle for definitions and proofs involving many-step reductions. (Otherwise, the ‘trick’ of using multi-step reductions would not be sound!) Klop’s commutative diagrams can be used instead [46]. Klop diagrams are constructed using developments rather than multi-steps, and this involves ‘splitting’ of elementary (or one-step) diagrams. The following is a simple example of a Klop-diagram:

[figure: ·; ·; ·]

[figure: ·; ·; ·]

[figure: ·; ·; ·; ·]

where arrows now represent reduction steps, not multi-steps, and each inner square is again yielded by the equation U +V/U ≈_{H} V +U/V where U and V as well as U/V and V/U are now complete developments of respective sets of redexes. Both multi-step and Klop diagrams use empty (multi-) steps to retain the rectangular shape of the diagrams. Construction of a Klop-diagram need not terminate in general, but it always does for reductions in DRSs, by virtue of the [FD] axiom. Construction of Klop diagrams is also well described in [8], for the case of the λ-calculus. We will often use Klop diagrams in proofs. In which case P/Q, say is considered as a reduction rather than a multistep reduction, and is thus only unique up to the particular sequentializations of corresponding multi-steps. (However, P/Q is defined more precisely than up to ≈_{L}.) In conclusion, we note that instead of [FD] in the definition of DRSs, we could require equivalently only termination of developments and the following strong local commutativity property: for all co-initial redexes u and v, u ⊔ v ≈_{H} v ⊔ u.

The [stability] axiom is not used in the above constructions. 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 which captures the concept that two external reductions do not contract redexes that have common residuals (although the contracted redexes may have ‘inessential’ common ancestors).

Definition 3 • Let u ∈ U ⊆ t and P : t → → o. 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} → → t_{n} and Q : t_{0} = s_{0} → →^{Q_{j}} s_{j}→^{v_{j}}s_{j+1} → → s_{m}. Let

U_{i,j} = u_{i}/(Q_{j}/P_{i}) and V_{i,j} = v_{j}/(P_{i}/Q_{j}) (see diagram). We call P external to Q if for any i, j, U_{i,j} ∩ V_{i,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 4 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 the set U′ = U/Q_{0}.

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)

(see the figure). 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′.

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

We conclude this section by proving two fundamental lemmas, which generalize the [weak acyclicity] and [stability] axioms to many-step reductions, and are used repeatedly throughout the paper

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

Proof We show that P/N = ∅ implies N/P ≠ ∅ by induction on the number of elementary diagrams in a Klop diagram D(P, N) of P and N. It follows from Definition 3 that the top and left edges of all sub-diagrams of D(P, N) are external reductions, therefore the induction is sound. So let P/N = ∅. If |P | = |N| = 1, we have N/P ≠ ∅ by [weak acyclicity]. Otherwise, let say |P | > 1, let P : t → →^{Q} e→^{v}o, and let N^{∗} = N/Q (see the figure). By the induction assumption, N^{∗} ≠ ∅. So let N^{∗} = N′ + w, where w is the last (nonempty) step of N^{∗}, and let V = v/N′. Again by the induction assumption, w/V ≠ ∅. Hence N/P ≠ ∅.

[figure: t; Q; e; v; o]

[figure: ·; N′; V; ·]
[figure: s; N; ∅; s; w; ∅; s]

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

[figure: t; P; s ⊇ W; e; Q; P/Q; o ⊇ W/(Q/P); Q/P]

Proof By induction on the number n of elementary diagrams in the Klop diagram D(P, Q) of P and Q. The case n = 1 is the axiom [stability]. It follows from Definition 3 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). Let W^{∗} = W/(Q/P) ≠ ∅.

If |P | = 1 and |Q| > 1, say Q = v + Q′, then W′ = W/(v/P) ≠ ∅, and by [stability] redexes in W′ are created by P/v. By the induction assumption, redexes in W^{∗} are created by P/Q and Q′/(P/v) is external to W′, implying that Q/P = v/P + Q′/(P/v) is external to W.

[figure: t; v; ·; Q′; e; W ⊆ s; P; v/P; s′ ∋ W′; P/v; Q′/(P/v); ·; P/Q]

Now it remains to consider the case when |P | > 1, i.e., P = u + N with |N| > 0 (see the figure below). 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 4, Q/P = (Q/u)/N is external to the set 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.

t  [figure: Q] e

[figure: W_{u} ∈ o; u; Q/u; o′ ∋ W_{u}/(Q/u); u/Q]

[figure: W ∈ s; N; (Q/u)/N; s′ ∋ W^{∗}; N/(Q/u)]

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.

Definition 7 Let S be a set of terms in a DRS R.

(1) We call a redex u ∈ t S-needed if at least one residual of it is contracted in any reduction from t to a term in S, and call u S-unneeded otherwise.

(2) We call S 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.

(3) We call a stable set S regular if in no term can an S-unneeded redex duplicate an S-needed one.

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. For simplicity, we only consider stable sets that are closed under reduction, although the theorem holds for all stable sets as shown in [18,22]; obviously, closure under reduction implies closure under parallel moves.

Examples of stable sets are normal forms [29], head-normal forms in the λcalculus [10], weak-head-normal forms in the λ-calculus, constructor-head-normal forms for constructor TRSs [59], and root-stable forms in orthogonal TRSs [57]. 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) [73], the set of answers in the call-by-need λ-calculus of Ariola et al. [3], and flexible generalized-head-normal forms in the λ_{hd}^{v}-calculus of Xi [72]; all are conditional rewrite systems. An example of an orthogonal TRS with an irregular stable S is given in Remark 16.

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

Lemma 8 For any stable S, residuals of S-unneeded redexes of a term t under any reduction P : t → → s remain S-unneeded.

Proof Let u ∈ t be S-unneeded, and let v be a P -residual of u. Then there is an S-normalizing reduction Q : t → → o that is external to u. By Lemma 4, Q/P is external to v, thus v is S-unneeded (as Q/P is S-normalizing by stability of S).

Lemma 9 Let S be stable, let t ∉ S, let t→^{u}e, let u be S-unneeded, and let w ∈ e be a redex created by u, in a stable DRS. Then w is S-unneeded.

Proof If e ∈ S, then every redex in e, including w, is S-unneeded. But suppose e ∉ S: Since u is S-unneeded, there is an S-normalizing P : t → → s that does not contract residuals of u. By Lemma 6, 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 10 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 does not 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 does not contain an S-needed redex.

Definition 11 We call P : t_{0} → t_{1} → … S-(un)needed if it contracts only S- (un)needed redexes. We call P S-quasi-needed if it contracts infinitely many Sneeded redexes, and call it S-semi-needed if it can be expressed as P = P_{1}+P_{2} where P_{1} is S-needed and P_{2} is S-unneeded. 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 set of terms S in an SDRS R, transforms any finite or infinite reduction P into an S-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 u is S-unneeded and v is S-needed. Let P = P_{1} + P_{0} + P_{2}. By Lemma 9, v is a residual of a redex v′ ∈ t, which is S-needed by Lemma 8. Since S 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 S, the number of S-unneeded steps in P′ preceding v′ is less than the number preceding v in P, and the number of S-needed steps in P and P′ coincide.

For the above transformation procedure to terminate, instead of regularity of S it would be enough to require that an S-needed redex had at most one Sneeded residual under an S-unneeded step. Termination of the transformation procedure is crucial for our method for proving termination of any S-needed reduction starting from an S-normalizable term.

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

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

(2) If P is S-quasi-needed, then K(P) is an infinite S-needed reduction.

Proof

(1) Since the transformation K does not change the number of S-needed steps in P, it follows that K(P) is S-semi-needed, and it ends at S since K(P) ≈_{L} P. The step of K(P) entering S is the last S-needed step of K(P) by stability of S.

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

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

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

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

Lemma 14 Let t_{0} have an S-quasi-needed reduction and t_{0}→^{u}s_{0}. Then s_{0} also has an S-quasi-needed reduction.

Proof By Lemma 12, t_{0} has an infinite S-needed reduction P : t_{0}→^{u_{0}}t_{1}→^{u_{1}} . . .. Let U_{i} = u/(u_{0}+…+u_{i−1}), i = 0, 1, … (see the diagram below). 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 13, u_{k} has at least one S-needed U_{k}-residual in s_{k}, i.e. u_{k}/U_{k} contains at least one S-needed step. Hence P/u is S-quasi-needed.

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

Theorem 15 (Relative Hypernormalization) Let S be a regular stable set of terms in a stable DRS R, and let t ∉ S be a term in R. Then (1) t contains at least one S-needed redex.

(2) t has an S-normal form iff it does not possess a reduction in which infinitely many times S-needed redexes are contracted.

Proof

(1) By Definition 7 if t is not S-normalizing, and by Lemma 12 otherwise.

(2) (⇒) Let t → →^{P} s ∈ S. Suppose on the contrary that there is an S-quasi-needed Q starting from t. Then by Lemma 14 Q/P is S-quasi-needed as well – a contradiction, since all terms of Q/P are in S, by the closure of S under reduction, and therefore Q/P must be S-unneeded.

(⇐) By (1), one can repeatedly contract S-needed redexes in t, unless a term in S is reached; the latter is inevitable since t does not have an infinite S-needed reduction.

Remark 16 If S is not regular, then Lemma 12 need not hold. Indeed, consider the example from [18,22]: take R = {f(x) → h(f(x), f(x)), a → b} and take for S the set of terms not containing occurrences of a. It is easy to check that S is stable, but is not regular, since the outermost redex in t = f(a) is S-unneeded, while the innermost one is S-needed. Then the reduction 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 14 fails, and the S-needed strategy need not be hypernormalizing.

4 Relative Normalization and Optimality in Deterministic Family Structures

In order to generalize the RN theorem to all stable sets in DRSs, and to prove a Relative Optimality theorem, 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 [18,22] for all DFSs, and makes explicit the properties of a family relation needed to develop an abstract theory of optimal normalization.

Definition 17 (Deterministic Family Structure) A Deterministic Family Structure (DFS) is a triple F = (R, ≃, ↪), where R is a DRS; the family relation ≃ 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 ⊴_{L} 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. 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) Further, ≃ and ↪ satisfy the following axioms:

[initial] Let u, v ∈ t and u ≠ v, in R. Then F am(∅_{t}u) ≠ F am(∅_{t}v), where ∅_{t} is the empty reduction starting from t.

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

in ϕ.

[creation] Let e → →^{P} t→^{u}s, and let u create v ∈ s. Then F am(u) ↪ F am(v), or more precisely, F am(P u) ↪ F am((P + u)v).

[FFD] ( Finite Family Developments) Any reduction that contracts redexes of a finite number of families is terminating.^{2}

Note that the [contribution] can be viewed as a definition of ↪ rather than as an axiom. Hence sometimes we will consider a DFS as a pair F = (R, ≃).

One can check that all the existing definitions of family relation in the literature [50,46,32,53,4,62] satisfy the above axioms, thus our definition is consistent. Indeed, validity of the first three axioms follow immediately from the structure of labels in the labelling definitions of these families. The axiom [FFD] had been proved separately for all the above systems using the syntax in [50,46,63]. An axiomatic approach to [FFD] is developed in [54], but it is not fully general as for example it does not apply to all orthogonal higher-order or graph rewriting systems [63,54]. Since there are many different (and perhaps incompatible) ways to construct a DFS from a stable DRS, and since we want to be as general as (reasonably) possible, we do not investigate here any finer axiomatization of the residual relation that would imply [FFD]. The reason for considering notions of family other 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. Further, there are well-behaved sharing mechanisms, such as the one in [4], that are strictly larger than zig-zag (when we regard the reduction system as a DRS). We will comment on this below. Moreover, as we will see, our sharing concept has the nice property of compositionality, facilitating study of complex concepts of family.

Despite its generality, our family concept does not cover all possible sharing concepts studied in the literature. For example, consider the TRS from [27] for computing Fibonacci numbers, having the following three rules: fib(0) → 0, fib(succ(0)) → succ(0) and fib(succ(succ(n))) → fib(succ(n)) + fib(n),

2 This axiom is called [termination] in [20].

and rules for functions 0, succ and +; and consider the reduction:

fib(succ^{4}(0))
→ fib(succ^{3}(0)) + fib(succ^{2}(0))
→ fib(succ^{2}(0)) + fib(succ^{1}(0)) + fib(succ^{2}(0))
→ …

In the Jungle Graph implementation of that TRS [27] (which allows ‘accidental’ sharing of possibly completely unrelated, but graphically equal, subterms), it is possible to share the two occurrences of fib(succ^{2}(0)) in the last term, but (by [contribution]) the two occurrences cannot be considered as members of the same family since (by [creation]) they have different contributor families.

Let us call ⌈ϕ⌉^{≤} = {ϕ_{i} | ϕ_{i} ↪ ϕ} the cone of ϕ. It follows immediately from the family axioms that:

Proposition 18 In any DFS F:

[irreflexivity] ϕ ↛ ϕ. [transitivity] If ϕ ↪ ϕ′ and ϕ′ ↪ ϕ′′, then ϕ ↪ ϕ′′.

[cone] ϕ ↪ ψ ⇒ ⌈ϕ⌉^{≤} ⊂ ⌈ψ⌉^{≤}. (i.e., ⌈ϕ⌉^{≤} ⊆ ⌈ψ⌉^{≤} and ⌈ϕ⌉^{≤} ≠ ⌈ψ⌉^{≤}). [finiteness] For any ϕ, ⌈ϕ⌉^{≤} is finite, and ⌈∅_{t}u⌉^{≤} = ∅ for any u ∈ t. [antisymmetry] If ⌈ϕ⌉^{≤} = ⌈ψ⌉^{≤} and ϕ ≠ ψ, then ϕ ↛ ψ (and ψ ↛ ϕ).

Proof [irreflexivity], [transitivity], and [finiteness] follow immediately from [contribution]. [cone] follows from [irreflexivity] and [transitivity]. [antisymmetry] follows from [cone].

The following example shows that, in a stable DRS with ≃ and ↪, [initial],

[creation] and [contribution] do not imply [FFD].

Example 19 Consider the ARS R given by the figure 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, and 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 except [FFD] are satisfied too. Note that the DRS R is stable.

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

Lemma 20 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, ⌈F am(w′)⌉^{≤} = ∅ if w′ is not a created redex, and ⌈F am(w′)⌉^{≤} = {F am(v)} otherwise; and ⌈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}⊆≃).

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

Example 21 Consider the DRS R given by the figure below, 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 R is not stable.

[figure: t; u; e; w; o^{∗}]

[figure: s; v; u′; o; v′]
[figure: w^{∗}]
[figure: o^{∗}; w′; ∅; o^{∗}; ∅]

Lemma 22 Let S be stable, let t ∉ S, let t→^{u}t′, let u be S-unneeded, and let u′ ∈ t′ be a redex created by u, in a DFS F. Then u′ also is S-unneeded.

Proof By Lemma 9 and Lemma 20.

Now we can generalize the RN theorem, proved in [18,22] for orthogonal ERSs, to all DFSs. In the following we allow for arbitrary stable sets S.

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

Theorem 23 (Relative Normalization) Let S be a stable set of terms in a DFS 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, u is S-needed. By Lemma 8 and Lemma 22, 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 figure below). By ≃_{z}⊆≃, F AM(P_{i}) ⊆ F AM(P) (families are considered with respect to t). 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 [FFD].

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

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

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

Lemma 24 Let S be a stable set of terms in a DFS F, and let t→^{u}s. Then any S-needed redex v ∈ t different from u has an S-needed residual in s.

Proof Same as the proof of Lemma 13, but using Theorem 23 instead of Lemma 12.

We now 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 [51] to all stable sets S in any DFS.

Definition 25 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 26 Let S be a stable set of terms in a DFS F, and let t be an Snormalizable term in F. Then any weakly S-needed reduction starting from t is terminating.

Proof By [FFD], since there is only a finite number of S-needed families relative to t (that number does not exceed the length of any S-normalizing reduction starting from t).

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

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

Lemma 28 Let S be a stable set of terms in a DFS F. Then any sequentialization of an S-needed family-reduction is weakly S-needed.

Proof Let P : t_{0} → →^{U_{0}} t_{1} → →^{U_{1}} … → →^{U_{k−1}} t_{k} be an S-needed family-reduction, and let u_{i} ∈ U_{i} be S-needed (i = 0, …, k − 1). We need to show that U_{i} (with history P_{i} : t_{0} → →^{U_{0}} … → →^{U_{i−1}} t_{i}) is an S-needed family, i.e., any S-normalizing reduction Q starting from t_{0} contracts at least one redex in the family of U_{i}. By closure of S under reduction, Q/P_{i} is S normalizing (for every i), and by S-neededness of u_{i}, Q/P_{i} contracts at least one residual of u_{i}, thus Q indeed contracts a redex in the family of U_{i}.

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

Lemma 30 (Unique Families) 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 ⌈F am(U_{i})⌉^{≤} ≠ ⌈ϕ⌉^{≤}, and (b)_{n} follows.

Theorem 31 (Relative Optimality) Let S be a stable set of terms in a DFS F, and let t be an S-normalizable term in F. Then any S-needed Snormalizing complete family-reduction Q : t → → e ∈ S is S-optimal in the sense that it has the minimal number of family-reduction steps.

Proof As in the λ-calculus [51]. Let P : t → → s be an S-normalizing familyreduction. It follows from the proof of Theorem 23 that F AM(Q) ⊆ F AM(P) (see the figure for Theorem 23). Hence, by Lemma 30, ∥Q∥ = n(F AM(Q)) ≤ n(F AM(P)) ≤ ∥P ∥, where n(F AM(Q)) denotes the number of families in F AM(Q).

5 Equivalence of Zig-zag and Extraction in Affine SDRSs

We will use the term Affine Stable Deterministic Residual Structure (ASDRS) for an SDRS with a non-duplicating residual relation. In this section, we introduce an abstract extraction algorithm for ASDRSs and show that zig-zag related redexes (with histories) have the same canonical representatives w.r.t. extraction, up to an equivalence on histories. These canonical representatives are obtained as normal forms of redexes with histories P v w.r.t. the extraction procedure, which eliminates all steps of histories P that do not ‘contribute’ to the family of v.^{3}

Lévy introduced an extraction procedure for the λ-calculus in [50,51] in order to prove decidability of the family relation. His extraction procedure is effective, and gives canonical representatives of families, which are unique, thus implying the decidability of the family relation. For higher order rewrite systems, whose reduction steps are more complicated, there are two conceptually different extensions of Lévy’s extraction algorithm. The first is due to Asperti and Laneve [4], and the second to van Oostrom [62].

A ‘problem’ arises because a redex can create a number of redexes ‘intuitively’

3 The extraction process was thought to require the syntactic structure of terms. To quote Lévy [51]: ‘We turn now to the hard part of this paper, which is to show that the family relation is decidable. The trouble comes from the necessity of looking now inside λ-expressions and from not being able to go on with algebraic manipulations’.

in the same family without the help of previous steps, something which cannot happen in the λ-calculus or term rewriting. That these redexes are intuitively in the same family, can be seen after decomposing the rewrite step into two parts – the TRS part that only creates new symbols, and the substitution part, that performs all (often nested) substitutions. The substitution part can duplicate or erase the redexes created during the TRS part, and all substitution copies of a redex created by the TRS-part are viewed as belonging to the same family, as the labels of such redexes are the same. Such redexes cannot be related by the zig-zag if one works with the original system [4], but can be related if one works in the refinement of the original system [62]. Now, the difference between the two approaches is that Asperti and Laneve decided to accept the inadequacy of the zig-zag, but extended Lévy’s extraction algorithm by the shift operation which relates all copies of the simultaneously created redexes of the same family to a canonical representative, thus making extraction match the labelling; the resulting family-relation is non-separable – a redex can create multiple members of the same family simultaneously. On the contrary, van Oostrom works with the refined rewrite systems and no operation like shift is necessary to ensure coincidence of labelling, extraction and zig-zag families. Since we want to define an extraction procedure adequate for zig-zag, we do not need an operation modelling shift. Our results in Section 7 will shed further light on the separability problem.

Another relevant extraction procedure is studied by Kennaway et al. [33] for orthogonal Term Graph Rewriting Systems (TGRSs). That paper is concerned with Event Structure [70,58,71] semantics for orthogonal TGRSs and does not mention families explicitly : pre-events there correspond to redexes with histories. The extraction algorithm in [33], called there the minimization algorithm, is based on a syntactic concept of the contribution relation on redexes and is technically different from our extraction algorithm. Note that TGRSs are nonduplicating rewrite systems, hence our extraction algorithm, as well as other results in this paper concerning ASDRSs, apply to orthogonal TGRSs.

We start by studying standard reductions in ASDRSs. Our standardization concept differs from the usual ‘left-to-right and outside-in’ concept of standardization in the λ-calculus [16]. Our standard reductions are simply ‘selfneeded’ reductions – reductions in which every step essentially contributes to the whole computation – since we do not have any nesting relation imposed on redexes, unlike in the ARSs of [24], and there is no concept of ‘left’ or ‘right’ occurrences in DRSs. However, our concept of standardization captures the essence of the usual notion in many respects. In particular, in the extraction process which we study below, self-needed reductions play the same role as leftto-right outside-in standard reductions in the extraction processes of [51,4,62]. For a theory of standardization for stable DRSs in general, see [39,40]. And for an ‘outside-in theory’ of standardization in ARSs with an axiomatized nesting relation, see [24,54].

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

• We call u P -needed if there is no Q ≈_{L} P that is external to u, and call it

P -unneeded otherwise.

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

• Let Q : t → → o, P : t → →^{P′} s → → e, and u ∈ s. We say that u is Q-needed, or more precisely, P′u is Q-needed, if u is Q/P′-needed. We call P Q-needed if every redex contracted in P is. We call P self-needed or standard if it is P -needed. The other concepts above are extended in the same way.

Note that P -neededness and P -erasure do not depend on the choice of a reduction in the class ⟨P ⟩_{L} of reductions Lévy-equivalent to P, since u/P = u/Q when P ≈_{L} Q. The external and discards concepts however do depend on the particular reduction in the Lévy-equivalence class.

Lemma 33 Let P : s → → t→^{u}e → →^{P′} o in an ASDRS.

(1) If P : s → → s′→^{w}o, then w ∈ s′ is P -needed.

(2) If u creates v ∈ e and is P -unneeded, then so is v.

(3) If u ≠ v ∈ t, then v is P -needed iff it has a P -needed residual in e.

Proof

(1) By Lemma 5 (Weak Acyclicity Lemma), there is no Q : s′ → → o such that Q is external to w and Q ≈_{L} w. Hence w is w-needed, i.e., is P -needed.

(2) Since u is P -unneeded and P -erased, there is Q_{t} ≈_{L} u+P′ that discards u. By Lemma 6 (Stability Lemma), Q_{e} = Q_{t}/u is external to v, and Q_{e} ≈_{L} P′. Hence v is P -unneeded.

(3) (⇒) If on the contrary v/u = ∅, then u + P′ would discard v, contradicting P -neededness of v. So let v′ be the only u-residual of v. 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 – a contradiction.

(⇐) Let v have a P -needed residual v′′ ∈ e. If on the contrary v is P - unneeded, there is Q_{t} ≈_{L} u + P′ that is external to v. Hence u/Q_{t} = ∅ (since u/(u+P′) = ∅) and Q_{e} = Q_{t}/u ≈_{L} P′. By Lemma 4, Q_{e} is external to v′′, contradicting P -neededness of v′′.

The following is a standardization procedure for reductions in ASDRSs.

Definition 34 Let P : t → → s. The canonical standard variant of P, ST (P), is defined as follows: If P = ∅, then so is ST (P). Otherwise, let v ∈ t be such that it is P -needed and its residual is contracted in P first among P -needed residuals of P -needed redexes in t (existence of such v follows from Lemma 33).

Then ST (P) = v + ST (P/v).

Theorem 35 (Standardization) For any finite reduction P in an ASDRS, ST (P) is a finite standard reduction Lévy-equivalent to P.

Proof Termination of the standardization follows immediately from the fact that, in the above definition, |P/v| ≤ |P | − 1, and we have immediately from the construction that P ≈_{L} v + P/v ≈_{L} … ≈_{L} ST (P).

We write P ≈_{ST A} Q if P ≈_{L} Q and both P and Q are standard. For any standard P, we define ⟨P ⟩_{S} = {Q | Q ≈_{ST A} P }. Further, we write Q ∈ ST V (P) if Q ∈ ST A and Q ≈_{L} P, where ST A denotes the set of all standard reductions, and call Q a standard variant of P. Note that Lemma 33 gives an algorithm of construction of a standard variant of any finite reduction P : t_{0}→^{u_{0}}t_{1}→^{u_{1}} … →^{u_{n−1}}t_{n} in an ASDRS. Indeed, the last step u_{n−1} of P is P -needed by Lemma 33.(1). If it is created by u_{n−2}, then the latter is P -needed too, by Lemma 33.(2). Otherwise, the ancestor redex of u_{n−1} in t_{n−2} is P -needed by Lemma 33.(3). Similarly, we can trace the ‘responsible’ redex of u_{n−1} in t_{0}, which is P -needed. Repeated contraction of P -needed redexes terminates, and yields a standard variant of P; the proof is similar to the proof of Theorem 35. The next proposition shows that, moreover, all standard variants of a finite reduction P in an ASDRS can be found effectively. (Since the length of any standard variant of P coincides with the number of P -needed steps in P, P has only a finite number of standard variants.)

Proposition 36 For any finite reduction P in an ASDRS, P -neededness of redexes in all terms of P is decidable. Consequently, any standard variant of P can be constructed efficiently (in particular, the standardization procedure of P is computable).

Proof Let P : t_{0}→^{u_{0}}t_{1}→^{u_{1}} … → t_{n}. P -(un)neededness of any redex in a term t_{i} can be established by induction on n = |P |, as follows. If n = 1, then only the contracted redex u_{0} is P -needed in t_{0} by Definition 32 and Lemma 33.(1). Let n > 1, and let P_{1} : t_{1}→^{u_{1}}t_{2}→^{u_{2}} … → t_{n}. We can assume to have found all the P -needed redexes in all t_{i} with i ≥ 1, since P -neededness in these terms coincides with P_{1}-neededness by Definition 32 (and |P_{1}| = n − 1). Then a redex in t_{0} different from u_{0} is P -needed iff it has such a residual in t_{1}, by Lemma 33.(3). If u_{0} does not create u_{1}, then they can be permuted. If u_{1} = u′_{1}/u_{0} and u′_{0} = u_{0}/u′_{1} = ∅, then u_{0} is P -unneeded by Definition 32; otherwise, if u′_{0} ≠ ∅, by the induction assumption, we can assume to know whether or not u′_{0} is needed w.r.t. P′ = u′_{0} + u_{2} + … + u_{n−1}, and u_{0} is P - needed iff u′_{0} is P′-needed. Finally, if u_{0} creates u_{1}, we can standardize P_{1}, or construct a standard variant P′_{1} of P_{1}; then if u_{0} still creates the first step of P′_{1} (which is P -needed by Definition 32), then u_{0} is P -needed by Lemma 33.(2); if not, then we arrive to a previously considered case, and the decidability of P -neededness follows. The rest is immediate from the discussion above.

Definition 37 Let P : t → → s in an ASDRS, and let v ∈ s. We call P v standard if so is P. We call P v canonical if it is standard and, for any Q ≈_{L} P, the last step in Q creates v.

Note that if P ≈_{ST A} P′, then P v is canonical iff so is P′v. So the canonical forms we speak of are actually objects ⟨P ⟩_{S}v, for standard finite reductions P. Our extraction algorithm, defined in Definition 39 below, transforms any redex with history into a canonical one, and the main result of this section is that redexes are zig-zag related iff they have the same canonical form.

The ‘syntactic’ extraction procedures in [51,4,62] (without the shift operation) can quickly be summarized as follows: First, given a P u, one must standardize P + u according to a left-to-right outside-in standardization procedure, and if P′ + u′ + P′′ is the standard variant of P + u, where u is a P′′-residual of u′, one starts the extraction procedure from P′u′. Now, if the last step, say w, of P′ does not create u′, then the contraction of w can be ‘omitted’ in P′. Otherwise there is a non-empty tail P′_{2} of P′, say P′ = P′_{1} + v + P′_{2}, that takes place either in a part disjoint from v or inside a descendant of an argument of v, and in both cases v does not contribute to the creation of u′, therefore is ‘omitted’ by the extraction step. Since redexes in DRSs do not have any structure (in particular, they are not partitioned into patterns and arguments), these ‘syntactic’ extraction algorithms (and corresponding correctness proofs) cannot be directly generalized to ASDRSs. The same is true for the extraction algorithm in [33]. Instead, our extraction algorithm (when applied to P u) checks every standard variant of P in order to find one whose last step does not create u and therefore can be omitted. The following lemma says that we can indeed restrict our search to standard reductions only:

Lemma 38 Let Q : t → →^{P} s→^{u}e, where u does not create v ∈ e. Then there is a standard Q′ ≈_{L} Q such that Q′ : t → →^{P′} s′→^{u′}e, where P′u′ ⊴_{z} P u and u′ does not create v.

Proof We show that ST (Q) can be taken for Q′. By Definition 34, ST (Q) is obtained from Q by a sequence of transformations Q = Q_{1}, Q_{2}, …, Q_{n} = ST (Q) such that Q_{i+1} is obtained from Q_{i} by permuting the first Q-needed step that has preceding Q-unneeded steps before those Q-unneeded steps (all Q_{i} are Lévy-equivalent). Since u is the last Q-needed step in Q by Lemma 33.(1), any Q_{i} with i < n has the form P_{i} + u such that P_{i} ≈_{L} P, and P_{n−1} has the form P_{n−1} : t → →^{P′} o → →^{P′′} s where P′ is Q-needed and P′′ is Q-unneeded. By Lemma 33.(2), P′′ cannot create u, i.e., there is u′ ∈ o such that u′/P′′ = u, and u′ is Q-needed by Lemma 33.(3) (see the diagram). Since P′′/u′ is Qunneeded by Lemma 33.(3), and since the last step of P′ + u′ + P′′/u′ is Q-needed by Lemma 33.(1), P′′/u′ = ∅. Since u′ is Q-needed and P′′ is Q-unneeded, P′′ is external to u′ by Lemma 33.(3). Hence, by the Stability Lemma, u′ does not create v, and the lemma follows since ST (Q) = P′ + u′ is standard by Theorem 35, and P′u′ ⊴_{z} P u since u = u′/P′′.

[figure: t; P′; o; P′′; s; u; e ∋ v; v ∈ e; u′; ∅; e ∋ v; u; ∅; e ∋ v; ∅]

It follows from Definition 37, Proposition 36 and Lemma 38 that it is decidable whether a redex with history P v is canonical, and if P v is not canonical, one can effectively find a reduction Q : t → →^{P′} e→^{u}s such that Q ∈ ST V (P) and u does not create v, say v = v′/u. In the search for a shortest reduction that creates a redex in the zig-zag class of P v, contraction of u in Q can be omitted – P′v′ ≃_{z} P v and |P′| < |P |, since all standard Lévy-equivalent reductions have the same (minimal) length. Obviously, reductions creating a redex in some family in the quickest way must be standard, since they are the shortest in their Lévy-equivalence classes. The transformation of P v into P′v′ is denoted by P v⇀^{u}P′v′, or just P v⇀P′v′. For example, consider the ASDRS corresponding to the TRS R = {f(x) → g(x), a → b, b → c}, let P : f(a) → g(a) → g(b), and let v = b in g(b). Then P v is not canonical, as P ≈_{ST A} Q : f(a) → f(b) → g(b) and the last step of Q does not create v – the latter is the residual of v′ = b in the final term of P′ : f(a) → f(b). Hence we can perform an extraction step P v⇀P′v′. The latter redex is in extraction normal form.

The formal definition of extraction is as follows:

Definition 39 (Extraction) Let Q : t → →^{P′} e→^{u}s be a standard variant of P, in an ASDRS, and let v ∈ s be a u-residual of v′ ∈ e. Then we write P v⇀^{u}P′v′, and call the transformation an extraction step. (Note that, since Q is standard, so is P′ by Definition 32.) ⇀ ⇀ is the transitive and reflexive closure of ⇀.

Since in the above definition |P′| < |Q| ≤ |P |, the relation ⇀ is trivially strongly normalizing, and in order to prove that it is confluent (modulo ≈_{ST A} on histories), it is enough to prove that it is weakly (or locally) confluent, that is, Qw′′↼^{v}Nw⇀^{u}P w′ implies Qw′′⇀^{u′}N^{∗}w^{∗}↼^{v′}P w′. This will be proved in Theorem 42. We need two lemmas first, which state particular cases of a general fact that causally unrelated steps (or rather families) can be contracted in any order.

Lemma 40 Let u + P ≈_{ST A} Q + u′, where u′ = u/Q and P = v + P′. Then u does not create v, and u can be contracted after v, i.e., u + v ≈_{L} v^{∗} + u^{∗}, where v = v^{∗}/u and u^{∗} = u/v^{∗}. Further, v^{∗}/Q = ∅ and u′ = u^{∗}/(Q/v^{∗}).

Proof Let Q′ = Q/u. Since u + P is standard, so is P by Definition 32, so v is P -needed, and since P ≈_{L} Q′, v is Q-needed too, i.e, Q′ contracts a residual v′ of v. Since Q′ contracts residuals of redexes contracted in Q, Q contracts a redex v′′ whose residual is v′. So we have the following picture:

[figure: ·; u; ·; v; ·; P′; ·]
[figure: ·; ·; v′; ·; ·]
[figure: ·; v′′; ·; v′; ·; ·]
[figure: Q; u′; Q′; ∅; ·; ·]

Now, since Q is external to u (since u has a Q-residual u′ and the DRS is nonduplicating), we have immediately by the Stability Lemma that both v and v′′ are residuals of some redex v^{∗} in the initial term. Hence u+v ≈_{L} v^{∗}+u^{∗}, where v = v^{∗}/u and u^{∗} = u/v^{∗}. Since Q contracts a residual v′′ of v^{∗}, v^{∗}/Q = ∅. Since Q is external to u, we have by Lemma 4 that Q^{∗} = Q/v^{∗} is external to u^{∗}. Since u is u + P -needed, so is u^{∗} by Lemma 33.(3). Hence u^{∗} is Q^{∗} + u′- needed. Since Q^{∗} is external to u^{∗} and Q^{∗} + u′ contracts a residual of u^{∗}, we have u′ = u^{∗}/Q^{∗}.

[figure: ·; v^{∗}; ·; u^{∗}; ·; P′; ·]

[figure: ·; Q; ∅; ·; Q^{∗}; u′; ·; ·]
[figure: ·; u′; ∅; ·; u′; ∅; ·; ∅; ·]

Lemma 41 Let P + u ≈_{ST A} Q + v and let u ≠ v. Then there are P′v′ and Q′u′ such that P′ + v′ ≈_{ST A} P, Q′ + u′ ≈_{ST A} Q, P′ ≈_{ST A} Q′, P′v′ ≃_{z} Qv and Q′u′ ≃_{z} P u, u = u′/v′ and v = v′/u′.

[figure: ·; P′; ·; v′; ·; u; ·]

[figure: ·; Q′; ∅; ·; ∅; v′; ·; ∅; u; ·; ∅]

[figure: ·; u′; ∅; ·; u′; v; ·; u; ∅; ·; ∅]

[figure: ·; v; ∅; ·; v; ∅; ·; ∅; ∅; ·; ∅]

Proof Since P + u ≈_{ST A} Q + v, we have v ≈_{L} (P + u)/Q. By Lemma 5, (P + u)/Q contracts a residual of v. Note that P ≈_{L} Q would imply u ≈_{L} v, implying by [weak acyclicity] that u = v. Thus P ≉_{L} Q. We show that P/Q ≠ ∅.

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

[figure: ·; Q; \begin{matrix}P/Q \\ v \end{matrix}; ·; Q/P; u; ∅; ·; ∅]

[figure: ·; v; ∅; ·; ∅; ·; ∅]

Suppose on the contrary that P/Q = ∅. Then, Q/P ≠ ∅ and by [weak acyclicity], v = u/(Q/P). But P + u ≈_{L} Q + v implies (Q/P)/u = ∅. Since Q + v is standard, the first (and any other) step of Q whose residual, say w, is contracted in Q/P is u-needed by Lemma 33.(3). Hence w/u = ∅ implies u = w, and therefore Q/P = u and u/(Q/P) = ∅, contrary to v = u/(Q/P). So P/Q ≠ ∅. Since P is P + u-needed (recall that P + u is standard), so is P/Q, i.e., P/Q is v-needed. Hence, by [weak acyclicity], the first (and the only) step of P/Q coincides with v, i.e., P/Q = v. Thus P contracts a redex v′′ whose residual is v. So if P = P_{1} + v′′ + P_{2}, then (Q + v)/P_{1} = Q/P_{1} + v, and we have v′′ + P_{2} + u ≈_{ST A} Q/P_{1} + v and v′′ + P_{2} ≉_{L} Q/P_{1} (see the figure).

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

[figure: ·; Q; ∅; ·; v; ·; ∅; ·; ∅; ·; ∅]
[figure: ·; v; ∅; ·; v; ∅; ·; ∅; ∅; ·; ∅; ∅; ·; ∅]

Now, by repeated application of Lemma 40, v′′ + P_{2} + u can be transformed into a reduction P′_{2} + v′ + u such that v′′ + P_{2} ≈_{ST A} P′_{2} + v′, v′ = v′′/P′_{2}, and v = v′/(Q/(P_{1} + P′_{2})).

[figure: ·; P_{1}; ·; P′_{2}; ·; v′; ·; u; ·]

[figure: ·; Q; ∅; ·; ∅; ·; v; ·; ∅; ·; ∅]
[figure: ·; v; ∅; ·; v; ∅; ·; v; ∅; ·; ∅; ·; ∅]

Hence, if we take P′ = P_{1} + P′_{2}, we have that P′ + v′ ≈_{ST A} P and P′v′ ⊴_{z} Qv. Existence of Q′u′ such that Q′ + u′ ≈_{ST A} Q and Q′u′ ⊴_{z} P u can be shown similarly. Since P_{2}/(Q/(P_{1} + v′′)) = ∅, we have again by repeated application of Lemma 40 that P′/Q ≈_{L} P′/(Q′ + u′) ≈_{L} (P′/Q′)/u′ = ∅. But P′/Q′ is external to u′ since u′ has a P/Q′ ≈_{L} P′/Q′ + v′/(Q′/P′)-residual (by Q′u′ ⊴_{z} P u).

[figure: ·; P′; ·; v′; ·; u; ·]

[figure: ·; Q′; ∅; ·; ∅; v′; ·; ∅; u; ·; ∅]

[figure: ·; u′; ∅; ·; u′; v; ·; u; ∅; ·; ∅]

[figure: ·; v; ∅; ·; v; ∅; ·; ∅; ∅; ·; ∅]

Hence we have by Lemma 5 and Lemma 33.(3) that P′/Q′ = ∅ (as otherwise P′/Q′ should have a non-empty u′-residual by Lemma 33.(3)). The converse is proved similarly, so P′ ≈_{L} Q′. It follows that u = u′/v′ and v = v′/u′.

Theorem 42 (Extraction) Every redex P v in an ASDRS has exactly one extraction normal form ⟨P^{∗}⟩_{S}v^{∗} which is canonical, and P^{∗}v^{∗} ⊴_{z} P v.

Proof It is enough to show that the extraction relation ⇀ is weakly confluent (as it is strongly normalizing). So let Qw′′↼^{v}Nw⇀^{u}P w′ with u ≠ v (since if u = v then there is nothing to prove). We will show that Qw′′⇀^{u′}N^{∗}w^{∗}↼^{v′}P w′ for some N^{∗}w^{∗}, u′, and v′ such that u = u′/v′ and v = v′/u′. By Definition 39,

we have from Qw′′↼^{v}Nw⇀^{u}P w′ that Q + v ≈_{ST A} N′ ≈_{ST A} P + u, where N′

is a standard variant of N, and w′′/v = w′/u = w. By Lemma 41, we have the following situation, where P′ + v′ ≈_{ST A} P, Q′ + u′ ≈_{ST A} Q, P′ ≈_{ST A} Q′, u = u′/v′, and v = v′/u′ (hence P′v′ ≃_{z} Qv, Q′u′ ≃_{z} P u).

[figure: ·; P′; ·; v′; ·; u; ·]

[figure: ·; Q′; ∅; ·; ∅; v′; · ∋ w′; ∅; u; ·; ∅]

[figure: ·; u′; ∅; · ∋ w′′; u′; v; · ∋ w; u; ∅; ·; ∅]

[figure: ·; v; ∅; ·; v; ∅; ·; ∅; ∅; ·; ∅]

Now, by [stability], there is a redex w^{∗} in the final term of P′ (and Q′) such that

w^{∗}/v′ = w′ and w^{∗}/u′ = w′′. Thus, for N^{∗} = P′, we have Qw′′⇀^{u′}N^{∗}w^{∗}↼^{v′}P w′

by Definition 39.

The extraction normal form ⟨P^{∗}⟩_{S}v^{∗} of P v is called a canonical form of P v, and so are all P′v′ ∈ ⟨P^{∗}⟩_{S}v^{∗}. Now we can prove the adequacy of our extraction procedure for the zig-zag.

Theorem 43 In an ASDRS, P u ≃_{z} Qv iff they have the same unique canonical form ⟨N⟩_{S}w.

Proof

(⇒) By definition of ≃_{z}, there are P_{0}u_{0} = P u, P_{1}u_{1}, …, P_{n}u_{n} = Qv such that P_{0}u_{0} ⊵_{z} P_{1}u_{1} ⊴_{z} P_{2}u_{2} ⊵_{z} … P_{n}u_{n}. By the Standardization Theorem, we can take P_{i} to be standard.

P_{0}u_{0}
[figure]
[figure: P_{1}u_{1}; Q_{1}; P_{2}u_{2}]

[figure][figure]

[figure: P_{3}u_{3}]
[figure]
[figure: ·; P_{n}u_{n}]

Since P_{0}u_{0} ⊵_{z} P_{1}u_{1}, there is Q_{1} such that P_{0} ≈_{L} P_{1} + Q_{1} and u_{0} = u_{1}/Q_{1}. Let P′_{1}u′_{1} be a canonical form of P_{1}u_{1}: P_{1}u_{1} ⇀ ⇀ P′_{1}u′_{1}. Then there is P_{1}^{∗} such that P_{1} ≈_{ST A} P′_{1} + P_{1}^{∗}. We show that P′_{1} is P′_{1} + P_{1}^{∗} + Q_{1}-needed, i.e., P_{0}-needed (since P′_{1} + P_{1}^{∗} + Q_{1} ≈_{L} P_{0}). Suppose on the contrary that P′_{1} contracts a P_{0}-unneeded redex. Let w be the latest P_{0}-unneeded step in P′_{1}. By Lemma 33.(2), w does not create the next step in P′_{1} (if w is not the last step in P′_{1}), therefore it can be permuted with its next step. That w-step is again P′_{1}-unneeded by Lemma 33.(3), and can be contracted after its next step, and so on. So we can assume that w is the last step in P′_{1} (P′_{1} is chosen up to ≈_{ST A}). Thus there is N ≈_{L} w + P_{1}^{∗} + Q_{1} that is external to w, and w/N = ∅. Since P′_{1}u′_{1} is canonical, w creates u′_{1}. Hence, by the Stability Lemma, ∅ = u′_{1}/(N/w) = u′_{1}/(P_{1}^{∗} + Q_{1}) = u_{1} – a contradiction. Thus P′_{1} is P_{0}-needed. This implies that the standardization procedure of Definition 34 does not effect P′_{1} when applied to P′_{1} + P_{1}^{∗} + Q_{1}, i.e., we can assume a standard P′_{0} ≈_{ST A} P_{0} such that P′_{0} = P′_{1} +P′′_{0} for some P′′_{0}, and u_{0} = u′_{1}/P′′_{0}. Hence P_{0}u_{0} ⇀ ⇀ P′_{1}u′_{1} by the definition of ⇀, and P′_{1}u′_{1} is a canonical form of both P_{0}u_{0} and P_{1}u_{1}. Similarly, since P_{1}u_{1} ⊴_{z} P_{2}u_{2}, we have that P′_{1}u′_{1} is a canonical form of P_{2}u_{2}, and so on. Now it is enough to apply Theorem 42.

(⇐) Immediate from Theorem 42 and the definition of ≃_{z}.

This theorem, together with computability of extraction normal forms, implies decidability of the zig-zag relation in ASDRSs. Note that, at this stage, we do not yet know whether or not zig-zag is a family relation. This is the subject of the next section.

6 Affine Zig-Zag and Separable Families

In this section we show that, in ASDRSs, the zig-zag relation forms a family relation, that is, it satisfies the family axioms of DFSs. We will also define separability of a family relation, and show that zig-zag is the only separable family relation in ASDRSs.

Definition 44 (1) We call a DFS F a zig-zag DFS, ZDFS, if its family

relation is the zig-zag ≃_{z}.

(2) We call an affine DFS separable, SDFS, if, for any redex P v, v cannot create two different redexes in the same family, that is, if v creates w′, w′′ and w′ ≠ w′′, then F am((P + v)w′) ≠ F am((P + v)w′′). In a separable DFS, the family and contribution relations will be denoted by ≃_{s} and ↪_{s}. The DFS is non-separable otherwise.

It is easy to see that not all (even linear, i.e., without duplication and erasure) DFSs are zig-zag DFSs or separable DFSs. For example, in the linear SDRS given by the reduction graph

·
[figure: v_{1}; v′_{2}]
· \overline{u_{}}·  ·
[figure: v_{2}; v′_{1}]
·

where u creates v_{1} and v_{2}, v′_{1} = v_{1}/v_{2} and v′_{2} = v_{2}/v_{1}, we can set all vs to belong to the same family ϕ, and u to form its own family ψ, and define ψ ↪ ϕ. Then we get a DFS which is not a ZDFS as for example uv_{1} ≄_{z} uv_{2}. That DFS is not separable either, as u creates two different members of the family ϕ. We will show below that this is not a coincidence. We could also define {v_{1}, v′_{1}} and {v_{2}, v′_{2}} to form separate families ϕ_{1} and ϕ_{2}, and define ψ ↪ ϕ_{1}, ϕ_{2}, and this would yield a ZDFS.

As already mentioned in the introduction, non-separable families (not using that name) for Interaction Systems are studied in [4], where it is demonstrated that such a family relation is in general strictly larger than the zig-zag. Indeed, consider the following example from [4]. Let an Interaction System be given by the μ-rule: μ-rule μ(λx.X) → [μ(λx.X)/x]X. Then the μ-reduction step t = μ(λx.(xx)) → (μ(λx.(xx)) μ(λx.(xx))) = s simultaneously creates the two μredexes in s; these redexes are intuitively in the same family (and this intuition is supported by an appropriate labelling system for Interaction Systems), but cannot be related by zig-zag (without taking into account the structure of rewrite steps, which is impossible to do for DRS steps as they do not carry any internal structure).

Another important example where a non-separable sharing is reasonable is the lazy call-by-value λ-calculus, λ_{LV} [64], which is obtained from the λ-calculus by allowing only β-redexes whose arguments are values (i.e, variables or abstractions λx.t), and that are not in the scope of λ-occurrences (we assume that there are no δ-rules in the calculus). it is easy to see that λ_{LV} is linear: if u, v are redexes in a term t and u = (λx.e)o, then v ∉ e because of the main λ of u, and v ∉ o since o is either a variable or an abstraction; orthogonality of λ_{LV} (i.e., that the residuals of redexes remain admissible) follows from a similar argument. Now consider the reduction

t = w = (λx.(xy)(xy))λx.u→^{w}o = \overbrace{((λx.u)y)}^{v_{1}} \overbrace{((λx.u)y)}^{v_{2}} → → uu = s,

where u is a λ_{LV} -redex such that x does not occur free in it. Note that the two occurrences of u in s are redexes created by v_{1} and v_{2}, as the occurrences of u in t and o are not λ_{LV} -redexes (they are not admissible). It is reasonable to share the occurrences of u in s, but in order to make the reduction graph of t a DFS (in particular, for the [contribution] axiom to be satisfied), we need to share v_{1} and v_{2} as well, although the two are not related.^{4} This goes beyond Lévy’s concept of sharing, and the resulting DFS is not separable as the contraction of w creates two different redexes, v_{1} and v_{2}, of the same family.

4 The redexes v_{1} and v_{2} get different labels in Levy’s labelling system for the λcalculus, and cannot be related either by zig-zag or by extraction.

Below, F AM_{z}(P) denotes the set of zig-zag classes whose member redexes are contracted in P, in an ASDRS; and F am_{z}(Qu) denotes the zig-zag class of Qu. Further, if ϕ′, ϕ are zig-zag classes, we write ϕ′ ↪_{z} ϕ iff for any P u ∈ ϕ, P contracts a redex in ϕ′.

Lemma 45 If P v ≃_{z} Qw, then v/(Q/P) = w/(P/Q). In particular, where P ≈_{ST A} Q, it follows that v = w.

Proof By Theorem 43, Q ≈_{L} N + Q′, P ≈_{L} N + P′, w = u/Q′ and v = u/P′, where Nu is a canonical form of Qw and P v. Then P/Q ≈_{L} P′/Q′ and Q/P ≈_{L} Q′/P′. Hence w/(P/Q) = w/(P′/Q′) = u/(Q′ ⊔ P′) = u/(P′ ⊔ Q′) = v/(Q′/P′) = v/(Q/P).

Corollary 46 Any reduction in an ASDRS R can contract at most one element of a zig-zag class.

Proof Let P : t_{0}→^{u_{0}}t_{1}→^{u_{1}} … be a reduction in R, and let P_{i} : t_{0} → → t_{i} be its initial part. If on the contrary P_{i}u_{i} ≃_{z} P_{k}u_{k} for some i < k, then we must have by Lemma 45 that u_{i}/(u_{i} + … + u_{k−1}) = u_{k} – a contradiction.

As a consequence, we get that ≃_{z} satisfies [FFD] in any ASDRS. To show that ≃_{z} satisfies [creation] too, we need a few lemmas.

Lemma 47 Let P be Q-needed, in an ASDRS. Then F AM_{z}(P) ⊆ F AM_{z}(Q). In particular, if P ∈ ST V (Q), then F AM_{z}(P) ⊆ F AM_{z}(Q), and if P ≈_{ST A} Q, then F AM_{z}(P) = F AM_{z}(Q).

Proof Let v be a contracted redex in P, say P = P′ + v + P′′. Then v is Q/P′-needed. Hence F am_{z}(P′v) ∈ F AM_{z}(Q/P′) ⊆ F AM_{z}(Q), implying the lemma.

Lemma 48 Let Q^{∗} : t → →^{P} s→^{u}e where u creates v ∈ e. Then, for any canonical form Q′v′ of Q^{∗}v, Q′ contracts a redex zig-zag related to P u.

Proof We have by Lemma 38 that Q = ST (Q^{∗}) = P′+u′, where P ≈_{L} P′+P′′ (for some Q-unneeded P′′) and u = u′/P′′. If Qv is not a canonical form, by Lemma 38 there is an extraction step Qv⇀^{w_{1}}Q_{1}v_{1} (i.e., Q ≈_{ST A} Q_{1} + w_{1} and v = v_{1}/w_{1}). Since Q_{1} + w_{1} ≈_{ST A} Q = P′ + u′, we have by Lemma 41 that Q_{1} ≈_{ST A} P_{1} + u_{1} such that P_{1}u_{1} ≃_{z} P′u′ ≃_{z} P u. So we have (P′ + u′)v⇀^{w_{1}}(P_{1} + u_{1})v_{1} such that P_{1}u_{1} ≃_{z} P′u′. Similarly, if (P_{1} + u_{1})v_{1} is not a canonical form, there is an extraction step (P_{1} + u_{1})v_{1}⇀^{w_{2}}(P_{2} + u_{2})v_{2} such that P_{2}u_{2} ≃_{z} P_{1}u_{1} ≃_{z} P′u′ ≃_{z} P u, and so on. So a canonical form of Qv has the form (P_{m} + u_{m})v_{m} such that P u ≃_{z} P_{m}u_{m}. Since, by Theorem 42, for any canonical form Q′v′ of Qv (and hence of Q^{∗}v), Q′ ≈_{ST A} P_{m} +u_{m} and v_{m} = v′, it follows by Lemma 47 that Q′ contracts a redex in the family of P u.

Lemma 49 Let P v⇀^{w}P′v′. Then F AM_{z}(P′) ⊆ F AM_{z}(P).

Proof By Definition 39, P v⇀^{w}P′v′ implies that P′ + w ∈ ST V (P), and by Lemma 47, F AM_{z}(P′) ⊆ F AM_{z}(P′ + w) ⊆ F AM_{z}(P).

The next lemma implies that ≃_{z} satisfies [creation], in any ASDRS.

Lemma 50 Let Q : e → →^{P} t→^{u}s where u creates v ∈ s. Then F am_{z}(P u) ↪_{z} F am_{z}(Qv).

Proof By Lemma 48, if Q′v′ is a canonical form of Qv, then F am_{z}(P u) ∈ F AM_{z}(Q′). Now it follows from Lemmas 47 and 49 and Theorem 43 that for any Q^{∗}v^{∗} ≃_{z} Qv, F am_{z}(P u) ∈ F AM_{z}(Q^{∗}), i.e., F am_{z}(P u) ↪_{z} F am_{z}(Qv).

Theorem 51 Let R be a non-duplicating SDRS. Then F_{R} = (R, ≃_{z}, ↪_{z}) is a non-duplicating zig-zag DFS.

Proof We need to show that F_{R} satisfies all family axioms. [contribution] is immediate by the definition of ↪_{z}. Since for any u, v ∈ t, ∅_{t}u and ∅_{t}v are canonical forms, u ≠ v implies by Theorem 43 that ∅_{t}u ≄_{z} ∅_{t}v, i.e., [initial] holds. [creation] is immediate from Lemma 50, and [FFD] from Corollary 46.

Next we show that an affine DFS is a zig-zag DFS iff it is separable. First we establish a characterization of separability of a DFS F via uniqueness of contracted families in reductions in F. It shows that, in separable DFSs, and only in such DFSs, there is no sharing (in the affine case) – all reductions are in fact complete family-reductions.

Lemma 52 Let F = (R, ≃, ↪) be an affine DFS. Then the following are equivalent:

(1) F is separable;

(2) Elements of any family are contracted at most once in any reduction in F;

(3) P v ≃ P v′ implies v = v′;

(4) Any reduction in F is in fact a complete family-reduction, and vice versa.

Proof

(1) ⇒ (2): Let P : t_{0} → →^{P_{i}} t_{i}→^{u_{i}}t_{i+1} → → t_{n}, and let us prove that k < m implies that P_{k}u_{k} ≄ P_{m}u_{m} by induction on the number of families contributing to F am(P_{k}u_{k}). Suppose on the contrary that ϕ = F am(P_{k}u_{k}) = F am(P_{m}u_{m}). Let P′_{k}u′_{k} be a canonical form of P_{k}u_{k}, which exists by Theorem 42. Hence there is Q′_{k} such that P′_{k} + Q′_{k} ≈_{L} P_{k}, and u_{k} = u′_{k}/Q′_{k}. So we have that P_{k+1} = P_{k} + u_{k} ≈_{L} P′_{k} + Q′_{k} + u_{k} ≈_{L} P′_{k} + u′_{k} + Q′_{k}/u′_{k} (see the figure below). Since by [contribution] P′_{k} contracts redexes in all contributor families of F am(P′_{k}u′_{k}) = ϕ, and since by the induction assumption no redexes in these families can be contracted again, u_{m} is not created by its preceding step in u′_{k} + Q′_{k}/u′_{k} + u_{k+1} + … + u_{m−1}, by [creation]. Similarly, its ancestor redex is not a created redex, and so on. That is, u_{m} is a residual of some redex u′_{m} in the final term of P′_{k}, different from u′_{k}. Hence F am(P′_{k}u′_{k}) = ϕ = F am(P′_{k}u′_{m}). Since P′_{k}u′_{k} is in extraction normal form, the last step of P′_{k}, denote it by P′′_{k}u′′_{k}, creates u′_{k}. Hence ψ = F am(P′′_{k}u′′_{k}) ↪ ϕ by [creation]. Since by the induction assumption P′′_{k} does not contract redexes of the same family more than once, and by [contribution] the history of any member of ϕ must contract a redex in ψ, u′′_{k} must create u′_{m} too, contradicting separability.

[figure: ·; P′_{k}; ·; Q′_{k}; ·; ·; u′_{k}; Q′_{k}/u′_{k}; ·; u_{k}; u_{k+1}; ·; ·; u_{m−1}; ·]

(2) ⇒ (3): If there were P v ≃ P v′ with v ≠ v′, then at least one of P + v + v′/v, P + v′ + v/v′ would contract two members of F am(P v) by [weak acyclicity], contradicting (2).

(3) ⇒ (4): Immediate.

(4) ⇒ (1): If F was not separable, then there would be P v, w′ and w′′ such that v creates both w′ and w′′, w′ ≠ w′′, and F am((P + v)w′) = F am((P + v)w′′). By the assumption (4), the reduction P + v is also a complete family-reduction, implying that P + v + w′∥w′′, where w′∥w′′ is the multi-step contracting w′ and w′′ in parallel, is a complete family-reduction which is not a reduction, contradicting (4).

Lemma 53 Let P v be a canonical element of a family ϕ, in an affine DFS F = (R, ≃, ↪), and let P contract a redex w. Then F am(w) ↪ ϕ.

Proof Suppose on the contrary that ψ = F am(w) ↛ ϕ, and assume that P v and w are such that w is (one of) the latest among steps in canonical elements of ϕ that do not contribute to ϕ. Since P v is canonical, w cannot be the last step of P as the last step of P creates v by Definition 37, and therefore its family contributes to ϕ by [creation]. Further, if v is the next to w step in P, then w cannot create v as this would imply ψ ↪ F am(v) by [creation], implying ψ ↪ ϕ (as F am(v) ↪ ϕ by the choice of w). Hence w can be permuted with v in P, yielding again (by Lemma 33) a canonical element of ϕ in which a step whose family does not contribute to ϕ is contracted later than w in P – a contradiction.

Lemma 54 Let P and Q be standard co-initial finite reductions such that F AM_{z}(P) = F AM_{z}(Q). Then P ≈_{L} Q.

Proof Suppose on the contrary that P ≉_{L} Q, and say P/Q ≠ ∅. Then P contracts a redex u, say P = P′ + u + P′′, such that u/(Q/P′) ≠ ∅. Let v be a step in Q, i.e., Q = Q′ + v + Q′′ (see the figure). Then if u′ = u/(Q′/P′) and v′ = v/(P′/Q′), we have u′ ≠ v′, thus (P′ ⊔ Q′)u′ ≠ (P′ ⊔ Q′)v′. Hence, by Lemma 45, F am_{z}(P′u) = F am_{z}((P′ ⊔ Q′)u′) ≠ F am_{z}((P′ ⊔ Q′)v′) = F am_{z}(Q′v), i.e., F AM_{z}(P) ∋ F am_{z}(P′u) ∉ F AM_{z}(Q) – contradiction.

[figure: P′; u; P′′]

[figure: Q′; u′; ∅]
[figure: v; v′; ∅; ∅; ∅]

[figure: Q′′; ∅; ∅; ∅; ∅]

Theorem 55 An affine DFS F is separable iff it is a zig-zag DFS.

Proof

(⇒) Let F = (R, ≃_{s}, ↪_{s}) be separable, and suppose on the contrary that ≃_{s}≠≃_{z}. Then, by ≃_{z}⊆≃_{s}, there is a ≃_{s}-family ϕ which contains at least two zig-zag classes ϕ′ and ϕ′′, and we can assume that ϕ has a minimal number of ↪_{s}-contributor ≃_{s}-families ϕ_{1}, …, ϕ_{n}. By the minimality of ϕ, ϕ_{1}, …, ϕ_{n} are also ≃_{z}-families. Let P′v′ and P′′v′′ be canonical elements of ϕ′ and ϕ′′. By Lemma 53 and [contribution], P′ and P′′ both contract exactly the elements of (all) families ϕ_{1}, …, ϕ_{n}, thus F AM_{z}(P′) = F AM_{z}(P′′), implying by Lemma 54 that P′ ≈_{ST A} P′′. Hence the last step of P′ creates two different members P′v′ and P′v′′ of a ≃_{s}-family ϕ – a contradiction.

(⇐) Immediate from Lemma 52 and Corollary 46.

We conclude this section by a useful characterization of histories of canonical elements of zig-zag (hence extraction and separable) families, in ASDRSs. In particular, it implies that the history of a canonical redex is indeed a shortest reduction creating a member of the corresponding family.

Theorem 56 Let P v be a canonical element of a family ϕ, in an AZDFS F_{R} = (R, ≃_{z}, ↪_{z}). Then P contracts exactly one redex in every contributor family of ϕ.

Proof By Lemma 53 and [contribution], P contracts exactly redexes in (all) contributor families of ϕ. The uniqueness of contracted families follows from Lemma 52 and Theorem 55.

7 Implementation DFSs

We now define the implementation F_{I} of a DFS F, whose reduction steps correspond to complete family-reductions in F, hence the name. We also show that optimal reductions in F, relative to any stable set S of results, are implemented in F_{I} by the shortest S_{I}-normalizing reductions, where S_{I} is the set of terms in F_{I} corresponding to terms in S. We will assume that the reduction graph of F is the reduction graph of an initial term, denoted by t_{∅}, and that families are considered relative to t_{∅}, i.e, all histories start with t_{∅}.

Definition 57 Let F = (R, ≃, ↪) be a DFS where R = (A, /) and A = (T er, Red, →). Then the implementation or Lévy-implementation of F is the AZDFS F_{I} = (R_{I}, ≃_{I}, ↪_{I}), where

• the branches of the reduction graph of the underlying ARS A_{I} of R_{I} = (A_{I}, /_{I}) are complete family-reductions starting from t_{∅}, each edge (i.e., reduction step) being a multi-step contracting a family of redexes.

• the residual relation /_{I} is defined as follows: let U and V be complete sets of redexes in two ≃-families, in a term s, and let U : s →_{I} o be the multi-step contracting U. Then V/_{I}U is the multi-step o →_{I} e contracting all members of the set V/U.

• the family and contribution relations ≃_{I}, ↪_{I} in F_{I} are those induced by ≃ and ↪: let P_{I} and Q_{I} be reductions in R_{I} corresponding to complete familyreductions P and Q in F; then P_{I}U ≃_{I} Q_{I}V iff for any u ∈ U, v ∈ V, P u ≃ Qv; and F am(P_{I}U) ↪_{I} F am(Q_{I}V) iff F am(P u) ↪ F am(Qv).

We need to verify that F_{I} in the above definition is indeed an AZDFS.

Lemma 58 Let P : t_{∅} → → s be a complete family-reduction in a DFS F = (R, ≃, ↪), let U, V ⊆ s be complete sets of redexes of families ϕ and ψ in s, respectively, and let s → →^{V} o. Then U′ = U/V is the complete set of redexes of ϕ in o.

Proof Since ≃_{z}⊆≃, U′ consists of redexes of ϕ. Suppose on the contrary that there is w ∈ o such that (P + V)w ∈ ϕ and w ∉ U′. Again by ≃_{z}⊆≃, w must be created along V, and we have by [creation] that ψ ↪ ϕ. But this implies by [contribution] that P contracts a member of ψ, and therefore the complete family ψ (since P is a complete family-reduction), and P + V contracts the family ψ twice, contradicting Lemma 30.

Thus the residual relation is well defined. Obviously, V/_{I}V = ∅, and every family in o has at most one ancestor family in s. Further, [weak acyclicity] and [stability] for F_{I} follow immediately from the Weak Acyclicity Lemma and the Stability Lemma, respectively (one just needs to take for the reductions P and Q in these lemmas complete developments of disjoint sets of redexes, which are clearly external). The axiom [initial] in F_{I} follows immediately from [initial] in F. If P +U +V is a reduction in F_{I} such that U creates V, then the redexes in V are created along U (when P +U +V is considered as a reduction in F), i.e., F am(U) ↪ F am(V) in F, hence F am(U) ↪_{I} F am(V), implying [creation] in F_{I}. Since complete family-reductions can be viewed as reductions in F (by considering multi-steps as corresponding complete developments), [contribution] for ↪_{I} follows immediately from [contribution] for ↪. Finally,

[FFD] for F_{I} follows immediately from Lemma 30 for F. Hence F_{I} is indeed a DFS as ≃_{I} clearly contains the zig-zag relation. Note that F_{I} is separable as its steps contract entire ≃-families, hence it is an AZDFS by Theorem 55:

Theorem 59 For any DFS F, F_{I} is an AZDFS.

Next we show that any sharing ≃ in an SDRS stronger than zig-zag can be decomposed into any weaker sharing ≃′ and a non-separable sharing ≃^{∗} in the implementation of ≃′.

Definition 60 Let F = (R, ≃) and F′ = (R, ≃′) be DFSs. We say that F has a stronger sharing than F′, written F ≥ F′, if ≃′⊆≃.

Theorem 61 Let F = (R, ≃) and F′ = (R, ≃′) be DFSs. Then F > F′ iff there is a non-separable family relation ≃^{∗} on the implementation DRS R′_{I} of F′ such that F_{I}^{∗} = F_{I}, where F^{∗} = (R′_{I}, ≃^{∗}).

Proof

(⇒) Let F > F′. Define ≃^{∗} on R′_{I} by: P v ≃^{∗} Qu iff P′v′ ≃ Q′u′, where P′ and Q′ are reductions in R corresponding to P and Q, and v′ and u′ are Rredexes in redex-sets contracted in multi-steps v and u. It is immediate that the definition is correct (since reductions in F corresponding to a reduction in R′_{I} are all sequentializations of a multi-step reduction and are Lévyequivalent, and since F > F′). Further, the family axioms for ≃^{∗} follow from those of F exactly as they were verified above for F_{I} in the place of F^{∗} (the only difference is that F^{∗} is a ‘partial implementation’ of F while F_{I} is the ‘complete’ or Lévy-implementation). By the definition of ≃^{∗}, complete family-reductions in F^{∗} are exactly complete family-reductions in F, and F_{I}^{∗} = F_{I} follows since both are AZDFSs by Theorem 59. Since F > F′ and F′_{I} is an AZDFS, ≃^{∗} is strictly larger than zig-zag, hence is non-separable by Theorem 55.

(⇐) Immediate from Definition 60.

Thus, in particular, the study of a sharing in an SDRS strictly larger than the zig-zag can be reduced to studying zig-zag (when it is a family-relation) and studying non-separable affine families.

The following lemmas relate neededness in a DFSs with neededness in its implementation. Together with Theorem 31, they imply that the implementation DRSs F_{I} do indeed correctly implement complete family-reductions in DFSs F: If S_{I} is the set of terms in F_{I} corresponding to terms in a stable set S in F, then S_{I} is stable and S_{I}-needed reductions in F_{I} are actually S_{I}-needed complete family-reductions by Lemma 52.(4) and Theorem 59. Hence S_{I}-needed reductions are optimal w.r.t. S_{I} and implement optimal family-reductions in F, w.r.t S.

Lemma 62 Let S be a stable set of terms in a DFS F, and let S_{I} = S ∩ T er(F_{I}), where T er(F_{I}) is the set of terms in F. Then S_{I} is stable in F_{I}.

Proof Let t→^{u}_{I}s in F_{I}, where t ∉ S_{I} and s ∈ S_{I}. Then t → →^{U} s, where t ∉ S and s ∈ S. By closure of S under unneeded expansion, any sequentialization of t → →^{U} s must contract at least one S-needed redex, thus by Lemma 8, U ⊆ t must contain at least one S-needed redex. Hence there is no S-normalizing reduction in F external to U, thus there is no S_{I}-normalizing reduction in F_{I} external to u, i.e., u is S_{I}-needed. Closure of S_{I} under reduction follows from that for S, and we are done.

Lemma 63 Let S be a stable set of terms in a DFS F not containing the initial term t_{0} = t_{∅}, let P : t_{0} → →^{U_{0}} t_{1} → →^{U_{1}} … → → t_{n} be an S-normalizing complete family-reduction in F, and let P_{I} : t_{0}→^{u_{0}}_{I}t_{1}→^{u_{1}}_{I} … →_{I} t_{n} be its corresponding reduction in F_{I}. Then P is S-needed iff P_{I} is S_{I}-needed.

Proof

(⇒) Assume that P be S-needed, and suppose on the contrary that P_{I} is not S_{I}-needed, i.e., u_{i} is S_{I}-unneeded for some i. Then there is an S_{I}- normalizing reduction N : t_{i} → → _{I}s in F_{I} that is external to u_{i}. It remains to show that any corresponding complete family-reduction N′ in F (no matter how the multi-steps are sequentialized) is external to U_{i}: the latter implies that U_{i} does not contain an S-needed redex, contradicting S-neededness of P. If on the contrary a multi-step W of N′ contracts a residual of a redex in U_{i}, then it follows from Lemma 58 that W is the residual of U_{i} along N′ (as both U_{i} and W are complete sets of redexes of the same family in corresponding terms), implying that the corresponding step of N is a residual of u_{i} – a contradiction.

(⇐) Let P_{I} be S_{I}-needed. Suppose on the contrary that U_{i} is not S-needed for some i. Let Q be an S-needed S-normalizing complete family-reduction (which exists by Corollary 29). Note that the residual of U_{i} in any term along Q forms a complete family by Lemma 58, and all residuals of redexes in U_{i} remain S-unneeded by Lemma 8. Thus residuals of U_{i} along Q are redexsets disjoint from the contracted redex-sets, implying that the corresponding reduction of Q in F_{I} is external to u_{i}, which contradicts S_{I}-neededness of u_{i}.

Corollary 64 (Optimal Implementation) Let S be a stable set of terms in a DFS F and S_{I} be its corresponding stable set of terms in F_{I}. Then S_{I}-needed S_{I}-normalizing reductions in F_{I} are S_{I}-optimal in F_{I}, and they implement Soptimal complete family-reductions in F.

8 Conclusions and future work

We have introduced Deterministic Residual and family Structures and have proven two abstract versions of the RN theorem: one in stable DRSs for regular stable sets S, 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 [18,22], which is covered by our second RN theorem. It is remarkable that, unlike the proofs in [16,29,10], our first proof does not use the notion of standard reduction. Similar proofs for orthogonal CRSs in [32] and for orthogonal DAGs in [52,53] use an even stronger termination argument, expressed by the [FFD] 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 earlier by Lévy in [50,51]. It would be interesting to investigate whether it is possible to prove our second theorem in the context of stable DRS, without invoking family axioms, but possibly using some much weaker axioms.

Further, we have introduced and studied an abstract concept of optimal implementation of DFSs, and showed that needed computations (w.r.t. stable sets of results) in implementation DRSs mimic optimal (in the sense of Lévy and beyond) computations in original DFSs. We have shown that every affine SDRS can be turned into an affine DFS by taking zig-zag as the family relation, and that zig-zag is the only family relation with the separability property – no redex can create two different members of the same family simultaneously. Finally, we have shown that sharing is compositional. In particular, any family relation can be decomposed into zig-zag (when it is a family relation) and a non-separable affine family-relation, which facilitates the study of complicated (non-separable) concepts of sharing in duplicating systems (such as the one in [4]). As for zig-zag in duplicating SDRSs, we believe that suitable extensions of SDRSs can be defined, in which one can extend our construction of zig-zag DFSs to the general (duplicating) case, and our proofs can be used as a basis. In the general case, the [FFD] axiom of DFSs becomes a strong requirement, and extra axioms will be necessary to ensure it. We expect that a modification of our extraction algorithm will be applicable.

Besides their clear relevance for the study of syntactic properties of orthogonal rewrite systems (which we hope to have amply demonstrated), DFSs have already proven their usefulness also in the study of concurrent semantics of orthogonal rewrite systems: Indeed, based on the results obtained in this paper, we have defined in [44] a fully adequate Prime Event Structure [70,58,71] style semantics for orthogonal rewrite systems in a uniform fashion. Furthermore in [42,43] we studied the concepts of independence and interaction of (sub)computations in the framework of DFSs, yielding a nice theory of Euclidian Geometry for reduction spaces in orthogonal rewrite systems. And we have also developed a relativized stable computational semantics for orthogonal reduction systems [38], extending the computational semantics of rewrite systems proposed by Boudol [13]. Among many possible directions for future work, let us mention that it is important to extend these results, both the syntactic and semantic aspects, to non-deterministic systems, enabling one to model languages for concurrency for example. Related work in this direction (not restricted to conflict-free systems) includes [13,15,65,54–56].

References

[1] S. Antoy, R. Echahed and M. Hanus, A needed narrowing strategy, in: Proc. 21st ACM Symp. on Principles of Programming Languages (1994) 268-279.

[2] S. Antoy and A. Middeldorp, A Sequential Reduction Strategy, Theoret. Comput. Sci. 165(1) (1996) 75-95.

[3] Z.M. Ariola, M. Felleisen, J. Maraist, M. Odersky, P.A. Wadler, A call-by-need lambda calculus, in: Proc. 22nd ACM Symp. on Principles of Programming Languages (1995) 233-246.

[4] A. Asperti and C. Laneve, Interaction systems I: The theory of optimal reductions, Mathematical Structures in Computer Science 11 (1993) 1-48.

[5] A. Asperti and C. Laneve, Interaction systems II: The practice of optimal reductions, Theoret. Comput. Sci. 159(2) (1996) 191-244.

[6] A. Asperti and H. Mairson, Parallel beta reduction is not elementary recursive, in: Proc. 25th ACM Symp. on Principles of Programming Languages (1998).

[7] A. Asperti and S. Guerrini, The Optimal Implementation of Functional Programming Languages (Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 199?). (To appear.)

[8] H. P. Barendregt, The Lambda Calculus, Its Syntax and Semantics (North-Holland, Amsterdam, 1984).

[9] H.P. Barendregt, J.A. Bergstra, J.W. Klop and H. Volken, Some notes on lambda-reduction, in: Degrees, reductions, and representability in the lambda calculus, Preprint no. 22, University of Utrecht, Department of mathematics, 1976, 13-53.

[10] H.P. Barendregt, J.R. Kennaway, J.W. Klop, M.R. Sleep, Needed reduction and spine strategies for the lambda calculus, Information and Computation 75(3) (1987) 191-231.

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

[12] G. Berry and J.-J. Lévy, Minimal and optimal computations of recursive programs, J. of the Association for Computing Machinery 26 (1979) 148-175.

[13] G. Boudol, Computational semantics of term rewriting systems. in: M. Nivat and J.C. Reynolds, eds., Algebraic methods in semantics (Cambridge University Press, 1985) 169-236.

[14] A. Church and J.B. Rosser, Some properties of conversion, Transactions of American Mathematical Society 39 (1936) 472-482.

[15] D. Clark and J.R. Kennaway, Event structures and non-orthogonal term graph rewriting, Mathematical Structures in Computer Science 6 (1996) 545-578.

[16] H.B. Curry and R. Feys, Combinatory Logic, Vol. 1 (North-Holland, Amsterdam, 1958).

[17] P. Gardner, Discovering needed reductions using type theory, in: Proc. TACS’94, Lecture Notes in Computer Science, vol 789 (Springer, Berlin, 1994) 555-574.

[18] J.R.W. Glauert and Z. Khasidashvili, Relative normalization in orthogonal expression reduction systems, in: Proc. CTRS’94, Lecture Notes in Computer Science, vol. 968 (Springer, Berlin, 1994) 144-165.

[19] J.R.W. Glauert and Z. Khasidashvili, Minimal and optimal relative normalization in orthogonal expression reduction systems, Technical Report SYS-C94-06, UEA Norwich, 1994.

[20] J.R.W. Glauert and Z. Khasidashvili, Relative normalization in deterministic residual structures, in: Proc. CAAP’96, Lecture Notes in Computer Science, vol. 1059 (Springer, Berlin, 1996) 180-195.

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

[22] J.R.W. Glauert and Z. Khasidashvili, Stable results and relative normalization. (Submitted.)

[23] G. Gonthier, M. Abadi and J.-J. Lévy, The geometry of optimal lambda reduction, in: Proc. 19th ACM Symp. on Principles of Programming Languages (1992) 15-26.

[24] G. Gonthier, J.-J. Lévy and P.-A. Melliès, An abstract standardisation theorem, in: Proc. 7th IEEE Symp. on Logic in Computer Science (1992) 72-81.

[25] S. Guerrini, Theoretical and practical issues of optimal implementations of functional languages, Ph.D. Thesis, University of Pisa, 1996.

[26] R.J. Hindley, An abstract form of the Church-Rosser theorem I, Journal of Symbolic Logic 34(4) (1969) 545-560.

[27] B. Hoffmann and D. Plump, Implementing term rewriting by jungle evaluation, Theoretical Informatics and Applications 25 (1991) 445-472.

[28] G. Huet, Confluent reductions: Abstract properties and applications to term rewriting systems, J. of the Association for Computing Machinery 27(4) (1980) 797-821

[29] G. Huet and J.-J. Lévy, Computations in Orthogonal Rewriting Systems, in: J.-L. Lassez and G. Plotkin, eds., Computational Logic, Essays in Honor of Alan Robinson (MIT Press, 1991) 394-443.

[30] V. Kathail, Optimal interpreters for lambda-calculus based functional languages, Ph.D. Thesis, MIT, 1990.

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

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

[33] J.R. Kennaway, J.W. Klop, M.R. Sleep and F.-J. de Vries, Event structures and orthogonal term graph rewriting, in: M.R. Sleep, M.J. Plasmeijer, M.C.J.D. van Eekelen, eds., Term Graph Rewriting: Theory and Practice (John Wiley, 1993) 141-156.

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

[35] Z. Khasidashvili, β-reductions and β-developments of λ-terms with the least number of steps, in: Proc. COLOG’88, Lecture Notes in Computer Science, Vol. 417 (Springer, Berlin, 1990) 105–111.

[36] Z. Khasidashvili, The Church-Rosser theorem in orthogonal combinatory reduction systems, Report 1825, INRIA Rocquencourt, 1992.

[37] Z. Khasidashvili, Optimal normalization in orthogonal term rewriting systems, in: Proc. RTA’93, Lecture Notes in Computer Science, Vol. 690 (Springer, Berlin, 1993) 243-258.

[38] Z. Khasidashvili, Stable computational semantics of conflict-free rewrite systems. (Draft.)

[39] Z. Khasidashvili and J.R.W. Glauert, Discrete normalization and standardization in deterministic residual structures, in: Proc. ALP’96, Lecture Notes in Computer Science, vol. 1139 (Springer, Berlin, 1996) 135-149.

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

[41] Z. Khasidashvili and J.R.W. Glauert, Zig-zag, extraction and separable families in non-duplicating stable deterministic residual structures, Technical Report IR-420, Free University, Amsterdam, 1997.

[42] Z. Khasidashvili and J.R.W. Glauert, The geometry of orthogonal reduction spaces, in: Proc. ICALP’97, Lecture Notes in Computer Science, vol. 1256 (Springer, Berlin, 1997) 649-659.

[43] Z. Khasidashvili and J.R.W. Glauert, The geometry of conflict-free reduction spaces, Technical Report SYS-C98-04, UEA Norwich, 1998.

[44] Z. Khasidashvili and J.R.W. Glauert, Relating conflict-free stable transition and event models (extended abstract), in: Proc. MFCS’97, Lecture Notes in Computer Science, vol. 1295 (Springer, Berlin, 1997) 269-278.

[45] Z. Khasidashvili and J.R.W. Glauert, An abstract concept of optimal implementation, Technical Report SYS-C97-01, UEA Norwich, 1997.

[46] J.W. Klop, Combinatory reduction systems (Mathematical Centre Tracts no. 127, Amsterdam, 1980).

[47] J.W. Klop, Term rewriting systems, in: S. Abramsky, D. Gabbay and T. Maibaum, eds., Handbook of Logic in Computer Science, Vol. 2 (Oxford University Press, 1992) 1-116.

[48] Y. Lafont, Interaction nets, in: Proc. 17th ACM Symp. on Principles of Programming Languages (1990) 95-108.

[49] J. Lamping, An algorithm for optimal lambda calculus reduction, in: Proc. 17th ACM Symp. on Principles of Programming Languages (1990) 6-30.

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

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

[52] L. Maranget, Optimal derivations in weak λ-calculi and in orthogonal term rewriting systems, in: Proc. 18th ACM Symp. on Principles of Programming Languages (1991) 255-269.

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

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

[55] P.-A. Melliès, Axiomatic rewriting theory II: The lambda-sigma-calculus has the finite cone property, submitted.

[56] P.-A. Melliès, Axiomatic rewriting theory IV: A stability theorem in rewriting theory, in: Proc. 14th IEEE Symp. on Logic in Computer Science (1998).

[57] A. Middeldorp, Call by need computations to root-stable form, in: Proc. 24th ACM Symp. on Principles of Programming Languages (1997) 94-105.

[58] M. Nielsen, G. Plotkin and G. Winskel, Petri nets, event structures and domains, Part 1, Theoret. Comput. Sci. 13 (1981) 85-108.

[59] E. Nöcker, Efficient functional programming: Compilation and programming techniques, Ph.D. Thesis, Katholic University of Nijmegen, 1994.

[60] M. O’Donnell, Reduction strategies in subtree replacement systems, Ph.D. thesis, Cornell University, Ithaca, N.Y., 1976.

[61] V. van Oostrom, Confluence for abstract and higher-order rewriting, Ph.D. Thesis, Free University, Amsterdam, 1994.

[62] V. Van Oostrom, Higher order families, in: proc. RTA’96, Lecture Notes in Computer Science, vol. 1103 (Springer, Berlin, 1996) 392-407.

[63] V. Van Oostrom, Finite family developments, in: proc. RTA’97, Lecture Notes in Computer Science, vol. 1232 (Springer, Berlin, 1997) 308-322.

[64] G. Plotkin, Call-by-name, call-by-value and the λ-calculus, Theoret. Comput. Sci. 1 (1975) 125-159.

[65] F. van Raamsdonk, Confluence and normalisation for higher-order rewriting, Ph.D. Thesis, Free University, Amsterdam, 1996.

[66] B.K. Rosen, Tree-manipulating systems and Church-Rosser theorems, J. of the Association for Computing Machinery 20 (1973) 160-187.

[67] R.C. Sekar and I.V. Ramakrishnan, Programming in equational logic: Beyond strong sequentiality, Information and Computation 104(1) (1993) 78-109.

[68] E.W. Stark, Concurrent transition systems, Theoret. Comput. Sci. 64(3) (1989) 221-269.

[69] P.C. Wadsworth, Semantics and pragmatics of the lambda-calculus, Ph.D. thesis, University of Oxford, 1971.

[70] G. Winskel, Events in computation, Ph.D. Thesis, Edinburgh University, 1980.

[71] G. Winskel, An introduction to event structures, in: Proc. Linear time, branching time and partial order in logics and models of concurrency, Lecture Notes in Computer Science, vol. 354 (Springer, Berlin, 1989) 364-397.

[72] H. Xi, Evaluation under lambda abstraction, in: proc. PLILP’97, Lecture Notes in Computer Science, vol. 1292 (Springer, Berlin, 1997) 259-274.

[73] N. Yoshida, Optimal reduction in weak λ-calculus with shared environments, in: Proc. ACM Conference on Functional Programming Languages and Computer Architecture (1993) 243-252.