An Abstract Concept of Optimal Implementation

Zurab Khasidashvili NTT Basic Research Laboratories Atsugi, Kanagawa, 243-01, Japan

zurab@theory.brl.ntt.jp ^{∗}

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

Abstract

In a previous paper, we introduced Stable Deterministic Residual Structures (SDRSs), Abstract Reduction Systems with an axiomatized residual relation which model orthogonal term and graph rewriting systems, and Deterministic Family Structures (DFSs), which add an axiomatized notion of redex-family to capture known sharing concepts in the λ-calculus and other orthogonal rewrite systems. In this paper, we introduce and study a concept of implementation of DFSs. We show that for any DFS F, its implementation F_{I} is a non-duplicating DFSs 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. In F_{I}, one can implement optimal family-reductions in F. Further, we show that sharing is compositional: the sharing in a DFS F can be decomposed into a weaker sharing F′ (such as zig-zag) and a sharing in the implementation F′_{I} of F′ stronger than zig-zag. These results require 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 needed to develop an abstract extraction procedure, which was thought to require the tree structure of terms, and to show that the family concepts defined via zig-zag and via extraction yield the same relation.

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 [Lév78, Lév80]. There was no other way as Barendregt et al [BBKV76] showed that there does not exist a one-step optimal recursive β-reduction strategy on λ-terms. Such an implementation has indeed been achieved by Lamping [Lam90] and Kathail [Kat90], reviving interest in optimal graph reduction. Maranget [Mar91] generalized Lévy’s optimality theory to Orthogonal Term Rewriting Systems (OTRSs), Gonthier et al [GAL92] 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 constructor-destructor discipline [AL93, AL96]. More recently, van Oostrom generalized the optimality theory to the whole class of orthogonal Higher-Order Rewriting Systems (HORSs) [Oos96], and Guerrini developed a general theory of sharinggraph rewriting [Gue96].

∗Contact author: Tel: 81 462 403674; Fax: 81 462 404709; http://www.sys.uea.ac.uk/˜ zurab. Submission category:

regular research paper.

†Part of this work was supported by the Engineering and Physical Sciences Research Council of Great Britain under grant GR/H 41300. The first author was also supported by a Dutch NWO grant during his visit to Vrije Universiteit, Amsterdam, in October 1996.

Lévy introduced the family concept in three different ways: via a suitable 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 [Oos96]. However, the zig-zag family can be defined directly in R, and this yields a different, weaker, family concept [AL93]. Independently and much earlier, Kennaway and Sleep [KS89] defined a concept of labelling for orthogonal Combinatory Reduction Systems (CRSs), improving Klop’s original labelling system for CRSs [Klo80], which covers orthogonal TRSs and Interaction Systems. Their labelling is different from both Maranget’s labelling for OTRSs [Mar91] and Asperti-Laneve’s labelling for Interaction Systems [AL93].

This variety of family concepts, and development of alternative graph rewriting algorithms for optimal implementation of orthogonal rewriting systems, such as Term Graph Rewriting [KKSV93], Jungle Rewriting [HP91], and many others, inspired by Wadsworth’s original work on graph-based implementation of the λ-calculus [Wad71], created the need to develop an abstract notion of family general enough to cover all the existing notions, and refined enough to enable proof of normalization and optimality results. Such structures were introduced by the authors in [GK96] as Deterministic Family Structures (DFSs) building on recent developments of abstract reduction systems with an axiomatized residual relation, such as the Concurrent Transition Systems (CTSs) of Stark [Sta89] and the Abstract Reduction Systems (ARSs) of Gonthier et al [GLM92].

Our DFSs are defined as Deterministic Residual Structures (DRSs) with an axiomatized family relation. DRSs, in turn, are Abstract Reduction Systems with an axiomatized residual relation, similar to CTSs and ARSs, but with the difference that, unlike CTSs, the residual relation can be duplicating in DRSs and, unlike ARSs, there is no nesting relation on redexes defined or axiomatized in DRSs. Despite its highly abstract nature, a counterpart of Berry’s stability property [Ber79] enabled us to prove the normalization theorem for all DRSs, and not only w.r.t. normal forms, but in general for regular stable sets of ‘intermediate results’; all interesting sets of final terms, such as headnormal forms, weak head normal forms, etc, fall in the category of stable term-sets [GK96]. Moreover, a discrete theory of normalization can also be developed in Berry-stable DRSs (SDRSs), enabling one to construct reductions permutation-equivalent to a particular finite or infinite reduction, and to prove a version of the Standardization Theorem [KG96]. Further, as already mentioned, in DFSs one can prove the optimality theorem.

