Zig-zag, Extraction and Separable Families in Non-duplicating Stable Deterministic Residual Structures

Zurab Khasidashvili Department of Mathematics and Computer Science Free University De Boelelaan 1081a, 1081 HV Amsterdam, Netherlands zurab@cs.vu.nl

John Glauert School of Information Systems University of East Anglia 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 are SDRSs with an axiomatized notion of redex-family to capture known sharing concepts in the λ-calculus and other orthogonal rewrite systems. In this paper, we start to investigate ways of constructing DFSs from SDRSs. This is interesting for at least the following two purposes:

(1) to develop an algebraic theory of sharing for conflict-free rewrite and transition systems in order to understand what properties a sharing concept must possess to imply a reasonable theory of optimal evaluation, and

(2) to give an Event Structure style semantics to conflict-free rewrite and transition systems with erasure of redexes.

As a first step, we only consider non-duplicating systems, and show that every non-duplicating SDRS is already a DFS if zig-zag is taken for the family relation. (Zig-zag is simply the symmetric and transitive closure of the residual relation on redexes with histories.) We also show that the family relation in a non-duplicating DFS coincides with zig-zag if and only if it is separable in some sense. To achieve 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. As a side result, we get a Prime Event Structure semantics for non-duplicating SDRSs. Various forms of conflict-free Graph Rewriting Systems (or Graph Grammars) fall in the category of SDRSs.

∗This work was supported by the Engineering and Physical Sciences Research Council of Great Britain under grant GR/H 41300. It was (essentially) completed during a fruitful visit of the first author to Vrije Universiteit in October 1996, where he was supported by a Dutch NWO grant.

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 s by reduction of some graph representation, in which every multi-step would be represented by contraction of a single redex [Lév78, Lév80]. There was no other way – Barendregt et al [BBKV76] showed that there does not exist a onestep 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 of it, to Interaction Systems, which cover most of the languages with a constructor-destructor discipline [AsLa93, AsLa96]. Recently, van Oostrom has generalized the optimality theory to the whole class of orthogonal Higherorder Rewrite Systems (HORSs) [Oos96].

Lévy introduced the family concept in three different ways: via a suitable notion of labelling, via extraction, and by zig-zag. In each definition, a family is a class of objects of the form P v, where P is a finite reduction starting from a term t and ending in s, and v is a redex in s. Here P is called the history of P v; all histories of redexes in the same family are co-initial, i.e., start at the same term t. In the labelling definition of families, the initial term t gets an initial labelling, and labels grow along the reduction. Two redexes with co-initial histories are declared to be in the same family if they have the same label. The extraction process starting from a redex P v consists of elimination from P of all redexes ‘not contributing’ to v, and results in a reduction P′v′ such that P′ is standard (therefore unique in its permutation-equivalence class), and P v is a residual of P′v′, i.e., v is a residual of v′ under some reduction from the final term of P′ to that of P. Two redexes (with histories) are defined to be in the same extraction-family if the extraction process yields the same result for both redexes. Finally, the zig-zag relation is defined simply as the transitive and symmetric closure of the residual relation on redexes with histories. Clearly, all the above family concepts are equivalence relations, and Lévy 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 family concept [AsLa93]. Independently and much earlier, Kennaway and Sleep [KeSl89] defined their concept of labelling for orthogonal Combinatory Reduction Systems (CRSs), improving Klop’s original labelling system for CRSs [Klo80], which cover orthogonal TRSs and Interaction Systems, and their labelling is different from both Maranget’s labelling for OTRSs [Mar91] and Asperti-Laneve’s labelling for Interaction Systems [AsLa93].

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 [HoPl91], DAG (Directed Acyclic Graph) Rewriting [Mar91], and many others (in particular, covering cyclic graph reduction as well), 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 indeed introduced by the authors in [GlKh96] as Deterministic Family Structures (DFSs). This became possible also due to recent developments of abstract reduction systems with 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. (Therefore, DRSs cover more rewrite and transition systems than conflict-free CTSs or ARSs.) CTSs have successfully been used to give semantics to machine networks, while ARSs have been used to study more syntactic properties of orthogonal rewrite systems, such as standardization. Despite its highly abstract nature, a counterpart of Berry’s stability property [Ber79] enables 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 ‘(partial) results’; all interesting sets of final terms, such as head-normal forms, weak head normal forms, etc, fall in the category of stable term-sets [GlKh96]. Moreover, a discrete theory of normalization can also be developed in Berry-stable DRSs, enabling one to construct reductions permutation-equivalent to a particular finite or infinite reduction, and to prove a version of the Standardization Theorem [KhGl96]. Further, as already mentioned, in DFSs one can prove the optimality theorem, and DFSs can be interpreted as (deterministic or conflict-free) Prime Event Structures (PESs) [NPW81, Win80, Win86/89].