In this paper, we continue the abstract study of optimality theory started in [GK96]. We introduce an abstract concept of Lévy-implementation: With a DFS F we associate a non-duplicating DRS R_{I}, called the implementation of F, whose steps exactly correspond to complete familyreduction steps in F, thus, for example, they model sharing-graph implementation of Lévy’s complete family-reductions in the λ-calculus. It is not difficult to show that needed reductions in R_{I} (w.r.t. any stable set of results) correspond exactly to needed complete family-reductions in F, implying that the former indeed implement optimal computations in F in the sense of Lévy [Lév78, Lév80].

Further, we show that the family relation on R_{I} induced by that of F coincides with zig-zag, which is the weakest family sharing. At first sight, one might think that there is no need or possibility of a stronger sharing in non-duplicating SDRSs. However, this is not the case as the example of Asperti and Laneve [AL93] demonstrating ‘inadequacy’ of Lévy’s extraction algorithm for Interaction Systems is, when considered as an Abstract Reduction System, a non-duplicating SDRS. This example also shows that zig-zag does not coincide with the labelling and their extraction families based on the shift operation. These effects are caused by the fact that more than one members of a family can be created by a single step – the reduction step t = μ(λx.(xx)) → (μ(λx.(xx)) μ(λx.(xx))) = s, according to the μ-rule μ(λx.X) → [μ(λx.X)/x]X, simultaneously creates the two μ-redexes in s; these redexes are intuitively in the same family, but cannot be related by zig-zag, nor by an extraction procedure similar to Lévy’s. We call such families non-separable.

Actually, we show that the sharing concept formalized in DFSs is compositional: any sharing can be decomposed into a weaker sharing (such as zig-zag, when the latter forms a family-relation) and a non-separable 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 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 top-down and left-to right nature of the conventional concept of standardization.

The paper is organized as follows. In the next section, we recall the definitions of DRSs and DFSs and some relevant standardization results for them, and discuss examples. Section 3 gives a characterization of zig-zag relation via extraction, used in Section 4 to prove that zig-zag is a family relation in every non-duplicating stable DRS. In section 5 we show that a family relation in a non-duplicating SDRS is separable iff it is zig-zag. In Section 6 we define and study implementation DRSs, and show the compositionality of sharing. Conclusions appear in Section 7.

2 Deterministic Residual and Family Structures

In this section we recall Deterministic Residual Structures (DRSs) and Deterministic Family Structures (DFSs), and give a number of examples. We will also recall some basic theory of standardization in DRSs from [KG96].

2.1 Deterministic Residual Structures

A DRS is an Abstract reduction System (ARS) with an axiomatized residual relation. An ARS [Hin69] is a triple A = (Ter,Red,→) where Ter is a set of terms, ranged over by t, s, o, e; Red is a set of redexes (or redex occurrences), ranged over by u, v, w; and →: Red → (T er × T er) is a function such that for any t ∈ T er there is only a finite set of u ∈ Red such that → (u) = (t, s), written t→^{u}s. This set will be known as the redexes of term t, where u ∈ t denotes that u is a member of the redexes of t and U ⊆ t denotes that U is a subset of the redexes. Note that → is a total function, so one can identify u with the triple t→^{u}s. A reduction is a sequence t→^{u_{1}}t_{2}→^{u_{2}} . . .. Reductions are denoted by P, Q, N. We write P : t → → s or t → →^{P} s if P denotes a reduction (sequence) from t to s. |P | denotes the length of P. P + Q denotes the concatenation of P and Q. We use U, V, W to denote sets of redexes of a term.

The DRS concept is based on [Lév80, HL91]. DRSs model orthogonal term as well as graph rewrite systems, both first and higher order, and including the λ-calculus and its sharing evaluation models, with the standard Church notion of residual. Besides the CTSs of Stark [Sta89], and the ARSs of Gonthier et al. [GLM92], closely related, but more syntactically oriented, models are studied in [Oos94, Mel96, Raa96]. DRSs are a minimal axiomatization of the residual concept enabling one to develop a theory of normalization [GK96] and standardization [KG96] for conflict-free reduction systems in an abstract manner, and to study their semantics [KG97b, KG97a].

Definition 2.1 A DRS is a pair R = (A, /), where A is an ARS and / is a residual relation on redexes relating redexes in the source and target term of every reduction t→^{u}s ∈ A, such that for v ∈ t, the set v/u of residuals of v under u is a set of redexes of s; a redex in s may be a residual of only one redex in t under u, and u/u = ∅. If v has more than one u-residual, then u duplicates v. If v/u = ∅, then u erases v. A redex of s which is not a residual of any v ∈ t under u is said to be u-new or created by u. The set u/P of residuals of u 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] ([GLM92]) 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] ([Sta89]) Let u, v ∈ t, let u ≠ v, and let u/v = ∅. Then v/u ≠ ∅.

We call a DRS R stable (SDRS) if:

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

We call an SDRS non-duplicating or affine, ASDRS, if the residual relation is non-duplicating. Note that, since the only observables of DRSs are redexes, duplicating syntactic rewrite systems may still form affine SDRSs. For example, the DRS corresponding to innermost reductions in an orthogonal TRS is an affine SDRS, although innermost redexes may duplicate their arguments.

Similarly to [HL91, Lév78, Lév80, Sta89], in a DRS R the residual relation on redexes is extended to all co-initial reductions as follows: (P_{1} + P_{2})/Q = P_{1}/Q + P_{2}/(Q/P_{1}) and P/(Q_{1} + Q_{2}) = (P/Q_{1})/Q_{2}, and that Lévy-equivalence or permutation-equivalence is defined as the smallest relation on co-initial reductions satisfying: U +V/U ≈_{L} V +U/V and Q ≈_{L} Q′ ⟹ P +Q+N ≈_{L} P +Q′+N, where U and V are complete developments of redex sets in the same term. Further, one defines P ⊴ Q iff P/Q = ∅, and can show that P ≈_{L} Q iff P ⊴ Q and Q ⊴ P; and P ⊴ Q iff Q ≈_{L} P + N for some N. Below, P ⊔ Q will denote P + Q/P. Intuitively, P ≈_{L} Q means that P can be obtained from Q by a number of permutations of adjacent steps, therefore ‘Q and P do the same work’; and P ⊴ Q means that P does less work than Q, the difference being Q/P, so P + Q/P ≈_{L} Q. The following Strong Church-Rosser property can be proved: for any co-initial finite reductions P, Q, P ⊔ Q ≈_{L} Q ⊔ P.

The stability axiom, and more generally Lemma 2.3 below, states that a redex cannot arise from two ‘unrelated’ sources. The notion of ‘unrelated’ is formalized by the notion of externality, which expresses the absence of shared (residuals of) redexes.

Definition 2.2 ([GK96]) • 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}. We call P external to

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

[figure: t_{0}; P_{i}; t_{i}; u_{i}; t_{i+1}; Q_{j}; P_{i}/Q_{j}; Q_{j}/P_{i}; U_{i,j}; v_{j}; V_{i,j}]

Lemma 2.3 (Stability) ([GK96]) 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.

Lemma 2.4 (Weak Acyclicity) ([KG96]) Let P, N be external co-initial finite reductions in a DRS. Then N ≉_{L} P.

2.2 Standardization

In this section, we recall a fragment of results from [KG96], concerning standardization of reductions, relevant to this paper; so we restrict ourselves to affine stable DRSs, ASDRSs, only.

Definition 2.5 • 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 call u P -essential if there is no Q ≈_{L} P that discards u, and P -inessential 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 if u is Q/P′-needed. We call P Q-needed if so is every redex contracted in P. We call P self-needed if it is P -needed. The other concepts above are extended in the same way.

Note that P -neededness, P -erasure, and P -essentiality do not depend on the choice of a reduction in the class ⟨P ⟩_{L} of reductions Lévy-equivalent to P, 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 2.6 Let P : s → → t→^{u}e → → o in an ASDRS.

(1) w ∈ t is P -needed iff it is P -erased and P -essential.

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

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

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

Self-needed reductions play the role of standard reductions in SDRSs, since we do not have any nesting relation imposed on redexes, unlike ARSs of [GLM92], and there is no concept of ‘left’ or ‘right’ occurrences in DRSs. Furthermore, our concept of standardization captures the essence of the usual one in many respects. In particular, in the extraction process which we study below, selfneeded reductions play the same role as outside-in left-to-right standard reductions in the extraction processes of [Lév80, AL93, Oos96].

Definition 2.7 We call a reduction in a DRS standard if it is self-needed. We write P ≈_{S} Q if P ≈_{L} Q and both P and Q are standard. For any standard P, we define ⟨P ⟩_{S} = {Q | Q ≈_{S} P }.

The following algorithm is a standardization procedure for reductions in ASDRSs.

Definition 2.8 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 2.6). Then ST (P) = v + ST (P/v).

Termination of the standardization follows immediately from the fact that |P/v| ≤ |P | − 1. The following fragment (for ASDRSs) of the standardization theorem from [GK96] implies the correctness of our standardization procedure.

Theorem 2.9 (Standardization) For any finite reduction P in a stable non-duplicating DRS, ST (P) is a finite standard reduction Lévy-equivalent to P.

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 2.6 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 2.6.(2). If it is created by u_{n−2}, then the latter is P -needed too, by Lemma 2.6.(3). Otherwise, the ancestor redex of u_{n−1} in t_{n−2} is P -needed by Lemma 2.6.(4). 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; this can be shown exactly as the correctness of the standardization algorithm (and is also a corollary of the Discrete Normalization Theorem of [KG96]).