In this paper, we study the possibility of defining a family relation in stable DRSs. As the first step, we will only consider non-duplicating SDRSs. At first sight, one might think that there is no need or possibility of sharing in such SDRSs, and that the optimality theory for nonduplicating SDRSs is simple. However, this is not the case – the very example of Asperti and Laneve [AsLa93] 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 (i.e., with the shift operation) extraction families. 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 (in a slightly simplified notation), 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. The situation is different with van Oostrom’s approach to extraction [Oos96] (see discussion in section 4).

We will show that the zig-zag relation is a family relation in the sense that it satisfies the family-axioms of DFSs. So every non-duplicating stable DRSs is in fact a DFS with zig-zag as the family relation. The family relation in a non-duplicating DFS need not coincide with zig-zag. However, if the family relation is separable, i.e., no redex can create two different redexes in the same family, then it must coincide with the zig-zag. The converse is also true – zig-zag is separable in non-duplicating DFSs. These results are obtained by defining an abstract extraction procedure and showing that zig-zag coincides with our extraction-family relation. The technical contribution 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. ^{1}

1Actually, the extraction process was claimed to be syntactic in [Lév80]. To quote Lévy [Lév80]: ‘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’.

Construction of DFSs from non-duplicating SDRSs has particularly important semantic applications. Since families in DFSs, ordered by the contribution relation, form (conflict-free) PESs, our construction yields a translation of determinate stable CTSs into conflict-free PESs (which are stable Event Structures [Win86/89]), linking two widely accepted (operational and domaintheoretic) models of computation. Moreover, in a forthcoming paper [KhGl96a], we define extensions of PESs with axiomatized permutation equivalence and erasure relations. We show that event models thus extended are equivalent to non-duplicating SDRSs (as they yield isomorphic reduction/configuration domains), and the construction in this paper of a DFS from non-duplicating SDRSs is one of the essential building blocks in establishing the above isomorphism.

The paper is organized as follows. In the next two sections, we recall the definitions of DRSs and DFSs, and some relevant standardization results for them. Section 4 gives a characterization of zig-zag relation via extraction, used in Section 5 to prove that zig-zag is a family relation in every non-duplicating stable DRS, which is the main result of this paper. In section 6 and show that a family relation in a non-duplicating SDRS is separable iff it is zig-zag. In section 7, we give useful characterizations of Lévy’s embedding and equivalence relations via zig-zag. In section 8, we discuss an application of our results. Conclusions appear in Section 9.

2 Deterministic Residual and Family Structures

In this section we recall the definition of Deterministic Residual Structures (DRSs), which are Abstract Reduction Systems (ARSs) satisfying certain properties concerning residuals, and Deterministic Family Structures (DFSs) which are DRSs with an axiomatized family relation on redexes with histories. We will also introduce zig-zag and separable DFSs, and discuss an example.

A definition and some results about ARSs can be found e.g., in [Klo92]. Our definition is slightly different, and follows that of Hindley [Hin64].

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

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 [Lév78, HuLé91, Klo80, Kat90, Lam90, Kha92, KKSV93, Nip93, Oos94, Raa96, Gue96]. 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].

Definition 2.2 (Deterministic Residual Structure) A Deterministic Residual Structure (DRS for short) 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