In Section 3, we will show that, moreover, all standard variants of a finite reduction P in an ASDRS can be found effectively (there are clearly only a finite number reductions in ST V (P) as they all have the same length, which coincides with the number of P -needed steps in P).

2.3 Deterministic Family Structures

We now recall Deterministic Family structures (DFSs) which are DRSs where in addition a notion of redex-family is axiomatized so that the essence of sharing in the sense of Lévy [Lév78, Lév80] is captured, and all the known family notions (mentioned in the introduction) satisfy these axioms [GK96].

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

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

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

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

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

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

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

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, ≃).

Despite its generality, our family concept does not cover all possible sharing concepts studied in the literature. For example, consider the TRS from [HP91] 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), 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 [HP91] (which allows ‘accidental’ sharing of possibly completely unrelated 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 a same family since (by [creation]) they have different contributor families.

The following special kinds of DFSs will play an important role in this paper.

Definition 2.11 (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{\begin{matrix}u \\  \end{matrix}}•  •
[figure: v_{2}; v′_{1}]
•

1This axiom was called [termination] in [GK96].

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 (without the name) are studied in [AL93] for Interaction Systems, where it is demonstrated that such a family relation is in general strictly larger than the zig-zag. Another important example where a non-separable sharing is reasonable is the lazy call-by-value λ-calculus, λ_{LV} [Plo75]. It 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. It is reasonable to share the two 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. 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. Note that the occurrences of u in s are created by v_{1} and v_{2}, as the occurrences of u in t and o are not λ_{LV} -redexes (they are not admissible).

3 Equivalence of Zig-zag and Extraction

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.

Lévy introduced an extraction procedure for the λ-calculus in [Lév78, Lév80] in order to prove decidability of the family relation. His extraction procedure is effective, and gives canonical representations 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 [AL93], and the second to van Oostrom [Oos96].

The ‘problem’ arises because a redex can create a number of redexes ‘intuitively’ 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 to belong to the same family, as labels of such redexes are the same. Such redexes cannot be related by the zig-zag if one works with the original system [AL93], but can be related if one works in the refinement of the original system [Oos96]. 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. 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 6 will shed further light on the separability problem.

Definition 3.1 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 ≈_{S} P′, then P v is canonical iff so is P′v. So canonical forms we speak of are actually objects ⟨P ⟩_{S}v, for standard finite reductions P. Our extraction algorithm, defined in Definition 3.4 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. In order for the extraction procedure to be decidable and imply that of the zig-zag relation, we need to establish the decidability of P -neededness for finite reductions P is ASDRSs.

Proposition 3.2 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 See Appendix A.

Lemma 3.3 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 See Appendix A.

Let ⟨P ⟩_{S}v not be canonical. By Definition 3.1, there is Q : t → →^{P′} e→^{u}s such that Q ≈_{L} P and v is a u-residual of some v′ ∈ e. By Lemma 3.3, Q can be chosen standard. In Q, u does not ‘contribute’ to v, and in the search for a shortest reduction that creates a redex in the zig-zag class of Qv, contraction of u can be omitted – P′v′ ≃_{z} P v and |P′| < |P |, since all standard Lévy-equivalent reductions have the same (minimal) length [KG96]. Obviously, reductions creating a redex in some family in a 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 ≈_{S} 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 3.4 (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 2.5.) ⇀ ⇀ 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 proof that it is confluent (modulo ≈_{S} on histories), it is enough to prove that it

is weakly confluent, that is, Qw′′↼^{v}Nw⇀^{u}P w′ implies Qw′′⇀^{u′}N^{∗}w^{∗}↼^{v′}P w′. We need a lemma first whose proof is delayed to Appendix B, to enable the reader to follow the main intuition.

Lemma 3.5 Let P +u ≈_{S} Q+v and let u ≠ v. Then there are P′v′ and Q′u′ such that P′+v′ ≈_{S} P, Q′ + u′ ≈_{S} Q, P′ ≈_{S} 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; ∅; ∅; ∅; ∅]

Theorem 3.6 (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. 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 3.4, we have from Qw′′↼^{v}Nw⇀^{u}P w′ that Q + v ≈_{S} N′ ≈_{S} P + u, where N′ is a standard variant of N, and w′′/v = w′/u = w. By Lemma 3.5, we have the following situation, where P′ + v′ ≈_{S} P, Q′ + u′ ≈_{S} Q, P′ ≈_{S} 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 3.4.

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 3.7 In an ASDRS, P u ≃_{z} Qv iff they have the same unique canonical form ⟨N⟩_{S}w. Proof By definition of ≃_{z}, P u ≃_{z} Qv implies existence of 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. 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} ≈_{S} 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 2.6.(3), w does not create the next step in P′_{1} (if w is not the last step in P′_{1}), therefore can be permuted with its next step. That w-step is again P′_{1}-unneeded by Lemma 2.6.(4), 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 ≈_{S}). Since u′_{1} has a residual along P_{1}^{∗} + Q_{1}, it is P_{0}-essential by Definition 2.5. Since w is P_{0}-unneeded, it is P_{0}-inessential by Lemma 2.6.(1). Hence w does not create u′_{1} by Lemma 2.6.(3).

But this is impossible since P′_{1}u′_{1} is canonical and w is the last step of P′_{1}. So we have proven that P′_{1} is P_{0}-needed. This implies that the standardization procedure of Definition 2.8 does not effect P′_{1} when applied to P′_{1} + P_{1}^{∗} + Q_{1}, i.e., we can assume a standard P′_{0} ≈_{S} 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. The theorem now follows from Theorem 3.6.

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.

4 Affine Zig-zag 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.

Below, F AM_{z}(P) (resp. SF AM_{z}(P)) denotes the set of zig-zag classes whose member (P - needed) 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 4.1 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 ≈_{S} 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 4.2 If P v ≃_{z} Qw, then v/(Q/P) = w/(P/Q). In particular, if P ≈_{S} Q, then v = w. Proof By Theorem 3.7, 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/(Q/P) = w/(Q′/P′) = u/(P′ ⊔ Q′) = u/(Q′ ⊔ P′) = v/(Q′/P′) = v/(Q/P).

Lemma 4.3 Let Q^{∗} : t → →^{P} s→^{u}e and u create 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 3.3 that Q = ST (Q^{∗}) = P′ + u′, where P ≈_{L} P′ + P′′ (for some Qunneeded P′′) and u = u′/P′′. If Qv is not a canonical form, by Lemma 3.3 there is an extraction step Qv⇀^{w_{1}}Q_{1}v_{1} (i.e., Q ≈_{S} Q_{1} + w_{1} and v = v_{1}/w_{1}). Since Q_{1} + w_{1} ≈_{S} Q = P′ + u′, we have by

Lemma 3.5 that Q_{1} ≈_{S} 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 3.6, for any canonical form Q′v′ of Qv (and hence of Q^{∗}v), Q′ ≈_{S} P_{m} + u_{m} and v_{m} = v′, it follows by Lemma 4.1 that Q′ contracts a redex in the family of P u.

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

Lemma 4.5 Let Q : e → →^{P} t→^{u}s and let u create v ∈ s. Then F am_{z}(P u) ↪_{z} F am_{z}(Qv). Proof By Lemma 4.3, if Q′v′ is a canonical form of Qv, then F am_{z}(P u) ∈ F AM_{z}(Q′). Now it follows from Lemmas 4.1 and 4.4 and Theorem 3.7 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).

Lemma 4.6 Let P : t_{0} → →^{P_{i}} t_{i}→^{u_{i}}t_{i+1} → → t_{n}. Then k < m implies F am_{z}(P_{k}u_{k}) ≠ F am_{z}(P_{m}u_{m}).

Proof By induction on the number of zig-zag classes ↪_{z}-contributing to F am_{z}(P_{k}u_{k}). Suppose on the contrary that F am_{z}(P_{k}u_{k}) = F am_{z}(P_{m}u_{m}). Let P′_{k}u′_{k} be a canonical form of P_{k}u_{k}, which exists by Theorem 3.6, 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}. Since P′_{k} contracts redexes in all contributor zig-zag classes of F am_{z}(P′_{k}u′_{k}) = F am_{z}(P_{k}u_{k}) = F am_{z}(P_{m}u_{m}), and since by the induction assumption no redexes in these classes 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 Lemma 4.5. 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_{z}(P′_{k}u′_{k}) = F am_{z}(P_{m}u_{m}) = F am_{z}(P′_{k}u′_{m}) and u′_{k} ≠ u′_{m}, which is not possible by Lemma 4.2 – contradiction.

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

Theorem 4.7 Let R be a non-duplicating stable DRS. Then F_{R} = (R, ≃_{z}, ↪_{z}) is a 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 3.7 that ∅_{t}u ≄_{z} ∅_{t}v, i.e., [initial] holds. [creation] is immediate from Lemma 4.5, and [FFD] from Lemma 4.6.

5 Affine Separable Families

Based on the results of previous sections, we now 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. Recall that a complete family-reduction is a multi-step reduction contracting, in each multi-step, all members of a single family in parallel (we will often omit ‘complete’).

We will need the following lemma from [GK96].

Lemma 5.1 (Unique Families) Every family is contracted at most once in a (complete) familyreduction, in a DFS.