[figure: t; u; e; w; s; v; u/v; o; v/u; w/(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 of residuals of a redex under any reduction is defined by transitivity.

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

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

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

We call a DRS R non-duplicating or affine, ADRS, if the residual relation in R is nonduplicating.

Non-duplicating DRSs which we study here are essentially determinate CTSs, with no distinguished start states. Having in mind possible generalization of our results to the non-affine case, we will still speak of affine DRSs, rather than DCTSs.

Similarly to [HuLé91, 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 above relations can equivalently be defined also using Klop’s method of commutative diagrams [Klo80, Bar84].

Definition 2.3 We call a DRS R stable (SDRS) if the following axiom is satisfied:

• [stability] If u, v ∈ t are different redexes, t→^{u}e, t→^{v}s, and u creates a redex w ∈ e, then the redexes in w/(v/u) are not u/v-residuals of redexes of s, i.e., they are created by u/v (see the diagram above).

The stability axiom, and more generally Lemma 2.5 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. For syntactic systems externality is a natural concept relating to overlap between components of terms involved in reduction steps.

Definition 2.4 ([GlKh96]) • 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}]

Obviously, P is external to the set U iff it is external to any development of U, and is external to a redex u iff it is external to the reduction contracting u. Note that a reduction external to one complete development of U need not be external to all developments of U, and in general, externality is not invariant under ≈_{L}. For, consider a TRS R = {a → a′, f(x) → b, g(x) → c}, a term t = f(g(a)), and reductions P : t→^{a}f(g(a′))→^{f}b, Q : t→^{a}f(g(a′))→^{g}f(c), and N : t→^{g}f(c). Then we have Q ≈_{L} N, P is external to N, but not to Q; and P is not external to U = {a, g(a)}.

Lemma 2.5 (Stability Lemma) ([GlKh96]) Let P : t → → s be external to Q : t → → e, in a stable DRS, and let P create redexes W ⊆ s. Then the residuals W/(Q/P) of redexes in W are created by P/Q, and Q/P is external to W.

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 is captured, and all the known family notions (mentioned in the introduction) satisfy these axioms [GlKh96]. It is shown in [GlKh96] that any DFS is a stable DRS.

Definition 2.6 (Deterministic Family Structure) A Deterministic Family Structure (DFS for short) 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.^{2}

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

Definition 2.7 (1) We call a DFS F a zig-zag DFS, ZDFS, if its family relation is the zig-zag ≃_{z}; the corresponding contribution relation ↪_{z} is determined by [contribution]. (In general, one might view [contribution] as the definition of ↪ via ≃, rather than as an axiom.)

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

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 again ψ ↪ ϕ_{1}, ϕ_{2}, and this would yield a ZDFS.

Non-separable families (without the name) are studied in [AsLa93] for Interaction Systems, where it is demonstrated that such a family relation is in general strictly larger than the zig-zag. They only study ‘reasonable’ separable families, where reasonability is only visible from the fine structure of rewrite steps (which may involve creation of a redex and its duplication or erasure in an atomic move). We will comment on it below. On the contrary, ‘accidental’ sharing is employed in graph rewriting systems of [HoPl91], where sharing of redexes with the same pattern are allowed even if they have completely different origin. Such an approach goes beyond Lévy’s approach of optimality, but is completely legal for our concept of DFSs. As we have shown in [GlKh96], such a sharing also allows a reasonable theory of optimality, as long as our family axioms are satisfied.

2This axiom was called [termination] in [GlKh96, KhGl96].

3 Standardization

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

Definition 3.1 • 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, or more precisely, P′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 discards concept however does depend on the particular reduction in the Lévy-equivalence class.

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

(1) w ∈ t is P -needed iff it is P -erased and P -essential. Consequently, P is self-needed iff it is self-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, self-needed reductions play the same role as outside-in left-to-right standard reductions in the extraction processes of [Lév80, AsLa93, Oos96].

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

Definition 3.3 Let P : t → → s. The canonical standard variant of P, ST (P), is defined as follows: If P = ∅, when 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 3.2). 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 [GlKh96] implies the correctness of our standardization procedure.

Theorem 3.4 (Standardization) For any finite reduction P in a stable non-duplicating DRS, ST (P) is a 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 3.4 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 3.4.(2). If it is created by u_{n−2}, then the latter is P -needed too, by Lemma 3.4.(3). Otherwise, the ancestor redex of u_{n−1} in t_{n−2} is P -needed by Lemma 3.4.(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 [KhGl96]).

In the next section, 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 – the number of P -needed steps in P).

4 Equivalence of Zig-zag and Extraction

In this section, we introduce an abstract extraction algorithm 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. The 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 [AsLa93], and the second to van Oostrom [Oos96].

The ‘problem’ arises because a redex can (in general) create a number of redexes ‘intuitively’ in the same family, something which cannot happen in the λ-calculus or in 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 arguments of the contracted redex and 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 [AsLa93], 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 live with 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. On the contrary, van Oostrom works with the refined rewrite systems (where reduction steps are either TRS steps or substitution steps) and no operation like shift is necessary to ensure coincidence of labelling, extraction and zig-zag families.