Lemma 5.2 Let F = R, ≃, ↪) be an affine DFS. Them 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 family-reduction, and vice versa. Proof (1) ⇒ (2) Similar to the proof of Lemma 4.6, except replacing F am_{z}( ) by F am( ), using [creation] instead of Lemma 4.5, and using separability instead of Lemma 4.2 (see [KG97]).

(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 family-reduction, implying that P +v+w′∥w′′, where w′∥w′′ is the multi-step contracting w′ and w′′ in parallel, is a family-reduction which is not a reduction, contradicting (4).

Lemma 5.3 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 3.1, 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 2.6) a canonical element of ϕ in which a step whose family does not contribute to ϕ is contracted later than w in P – a contradiction.

Theorem 5.4 An affine DFS F is separable iff it is a zig-zag DFS. Proof (⇒) Let F = (R, ≃_{s}, ↪_{s}) be separable, and let P u ≃_{s} Qv. (We want to prove that P u ≃_{z} Qv.) By the Extraction Theorem, there are canonical forms P′u′ ≃_{z} P u and Q′v′ ≃_{z} Qv, and since ≃_{z}⊆≃_{s} (by the definition of DFSs), P′u′ ≃_{s} Q′v′. Now if P′ ≈_{S} Q′, since both P′u′ and Q′v′ are canonical, the last step of P′ creates both u′ and v′, and u′ = v′ by separability. Hence, P′u′ ≃_{z} Q′v′, implying P u ≃_{z} Qv, in this case. Otherwise, we must have P′ ≉_{L} Q′ (as P′, Q′ ∈ ST A), and if say P′ ⊲ Q′, Q′ ≈_{L} P′ + P′′ for some P′′ ≠ ∅. Again, since P′u′ and Q′v′ are canonical, the last step of P′ creates u′, and that of P′′, call it w, creates v′ (since the last step of P′′ coincides with that of ST (P′ + P′′)). By [creation], F am(w) ↪_{s} F am(v′) = F am(u′), hence by [contribution] P′ must also contract a redex in F am(w), contradicting separability by Lemma 5.2. Hence P′ ≉_{L} Q′ cannot hold, and we are done. (⇐) Let F be a ZDFS. By Lemma 4.6, any family is contracted at most once in a reduction in F, implying by Lemma 5.2 that F is an SDFS.

We conclude this section by a useful characterization of histories of canonical elements of zig-zag (hence extraction and separable) families, in ASDRSs.

Theorem 5.5 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 5.3, P contracts only redexes in contributor families of ϕ. That every such a family is contracted in P follows immediately from [contribution]. The uniqueness of contracted families follows from Lemma 5.2 and Theorem 5.4.

6 Implementation DFSs

We now define the implementation F_{I} of a DFS F, whose reductions correspond to complete familyreductions 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-normalizing reductions. We will assume that the reduction graph of F is the reduction graph of an initial term, denoted by ∅, and that families are considered relative to ∅, i.e, all histories start with ∅.

Definition 6.1 Let F = (R, ≃, ↪) be a DFS. 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 of R_{I} = (A, /) are familyreductions starting from ∅, each edge (i.e., a reduction step) being a multi-step contracting a family of redexes.

• the residual relation / is defined as follows: let U and V be complete sets of redexes in two families, in a term s, and let U : s → o be the multi-step contracting U. Then V/U is the multi-step o → 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 family-reductions 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 6.2 Let P : ∅ → → s be a 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 family-reduction), and P + V contracts the family ψ twice, contradicting Lemma 5.1.

Thus the residual relation is well defined. Obviously, V/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 Acyclicity Lemma and 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 family-reductions can be viewed as reduction 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 5.1 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 5.4:

Theorem 6.3 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 6.4 Let F = (R, ≃) and F′ = (R, ≃′) be DFSs. We say that F has a stronger sharing than F′, written F ≥ F′, if ≃′⊆≃.

Theorem 6.5 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 (any) reductions in R corresponding to P and Q, and v′ and u′ are any R-redexes 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évy-equivalent, 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 ≃^{∗}, family-reductions in F^{∗} are exactly family-reductions in F, and F_{I}^{∗} = F_{I} follows since both are AZDFSs by Theorem 6.3. Since F > F′ and F′_{I} is an AZDFS, ≃^{∗} is strictly larger than zig-zag, hence is non-separable by Theorem 5.4. (⇐) Immediate from Definition 6.4.

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.

In order to prove that implementation DRS can implement optimal family-reductions in DFSs, let us recall the relative optimality theorem from [GK96]:

Definition 6.6 ([GK96]) (1) Let S be a set of terms in a DRS. 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 it S-unneeded otherwise. We call a multi-step U ⊆ t S-needed if it contracts at least one S-needed redex.

(2) We call a set S of terms stable if: (a) S is closed under parallel moves: for any t ∉ S, any P : t → → o ∈ S, and any Q : t → → e which does not contain redexes 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.

Theorem 6.7 (Relative Optimality [GK96]) 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 (complete) family-reduction Q starting from t is eventually S-normalizing and is S-optimal in the sense that it has a minimal number of family-reduction steps.

The following lemma, whose proof can be found in Appendix A, relates neededness in a DFSs with neededness in its implementation. Together with Theorem 6.7, it implies that the implementation DRSs F_{I} indeed correctly implement family-reductions in DFSs F: S-needed reduct ions in F_{I}, which actually are S-needed family-reductions by Lemma 5.2.(4) and Theorem 6.3, and hence are optimal, implement optimal family-reductions in F.

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

Corollary 6.9 (Optimal Implementation) Let S be a stable set of terms in a DFS F. Then optimal (i.e., S-needed) reductions in F_{I}, w.r.t. S, implement optimal family-reductions in F, w.r.t. S.

7 Conclusions and Future Work

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. Together with [GK96], this work completes the first chapter of an axiomatic study of the optimality theory.

Further, 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 simultaneously two different members of the same family. These results have been used essentially in constructing a fully adequate Event Structure style semantics for ASDRSs, and thereby, for all orthogonal reduction systems [KG97b]. The latter construction covers for example the construction of Event Semantics for orthogonal graph rewriting systems in [KKSV93, Sch94]. These results have also been used in the definition of independence of computations, and construction of Euclidian Geometry from the reduction spaces in orthogonal rewrite systems [KG97a].

Finally, we have shown that sharing is compositional. In particular, any family relation can be decomposed into the 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 [AL93]). This makes clear the importance of the comprehensive investigation of affine families undertaken in this paper. As for zig-zag, we have demonstrated in [GK96] (see Example 4.1) that zig-zag need not be a family-relation in any (duplicating) SDRS. However, we believe that suitable extensions of stable DRSs can be defined, in which one can extended our construction of zig-zag ASDRSs to the general (duplicating) case, and our proofs can be used as a basis. In the general case, the [FFD] axiom of DFSs (which fails to hold in Example 4.1 mentioned above) 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.

References

[AL93] Asperti A., Laneve C. Interaction Systems I: the theory of optimal reductions. MSCS, 11:1-48, Cambridge University Press, 1993.

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

[BBKV76] Barendregt H. P., Bergstra J., Klop J. W., Volken H. Degrees, reductions and representability in the λ-calculus. Report 22, University of Utrecht, 1976.

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

[GK96] Glauert J.R.W., Khasidashvili Z. Relative normalization in deterministic residual structures. CAAP’96, Springer LNCS, vol. 1059, H. Kirchner, ed. 1996, p. 180-195.

[GAL92] Gonthier G., Abadi M., Lévy J.-J. The geometry of optimal lambda reduction. POPL’92, p.15-26.

[GLM92] Gonthier G., Lévy J.-J., Melliès P.-A. An abstract Standardisation theorem. LICS’92, p. 72-81.

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

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

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

[HP91] Hoffmann B., Plump D. Implementing term rewriting by Jungle evaluation. Theoretical Informatics and Applications 25:445-472, 1991.

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

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

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

[KG96] Khasidashvili Z., Glauert J. R. W. Discrete normalization in Deterministic Residual Structures. ALP’96, Springer LNCS, 1139, M. Hanus, M. Rodríguez-Artalejo, eds. 1996, p.135-149.

[KG97] Khasidashvili Z., Glauert J. R. W. Zig-zag, extraction and separable families in stable non-duplicating Deterministic Residual Structures. Technical Report IR-420, Free University, Amsterdam, February 1997. 24 pp.

[KG97a] Khasidashvili Z., Glauert J. R. W. The Geometry of Orthogonal Reduction Spaces. ICALP’97, Springer LNCS, vol. 1256, P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, eds. 1997, p. 649-659.

[KG97b] Khasidashvili Z., Glauert J. R. W. Relating conflict-free transition and event models. MFCS’97, Springer LNCS, vol. 1295, I. Prívara, P. Ružička, eds. 1997, p. 269-278.

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

[Lam90] Lamping J. An algorithm for optimal lambda calculus reduction. POPL’90, p.16-30. [Lév78] Lévy J.-J. Réductions correctes et optimales dans le lambda-calcul, Thèse de l’Université

de Paris VII, 1978. [Lév80] Lévy J.-J. Optimal reductions in the Lambda-calculus. In: To H. B. Curry: Essays on

Combinatory Logic, Lambda-calculus and Formalism, Hindley J. R., Seldin J. P. eds, Academic Press, 1980, p. 159-192.

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

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

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

[Oos96] Van Oostrom V. Higher order families. RTA’96, Springer LNCS, vol. 1103, Ganzinger, H., ed., 1996, p. 392–407.