To summarise, note that [AsLa93] work with non-separable families, from which many difficulties arise, while [Oos96] works with separable ones, and coincidence of the three family concepts can be established more smoothly in the latter case. We find the latter solution more appealing and correct, as labelling anyway (implicitly) requires work with refined systems. Therefore, the abstract extraction algorithm which we introduce below follows van Oostrom’s approach. Our results will shed further light on the separability problem, and as we will also show in our abstract setting, it is not surprising that the family relation of [AsLa93] does not coincide with the zig-zag in Interaction Systems in general.

Definition 4.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 4.4 below, transfers 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 4.2 For any finite reduction P in an ASDRS, P -neededness of redexes in all terms of P is decidable, and 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 3.1 and Lemma 3.2.(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 3.1 (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 3.2.(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 3.1; 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 fist step of P′_{1} (which is P -needed by Definition 3.1), then u_{0} is P -needed by Lemma 3.2.(3); if not, then we arrive to a previously considered case, and both decidability of P -neededness and the standardization procedure follow.

Lemma 4.3 Let Q : t → →^{P} s→^{u}e and let 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 (that is, P ≈_{L} P′ + P′′ and u = u′/P′′) and u′ does

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

Let ⟨P ⟩_{S}v not be canonical. By Definition 4.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 4.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évyequivalent reductions have the same (minimal) length [KhGl96]. Obviously, reductions creating a redex in some family in a quickest way must be standard, since they are the shortest in their Lévyequivalence 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}, 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 4.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 3.1.) ⇀ ⇀ 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 can be found in the appendix.

Lemma 4.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 4.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 4.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 4.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, it follows immediately from [stability] that 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 4.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 4.7 In a non-duplicating stable DRS, 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.

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} ≈_{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 3.2.(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 3.2.(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 3.1. Since w is P_{0}-unneeded, it is P_{0}-inessential by Lemma 3.2.(1). Hence w does not create u′_{1} by Lemma 3.2.(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 3.3 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 4.6.

This theorem, together with decidability of construction 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.

5 Affine Zig-zag Families

In this section we establish the main result of this paper – we show that, in ASDRSs, the zig-zag relation forms a family relation, that is, it satisfies the family axioms of DFSs. We also give a useful characterization of Lévy-equivalence via self-needed families.

Below, F AM_{z}(P) (resp. SF AM_{z}(P)) denotes the set of zig-zag classes whose member (resp. P -needed) redexes are contracted in P, in an ASDRS; and F am_{z}(Qu) denotes the zig-zag class of Qu.

Lemma 5.1 Let P be Q-needed, in an ASDRS. Then F AM_{z}(P) ⊆ F AM_{z}(Q). In particular, if P ∈ ST AQ, 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 5.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 4.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 5.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 4.3 that Q = ST (Q^{∗}) = P′ + u′, where Q ≈_{L} P′ + P′′ (for some Qunneeded P′′) and u = u′/P′′. If Qv is not a canonical form, by Lemma 4.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 4.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 4.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 5.1 that Q′ contracts a redex in the family of P u.

Lemma 5.4 Let P v⇀^{w}P′v′. Then F AM_{z}(P′) ⊆ F AM_{z}(P). Proof P v⇀^{w}P′v′ implies that P ≈_{L} P′ + w, and by Lemma 5.1, F AM_{z}(P′) ⊆ F AM_{z}(P′ + w) ⊆ F AM_{z}(P).

Definition 5.5 Let ϕ′, ϕ be zig-zag classes. We write ϕ′ ↪_{z} ϕ iff for any P u ∈ ϕ, P contracts a redex (with history) in ϕ′. (Note that this definition does not conflict with the definition of ↪_{z} in Definition 2.2.)

Lemma 5.6 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 5.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 5.1 and 5.4 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 5.7 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}v_{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}v_{m}). Let P′_{k}u′_{k} be a canonical form of P_{k}u_{k}, which exists by Theorem 4.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 5.6. 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 5.2 – a contradiction.

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

Theorem 5.8 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 4.7 that ∅_{t}u ≄_{z} ∅_{t}v, i.e., [initial] holds. [creation] is immediate from Lemma 5.6, and [FFD] from Lemma 5.7.

6 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 Fvia 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 family-reduction is a multi-step reduction contracting, in each multi-step, all members of a single family in parallel.

Lemma 6.1 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) Exactly as the proof of Lemma 5.7, except replacing F am_{z}( ) by F am( ), using [creation] instead of Lemma 5.6, and using affineness instead of Lemma 5.2.

(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 [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 multistep contracting w′ and w′′ in parallel, is a family-reduction which is not a reduction, contradicting the assumption (4).

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

Theorem 6.3 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 6.1. Hence P′ ≉_{L} Q′ cannot hold, and we are done.

(⇐) Let F be a ZDFS. By Lemma 5.7, any family is contracted at most once in a reduction in F, implying by Lemma 6.1 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 6.4 Let P v be a canonical element of a family ϕ, in an affine zig-zag DFS F_{R} = (R, ≃_{z} , ↪_{z}). Then P contracts exactly one redex in every contributor family of ϕ. Proof By Lemma 6.2, 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 6.1 and Theorem 6.3.

7 Characterizing Lévy-equivalence via Zig-zag

Lemma 7.1 Let P and Q be standard co-initial finite reductions. Then P ≈_{L} Q iff F AM_{z}(P) = F AM_{z}(Q). Proof (⇒) Immediate from Lemma 5.1. (⇐) 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 for Lemma 5.1). 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 5.2, 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}(u) ∉ F AM_{z}(Q) – a contradiction.

Lemma 7.2 Let P be a finite reduction in an ASDRS. Then SF AM_{z}(P) = F AM_{z}(ST (P)).

Proof Let P : t_{0} → →^{P_{i}} t_{i}→^{u_{i}}t_{i+1} → →^{P_{i+1}} t_{n}, and let u_{i_{1}}, u_{i_{2}}, …, u_{i_{k}} be all P -needed steps in P (i_{1} <

i_{2} < …). Then, by Definition 3.3 and Lemma 3.2, ST (P) : t_{0} = s_{0}→^{v_{0}}s_{1}→^{v_{1}}s_{2}→^{u_{2}} … →^{v_{k}}s_{k+1}, where u_{i_{j}} is the first P′_{j}-needed step in P′_{j} = P/(v_{0} + v_{1} + … + v_{j−1}), and u_{i_{j}} is a residual of v_{j} along P′_{j}. Thus F am_{z}(v_{j}) = F am_{z}(u_{i_{j}}). And since SF AM_{z}(P) = {F am_{z}(u_{i_{j}}) | j = 0, 1, …, k} and F AM_{z}(ST (P)) = {F am_{z}(v_{j}) | j = 0, 1, …, k}, the lemma follows.

[figure: t_{0} = s_{0}; P_{i_{j}}; t_{i_{j}}; u_{i_{j}}; t_{i_{j}+1}; P_{i_{j}+1}^{∗}; t_{n}; −; P′_{0} = P]

[figure: s_{j}; t_{i_{j}}; ∅; u_{i_{j}}; t_{i_{j}+1}; P_{i_{j}+1}^{∗}; t_{n}; −; P′_{j}]

[figure: s_{j+1}; v_{j}; t_{i_{j}}; u_{i_{j}}; ∅; t_{i_{j}+1}; ∅; P_{i_{j}+1}^{∗}; t_{n}; −; P′_{j+1}]

Proposition 7.3 Let P and Q be co-initial finite reductions. Then P ≈_{L} Q iff SF AM_{z}(P) = SF AM_{z}(Q). Proof Indeed, P ≈_{L} Q iff (since P ≈_{L} ST (P) and Q ≈_{L} ST (Q) by the Standardization Theorem) ST (P) ≈_{L} ST (Q) iff (by the Standardization Theorem and Lemma 7.1) F AM_{z}(ST (P)) = F AM_{z}(ST (Q)) iff (by Lemma 7.2) SF AM_{z}(P) = SF AM_{z}(Q).

Lemma 7.4 Let P and Q be co-initial reductions in an ASDRS such that F AM_{z}(P) ⊆ F AM_{z}(Q). Then P ⊴ Q. Proof We need to show that, for any redex v contracted in P, say P = P′ + v + P′′, v/(Q/P′) = ∅. But since Q contracts a zig-zag related redex Q′w, we have by Lemma 5.2 that v/((Q′+w)/P′) = ∅, implying v/(Q/P′) = ∅.

Proposition 7.5 Let P, Q be finite co-initial reductions in an ASDRS. Then P ⊴ Q iff ∃Q′ : F AM_{z}(P) ⊆ F AM_{z}(Q′). Proof (⇒) P ⊴Q implies Q ≈_{L} P +Q′′ for some Q′′, hence F AM_{z}(P) ⊆ F AM_{z}(Q′) for Q′ = P +Q′′. (⇐) By Lemma 7.4.

8 An Application

We have shown that every affine stable DRS is in fact a DFS with zig-zag as the family relation. The latter, when it is a comma-DFS, i.e., its term set is the reduction graph of a single term, can be interpreted as a conflict-free Prime Event Structure (PES) by considering families as events and the contribution relation on families as the causal dependency relation. (A conflict-free PES is simply an event set partially ordered by a causal dependency relation, in which any element can dominate only a finite number of others [Win86/89].) Important examples of affine stable DRSs are several forms of graph rewriting systems, and many authors have studied the correspondence between graph rewriting systems and PESs before [KKSV93, Sch94, CELMR94, ClKe95]. Our translation is different, and seems conceptually more clear as it is for Abstract Reduction Systems. It is close in spirit to that in [KKSV93], although the latter construction uses the syntax of orthogonal Term Graph Rewriting Systems heavily, and our proofs are different.

Moreover, we construct an affine DFS model, which is more powerful and informative than the PES model as in the latter one cannot speak of equivalence of configurations corresponding to Lévy-equivalent reductions. Note that [Sch94, CELMR94] construct a PES model by constructing a corresponding trace language first, and applying known results relating Mazurkiewicz traces with Event Structures [Bed87], but this is only possible because the systems considered in [Sch94, CELMR94] (graph grammars) are linear – no duplication and no erasure of redexes are possible. It is well known that PESs are inadequate to give account to erasure of redexes, and a Lévyequivalence class of reductions cannot be interpreted by a single configuration. This problem is well discussed in [Lan93], Chapter 8.

To cope with that problem (caused by erasure), in [KhGl96a] we extend the conflict-free PES model with an axiomatized Lévy-equivalence relation in two different but equivalent ways: One by directly constraining the class of all equivalence relations on configurations, and another by axiomatizing the inessentiality or erasure relation expressing redundancy of an event for a configuration. The latter extends by further axioms an incomplete axiomatization of the inessentiality relation in [GlKh96]. In the resulting extended models, Deterministic Permutation and Erasure Event Structures, DPESs and DEESs, we can identify configurations with different numbers of events but still representing the same permutation-equivalence class of reductions. We show that permutation-equivalence classes of configurations in a DPES/DEES, appropriately ordered, are isomorphic to Lévy’s reduction space of the corresponding ASDRSs, therefore the former give a fully adequate semantics to affine SDRSs. And the construction in this paper of DFSs from affine SDRSs is one of the essential building blocks in establishing the above isomorphism. All known duplicating orthogonal systems can be interpreted as affine SDRSs by considering (complete) family-reductions only, which correspond to their optimal graph implementation.

9 Conclusions and Future Work

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 in constructing a fully adequate Event Structure style semantics for ASDRSs, and thereby, for all orthogonal reduction systems. The latter was our original motivation for construction of DFSs from ASDRSs, and it was not immediate that this would require us to develop an extensive optimality theory for ASDRSs.

From the point of view of the optimality theory itself, our results are more of methodological significance rather than of practical value. However, we believe that suitable extensions of stable DRSs can be defined, based on the residual relation alone, in which one can extended our results to the general (duplicating) case, and our proofs can be used as a basis. For example, the concept ‘P is internal to an argument of a redex u in t’, used in all syntactic extraction algorithms, can be replaced by the concept ‘P is internal to a set of redexes V in t’, where P is internal to V iff it is external to the compliment of V. 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, but proofs will become more complicated.

To conclude, let us mention that non-deterministic Residual Structures must be considered as well. For example, semantics of non-orthogonal rewrite systems is studied in Boudol [Bou85], and constructions of Event Structures from non-orthogonal graph rewriting systems are studied, among others, in [CELMR94, ClKe95]. Further, the theory of Standardization and Discrete Normalization developed in [KhGl96] for (semi-linear) stable DRSs, which we used here, are equally applicable to the non-deterministic case, as non-deterministic Residual Structures, when restricted to the Lévy-equivalence class of a reduction, become deterministic.

Acknowledgements

The first author wishes to thank Jan Willem Klop, Jean-Jacques Lévy, Luc Maranget, Vincent van Oostrom and Roel de Vrijer for the opportunity to work at INRIA Rocquencourt and VU Amsterdam and in October 1996, where this work was essentially completed, and for fruitful discussions.

Diagrams were drawn using Paul Taylor’s Diagram package.

References

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

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

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

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

[Bed87] Bednarczyk M. A. Categories of asynchronous systems. PhD Thesis, University of Sussex, Brighton, 1987.

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

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

[ClKe95] Clark D., Kennaway R. Some properties of non-orthogonal term graph rewriting. Electronic Notes in Theoretical Computer Science, vol. 2, A. Corradini, U. Montanari, eds. Elsevier, 1995, p. 141-150. To appear in MSCS.

[CELMR94] Corradini A., Ehrig H., Löwe M., Montanari U., Rossi F. An event structure semantics for safe graph grammars. In proc PROCOMET’94, IFIP Transactions A-56, 1994.

[GlKh96] Glauert J.R.W., Khasidashvili Z. Relative normalization in deterministic residual structures. In: Proc. of the 19^{th} International Colloquium on Trees in Algebra and Programming, CAAP’96, Springer LNCS, vol. 1059, H. Kirchner, ed. 1996, p. 180-195.

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

[GLM92] Gonthier G., Lévy J.-J., Melliès P.-A. An abstract Standardisation theorem. In: 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.

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

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

[HoPl91] 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, PhD thesis, MIT, 1990.

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

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

[Kha92] Khasidashvili Z. The Church-Rosser theorem in Orthogonal Combinatory Reduction Systems. Report 1825, INRIA Rocquencourt, 1992.

[KhGl96] Khasidashvili Z., Glauert J. R. W. Discrete normalization in Deterministic Residual Structures. In proc. of the 5^{th} International Conference on Algebraic and Logic Programming, ALP’96, Springer LNCS, vol. 1139, M. Hanus, M. Rodríguez-Artalejo, eds. 1996, p.135-149.

[KhGl96a] Khasidashvili Z., Glauert J. R. W. Relating conflict-free transition and event models. draft.

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

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

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

[Lan93] Laneve C. Optimality and Concurrency in Interaction Systems. Ph.D. Thesis, University of Pisa, 1993.

[Lan94] Laneve C. Distributive evaluations of λ-calculus, Fundamenta Informaticae, 20(4):333 – 352, 1994.

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

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

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

[NPW81] Nielsen M., Plotkin G., Winskel G. Petri nets, event structures and Domains. Part 1. TCS 13:85-108, 1981.

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

[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. In proc. of RTA’96, Springer LNCS, vol. 1103, Ganzinger, H., ed., 1996, p. 392–407.

[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 [ScEh94], p. 326-340.

[ScEh94] Schneider H.-J. Ehrig H., editors. Proceedings of the Dagstuhl Seminar 9301 on Graph Transformations in Computer Science, Springer LNCS, vol. 776, 1994.

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

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

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

[Win86/89] Winskel G. An introduction to Event Structures. In proc. of School/Workshop on ‘Linear time, branching time and partial order in logics and models of concurrency’. Springer LNCS, vol. 354, 1989, p. 364-397. Extended version appears as Cambridge University Computer Laboratory Report n. 95, 1986.

10 Appendix: Proof of Lemma 4.5

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

Lemma 10.1 ([GlKh96]) 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 10.2 ([KhGl96]) Let u ∈ t_{0} → →^{P} t_{k}, and let P be external to u, in a DRS. Then u ≉_{L} P.

Lemma 10.3 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 3.1, 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 10.1 that Q^{∗} = Q/v^{∗} is external to u^{∗}. Since u is u + P -needed, so is u^{∗} by Lemma 3.2.(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 10.4 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 [acyclicity], this is only possible when u = v – a contradiction.

Lemma 10.5 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 3.2.(4).

Proof of Lemma 4.5 Since P +u ≈_{S} Q+v, we have v ≈_{L} (P +u)/Q. By Lemma 10.2, (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 [acyclicity], v = u/(Q/P). Further, by Lemma 10.4, 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 10.5. 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 [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 10.3, 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 10.3 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 10.2 and Lemma 10.5 that P′/Q′ = ∅. The converse is proved similarly, so P′ ≈_{L} Q′. It follows that u = u′/v′ and v = v′/u′.