[Plo75] Plotkin G. Call-by-name, call-by-value and the λ-calculus. TCS(1):125-159, 1975.

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

[Sch94] Schied G. On relating rewrite systems and graph grammars to event structures. In: Schneider H.-J. Ehrig H., eds. GTCS’94, Springer LNCS, vol. 776, 1994, p. 326-340.

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

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

[WN95] Winskel G., Nielsen M. Models for concurrency. In: S. Abramsky, D. Gabbay, and T. Maibaum eds. Handbook of Logic in Computer Science, vol. 4, OUP, 1995, p. 1-148.

Appendix A

Proof of Proposition 3.2 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 2.5 and Lemma 2.6.(2). 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 2.5 (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 2.6.(4). 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 2.5; 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 2.5), then u_{0} is P -needed by Lemma 2.6.(3); if not, then we arrive to a previously considered case, and the decidability of P -neededness follows. The rest follows from the correctness of the construction of a standard variant of P discussed in Subsection 2.2.

Proof of Lemma 3.3 We show that ST (Q) can be taken for Q′. By Definition 2.8, 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 2.6.(2), 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 2.6.(3), P′′ cannot create u, i.e., there is u′ ∈ o such that u′/P′′ = u, and u′ is Q-needed by Lemma 2.6.(4). Since P′′/u′ is Q-unneeded by Lemma 2.6.(4), and since the last step of P′ + u′ + P′′/u′ is Q-needed by Lemma 2.6.(2), P′′/u′ = ∅. Since u′ is Q-needed and P′′ is Q-unneeded, P′′ is external to u′ by Lemma 2.6.(4). Hence, by the Stability Lemma, u′ does not create v, and the lemma follows since ST (Q) = P′ + u′ is standard by Theorem 2.9, 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; ∅]

Proof of Lemma 6.8 (⇒) Assume that P be S-needed, and suppose on the contrary that P_{I} is not S-needed, i.e., u_{i} is S-unneeded for some i. Then there is an S-normalizing reduction N : t_{i} → → s that is external to u_{i}. It remains to show that any corresponding 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 6.2 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-needed. Suppose on the contrary that U_{i} is not S-needed for some i. Let Q be an S-needed S-normalizing family-reduction (which exists by Theorem 6.7). Note that the residual of U_{i} in any term along Q forms a complete family by Lemma 6.2, and all residuals of redexes in U_{i} remain S-unneeded by Corollary 3.1 of [GK96] (which states exactly that the residuals of S-unneeded redexes remain S-unneeded). Thus residuals of U_{i} along Q are redex-sets disjoint from the contracted redex-sets, implying that the corresponding reduction of Q in F_{I} is external to u_{i}, which contradicts S-neededness of u_{i}.

Appendix B: Proof of Lemma 3.5

We use the following lemma from [GK96], and three simple new lemmas in this proof.

Lemma 7.1 ([GK96]) Let P : t → → s be external to a set U ⊆ t of redexes, in a DRS, and let Q : t → → o. Then P/Q is external to the set U/Q.

Lemma 7.2 Let u + P ≈_{S} 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 2.5, 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 non-duplicating), 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 7.1 that Q^{∗} = Q/v^{∗} is external to u^{∗}. Since u is u + P -needed, so is u^{∗} by Lemma 2.6.(4). 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 7.3 Let P + u ≈_{S} Q + v and let u ≠ v. Then P ≉_{L} Q. Proof Suppose on the contrary that P ≈_{L} Q. Then P + u ≈_{S} Q + v iff u ≈_{L} v. But, by [weak acyclicity], this is only possible when u = v – a contradiction.

Lemma 7.4 Let P ≈_{S} Q. Then any non-empty step in Klop’s diagram of P and Q in P -needed. Proof Since every step in the diagram is a residual of a redex contracted in P or Q, the lemma follows immediately from Lemma 2.6.(4).

Proof of Lemma 3.5 Since P + u ≈_{S} Q + v, we have v ≈_{L} (P + u)/Q. By Lemma 2.4, (P + u)/Q contracts a residual of v. 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, by [weak acyclicity], v = u/(Q/P). Further, by Lemma 7.3, P ≉_{L} Q, hence P/Q = ∅ implies 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 7.4. 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 ≈_{S} 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 7.2, v′′ + P_{2} + u can be transformed into a reduction P′_{2} + v′ + u such that v′′ + P_{2} ≈_{S} 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′ ≈_{S} P and P′v′ ⊴_{z} Qv. Existence of Q′u′ such that Q′ + u′ ≈_{S} 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 7.2 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 2.4 and Lemma 7.4 that P′/Q′ = ∅. The converse is proved similarly, so P′ ≈_{L} Q′. It follows that u = u′/v′ and v = v′/u′.