The Geometry of Conflict-free Reduction Spaces

Z. Khasidashvili and J. Glauert Technical Report SYS-C98-01

UEA Norwich, UK

The Geometry of Conflict-free Reduction Spaces

Zurab Khasidashvili^{1} NTT Basic Research Laboratories Atsugi, Kanagawa, 243-01, Japan

zurab@theory.brl.ntt.co.jp

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

Technical Report SYS-C98-01

Abstract

We investigate mutual dependencies of subexpressions of a computable expression, in orthogonal rewrite systems, and identify conditions for their independent computation, concurrently. To this end, we introduce concepts familiar from ordinary Euclidean Geometry (such as basis, projection, distance, etc.) for reduction spaces. We show how a basis at an expression can be constructed so that any reduction starting from that expression can be decomposed as the sum of its projections on the axes of the basis. To make the concepts computationally more relevant, we relativize them w.r.t. stable sets of results, (such as the set of normal forms, head-normal forms, and weak-head-normal forms, in the λ-calculus), and show that an optimal concurrent computation of an expression w.r.t. S consists of optimal computations of its S-independent subexpressions. All these results are obtained for Deterministic Family Structures, which are Abstract Reduction Systems with an axiomatized residual and family relations on redexes, and model all orthogonal rewrite systems.

An extended abstract of this paper appears in Proc. of ICALP’97 [KG97a].

\begin{matrix}c \\ ◯ \end{matrix} Z. Khasidashvili & J. Glauert, UEA Norwich, 1997

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

1 Introduction

Efficient evaluation of expressions requires concurrent evaluation of subexpressions. In computation in general, it is normal that intermediate results of computation of different subexpressions are used by other subexpressions, and contribute to creation of new computable subexpressions. In concurrent languages like the π-calculus [Mil92] this is explicitly expressed by value-passing, while in sequential languages computations in different subexpressions can only interact by common creation of new redexes. Our aim in this paper is to give a formal numerical characterization of dependencies of subexpressions of an expression (or subprograms of a modular program), and in particular to identify conditions for independent evaluation of subexpressions. Computation of different independent subexpressions can be conducted in isolation from computations elsewhere in the expression, concurrently, and the results can then be combined to yield the final result. We restrict our attention to functional languages, and consider their operational model – orthogonal rewrite systems – of which the λ-calculus [Bar84] is the prime example, although we believe that our results can be generalized to the non-orthogonal case and cover the concurrent languages as well.

The idea we want to pursue is very simple and natural, and the concepts we introduce have their counterparts in ordinary Euclidean Geometry, although there will be some differences. For expository purposes, let us assume first that the given orthogonal rewrite system is linear – there are no duplication or erasure of redexes. The main analogy is the following. In a Euclidean 3-dimensional space, one can decompose a vector as the sum of its projections on the axes X, Y and Z, which form a Euclidean basis. Similarly, we can construct a basis at any expression t, consisting of independent reductions P_{i} starting from t, such that any reduction P starting from t can be decomposed as the sum of its projections on P_{i}. The ‘sum’ operation in orthogonal rewrite systems is Lévy’s least upper bound operation P′ ⊔ P′′ in the reduction space ordered by the embedding relation P′ ⊴_{L} P′′ [Lév80]. Here P_{i} and P_{j} are independent if no finite initial parts of them can interact, i.e., by common creation of a new redex. In the bases that we construct, every reductions P_{i} is a maximal reduction internal to a redex-set U_{i} in t, i.e, P_{i} contract residuals of redexes in U_{i} and created redexes; every U_{i} is independent, i.e., no reduction internal to U_{i} can interact with a reduction internal to the complement \overline{U_{i}} of U_{i}, which consists of redexes of t not in U_{i}; U_{i} are pairwise non-overlapping, and cover all redexes of t.

Further, the distance ∥P, Q∥ between co-initial reductions P, Q is the number of their ‘different’ steps, and characterizes ‘how far apart’ the reductions have progressed. Here ‘different steps’ means that they cannot be related by the zig-zag relation [Lév80], so they are in different zig-zag families. (We recall that zig-zag is simply the transitive and symmetric closure of the residual relation on redexes with creation histories.) When both P and Q are finite, ∥P, Q∥ coincides with the minimal number of reduction steps needed to reach a common reduct from the endpoints of P and Q. This is different from the Euclidean measure of distance. For example, in the simplest case, if two vectors P^{→} and Q^{→} are orthogonal (say parallel to axes X

and Y respectively), then the distance is ∥P^{→}, Q^{→}∥ = \sqrt{|P^{→}|^{2} + |Q^{→}|^{2}}, while the distance between reductions P and Q that contract redexes in different families is ∥P, Q∥ = |P | + |Q|. However, this is because the Euclidean space is continuous and allows ‘shortcuts’. If we would allow joining of the endpoints of the vectors P^{→} and Q^{→} only by moves parallel to X and Y, then we would get the same distance measure as for reductions!

Finally, the independence degree of a redex set U of an expression t is the length of a shortest reduction P internal to U such that there is a reduction Q internal to \overline{U} that interacts with P, and is ∞ otherwise. So at least |P | number of steps can be performed in U independently from the rest of the computation, after which results of computing U and \overline{U} must be combined in order for the computation to proceed ‘as concurrently as possible’. Note that if and only if U is independent, its independence degree is ∞.

These concepts can very naturally be explained in terms of Prime Event Structures (PES) [Win89], which in the conflict-free case (in which we are interested) are simply event sets E partially ordered by a causal dependency relation ≤, such that every event e ∈ E can only dominate a finite number of others. Computations in a linear orthogonal rewrite systems R are interpreted as left-closed sets of events (i.e., closed under ≤), called configurations, in the PES E = (E, ≤) whose events correspond to (the zig-zag classes of) redexes in R. Those event sets X_{i} ⊆ E that are closed under ≥ are independent, as they correspond to independent reductions in R. Further, if {X_{i} | i ∈ I} are disjoint independent sets covering E, they form a basis for E, as for any configuration α, α = ∪_{i∈I}α ∩X_{i}. Here α ∩X_{i} is the projection of α on X_{i}, and coincides with the restriction of α to the set X_{i}^{0} of all initial (i.e., minimal w.r.t. ≤) events of X_{i}. And the set {X_{i}^{0}}_{i∈I} is an independent covering of the set of initial events of E. Further, the distance between configurations α and β is defined as the cardinality of α∪β \α∩β (as is usual for sets), and it precisely corresponds to the distance measure for reductions in linear orthogonal rewrite systems – ∥P, Q∥ = ∥α_{P} , α_{Q}∥, where α_{P} , α_{Q} are configurations corresponding to P, Q. The independence degree of a set α_{0} of initial events is the cardinality of the smallest configuration α such that there exists a configuration β not containing elements of α_{0} and an event e such that α ∪ β ∪ {e} is a configuration, while neither α ∪ {e} nor β ∪ {e} are (i.e, α and β both contribute to creation of e, and they interact to create e).

The decomposition property, which is the main goal of our study of the independence concept, immediately breaks down if one wants to decompose any reduction in a duplicating reduction system. For example, consider a λ-term v = (λx.xx)u, where u is a β-redex. Then {v} and {u} form an independent redex-covering of v as u and v cannot commonly create a new redex. And the reduction P : v→^{v}uu→^{u}ou, contracting v and then the first (from the left) residual of u is not Lévy-equivalent to u⊔v, and the reason is that P contracts only one copy of the duplicated redex u. Note here that v contains u in the argument and can duplicate it. There is no reason why we should not allow the situation when redexes in one independent set duplicate or erase redexes in another independent set. Indeed, such a restriction would yield a trivial concept of independence as in that case (in general) only redex-sets in disjoint subterms may be regarded as independent, and this would result in the loss of efficiency in concurrent evaluation of an expression (if only independent redex-sets are to be evaluated concurrently). For example, consider a rewriting system R = {f_{i}(x) → f_{i+1}(x), g_{i}(x) → g_{i+1}(x) |i = 1, …, 5}. Then in the expression f_{1}(g_{1}(x)) we could independently evaluate components f_{1}(y) and g_{1}(x), yielding f_{5}(y) and g_{5}(x), respectively, and then combine these intermediate results into the final result, f_{5}(g_{5}(x)), by substituting g_{5}(x) for y in f_{5}(y), which is ‘quicker’ then normalizing f_{1}(g_{1}(x)) in ten sequential steps.

To recover the decomposition property for duplicating (and erasing) systems, we instead restrict ourselves to complete family-reductions (up to ≈_{L}), which are multi-step reductions contracting in each multi-step an entire family of redexes [Lév78, Lév80]. Redexes in a family are redexes of ‘the same origin’, and according to Lévy’s approach to optimal evaluation, these are the redexes that must be shared in a graph implementation of the λ-calculus. Such implementations have indeed been achieved by Lamping [Lam90] and Kathail [Kat90]. Although in general there may be reductions that are not complete family-reductions and that can be decomposed w.r.t. an independent basis, there seem to be no simple characterization of such a class of decomposable reductions independent from the particular rewrite system and the particular basis involved, and we leave such a refinement of our approach for a future work. Furthermore, restriction to complete family-reductions is not a restriction from the computational point of view as such reductions can compute any kind of results one is usually interested in the theory or practice of functional programming, such as normal forms, head-normal forms, or weak-head-normal forms, in the λ-calculus. For example, reductions of term graphs [KKSV93] or directed acyclic graphs (DAGs) [Mar92] correspond exactly to complete family reductions on terms, in orthogonal term rewriting systems (while reduction of sharing-graphs correspond to complete family-reductions in the λ-calculus only up to ‘book-keeping’ steps). And restriction to complete family-reductions is inevitable when one studies an adequate simulation of term rewriting with graph rewriting [KKSV94] (although the adequacy concept in [KKSV94] does not use ‘redexfamilies’ explicitly), or simulation of a duplicating system with an affine one in general.

In order to make the introduced concepts computationally more meaningful, we relativize them w.r.t. the semantics one may be interested in. For example, in the λ-calculus, one might be interested in computing normal forms, head-normal forms, weak-head-normal forms, etc. In [GK96], we have characterized all reasonable sets of finite ‘(partial) results’ as stable sets S of terms, and have shown that (only) w.r.t. stable sets S, S-needed reductions are S-normalizing (i.e., end at a term in S if the initial term is reducible to a term in S). This allows us to ignore S-unneeded redexes, and for example, we can define P, Q to be S-independent if there is no common creation of S-needed redexes. So reductions that interact may be S-independent. This is profitable since redex sets that are not independent may become S-independent, and this allows for finer independent splitting of redex-sets of terms, implying more parallelism in the computation. And indeed, if {U_{i}}_{i∈I} is an S-independent covering of an S-normalizable term t, in a possibly duplicating and/or erasing orthogonal rewriting system, we show that an optimal S-normalizing reduction starting from t (which is an S-needed S-normalizing complete family-reduction) is the sum of S-needed complete family-reductions P_{i} internal to U_{i}. Note that the later need not be normalizing even if S is the set of normal forms, as the S-unneeded redexes in final terms of P_{i} will not be present in the final term of the sum of P_{i}.

To remain as general as possible, and at the same time to avoid syntactic structure of computable expressions (terms, graphs, etc.), which is irrelevant for our purpose, we assume that the rewrite system is given in the form of a Deterministic Family Structure, DFS [GK96]. DFSs are Abstract Rewrite Systems (ARSs) with an axiomatized residual and family relations which model all orthogonal rewriting systems and cover all existing concepts of redex-family in the literature [Lév78, Lév80, KS89, Mar92, AL94, Oos96]. Standard important results such as the Standardization and Normalization Theorems of Curry and Feys [Bar84], or Lévy’s Optimality Theorem [Lév78, Lév80], can already be proven in the framework of DFSs [GK96, KG96]. Furthermore, by using the DFS axioms alone, one can interpret DFSs into non-duplicating, also called affine, DFSs with zig-zag as the family relation, by interpreting family-reduction multi-steps in the former as reduction steps in the latter. This allows us to reduce studying the decomposition property from DFSs to affine zig-zag DFSs (AZDFSs), and this enormously simplifies the theory of independent computation and the proofs.

Most of the (remaining) technical difficulties come from the erasure of redexes in AZDFSs. To cope with the erasure problems, and to have (most of the) concepts invariant under Lévyequivalence, we work with standard reductions, which in DFSs are reductions in which later steps ‘do not erase’ the preceding ones (we forget about outside-in and left-to-right order of contraction of redexes, as there are no such concepts in DFSs, and these are actually inappropriate) [KG96]. Finally, we remark that DFSs are an important transition model on their own right, and they have been successfully used (besides proving the syntactic results mentioned above) for example in defining a Prime Event Structure [Win89] style semantics [KG97b, KG98a] and a computational semantics [Kha98] for orthogonal rewrite systems in a uniform way.

The paper is organized as follows. In the next section, we recall some theory of DFSs used in this paper. In section 3, we introduce the restriction and projection concepts, study their properties, and prove the Decomposition Theorem. In section 4, we define the geometry of orthogonal reduction spaces, and prove the Independent Decomposition Theorem. In section 5, we relativize the geometry w.r.t. stable sets of results S, and show that an optimal computation w.r.t. S can be achieved by combining optimal computations of S-independent redex-sets. Conclusions appear in section 6.

An extended abstract of this work appears as [KG97a].

2 Deterministic Residual and Family Structures

In this section, we recall some basic theory of DFSs developed in [GK96, KG96, KG97, KG98]. Our presentation here will be somewhat concise, and we refer the reader to [KG98] for more explanations and examples.

We start by introducing Abstract Reduction Systems (ARSs). We then define Deterministic Residual Structure (DRSs) which are ARSs with an axiomatized notion of residual. DFSs are then defined as DRSs with an axiomatized concept of redex-family [Lév78].

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

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. ^{2} A reduction is a sequence t→^{u_{1}}t_{2}→^{u_{2}} . . ..

Notation 2.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, write P : t → → if P may be infinite, and write P : t → → ∞ if P is infinite (i.e, of the length ω). P + Q denotes the concatenation of P and Q. u also denotes the reduction that contracts u. The final term of a finite reduction P is denoted by ft(P). Q ≤ P denotes that Q is an initial part of P. We write Q < P if Q ≤ P and Q ≠ P. If U ⊆ t, then \overline{U} will denote the complement of U, i.e., the set of redexes in t not in U.

2Klop’s ARSs [Klo92] are pairs (T er, →), and cannot distinguish transitions with the same source and target terms.

UEA Norwich, UK Technical Report SYS-C98-01

DRSs are based on a classical work by Lévy who gave an algebraic definition of an embedding relation ⊴_{L} on reductions and a concept of permutation or Lévy-equivalence, ≈_{L}, for different orthogonal rewriting systems [Lév78, BeLé79, HL91, Lév80]. Closely related transition models are Stark’s Determinate Concurrent Transition Systems (DCTSs) [Sta89] and Abstract Reduction Systems of Gonthier et al. [GLM92]. Unlike DCTSs, the residual relation in DRSs may be duplicating, and unlike ARSs of [GLM92], we do not have a nesting relation on redexes. Several refined concepts of abstract rewriting are studied in [Oos94, Mel96, Raa96]. DRS are intended to model all orthogonal term and graph rewrite systems, both first and higher-order, and other conflict-free transition systems, with a reasonable level of abstraction, while say ARSs of [GLM92] do not cover e.g., orthogonal term graph rewriting systems [KKSV94], as observed by R. Kennaway. {Zurab:Further, computations in Interaction Nets [Laf90] and cut-elimination in Proof Nets for the lightweight variant LW [GAL92] of the Unified Logic [Gir91] can also be seen as reductions in DRSs, and these systems do not require any nesting relation.}

Definition 2.3 A Deterministic Residual Structure (DRS) is a pair R = (A, /), where A is an ARS and / is a residual relation on redexes relating redexes in the source and target term of every reduction t→^{u}s ∈ A, such that for v ⊆ t, the set v/u of residuals of v under u is a set of redexes of s; a redex in s may be a residual of only one redex in t under u, and u/u = ∅. If v has more than one u-residual, then u duplicates v. If v/u = ∅, then u erases v. A redex of s which is not a residual of any v ⊆ t under u is said to be 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 ≠ ∅.

In a DRS R, the residual relation on redexes is extended to all co-initial finite reductions exactly as in syntactic orthogonal rewrite systems [HL91, Lév80, Sta89]: (P_{1} +P_{2})/Q = P_{1}/Q+ P_{2}/(Q/P_{1}) and P/(Q_{1} + Q_{2}) = (P/Q_{1})/Q_{2}, and Lévy-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 ⊴_{L} Q iff P/Q = ∅, and can show that P ≈_{L} Q iff P ⊴_{L} Q and Q ⊴_{L} P; and P ⊴_{L} Q iff Q ≈_{L} P + N for some N. The following Strong Church-Rosser property can be proved: for any co-initial finite reductions P, Q, P ⊔Q ≈_{L} Q⊔P, where P ⊔ Q = P + Q/P, and is the greatest lower bound of P and Q in the reduction space ordered by ⊴_{L}. Finally, we will need the following Cube Lemma: for any finite co-initial reductions P, Q and N, N/(P ⊔ Q) = N/(Q ⊔ P).

We remark that, for finite co-initial reductions P and Q, P/Q is defined uniquely only if we regard it as a multi-step reduction, where a multi-step contracts simultaneously (or in parallel) a set of redexes in a term (for example, U, V, V/U and U/V in the above equation can be seen as multi-steps). If we want to regard P/Q as a reduction, then it is defined uniquely only up to the particular sequentializations of the corresponding multi-steps. (However, P/Q is defined more precisely than up to ≈_{L}.) It is conventional to switch freely between multi-steps and complete developments, and this does not cause any problems for the developments in this paper. The relations ⊴_{L}, ≈_{L}, / and ⊔ are extended to co-initial possibly infinite reductions N, N′ as follows. N ⊴_{L} N′, or equivalently, N/N′ = ∅ if, for any redex v contracted in N, say N = N_{1} + v + N_{2}, v/(N′/N_{1}) = ∅; and N ≈_{L} N′ iff N ⊴_{L} N′ and N′ ⊴_{L} N. Here, for any infinite P, u/P = ∅ (called u is erased in P or u is P -erased) if u/P′ = ∅ for some finite initial part P′ of P, and P/Q is only defined for finite Q, as the reduction whose initial parts are residuals of initial parts of P under Q. Finally, if P is infinite and Q is finite, we define P ⊔ Q = Q ⊔ P = Q + P/Q; and if both P and Q are infinite, say P = u_{1} + u_{2} + … and Q = v_{1} + v_{2} + …, then P ⊔ Q = U_{1} + V_{1} + U_{2} + V_{2} + …, where U_{i} = u_{i}/(Q_{i−1}/P_{i−1}), V_{i} = v_{i}/(), and P_{i} and Q_{i} are (possibly empty) initial parts of P and Q of the length i − 1 (i = 1, 2, …).

[figure: ·; u_{1}; ·; u_{2}; ·; u_{3}; ·; u_{4}; ·]

[figure: ·; v_{1}; ·; V_{1}; U_{2}; ·; ·; ·]

[figure: ·; v_{2}; ·; ·; V_{2}; U_{3}; ·; ·]

[figure: ·; v_{3}; ·; ·; ·; V_{3}; U_{4}; ·]

It is easy to check that for example P ⊔ Q ≈_{L} Q ⊔ P for infinite reductions as well.

Definition 2.4 (1) ([GK96]) 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.

(2) ([KG97]) We call R non-duplicating or affine if its residual relation is non-duplicating (i.e., a redex may have at most one residual under contraction of another redex). Affine SDRSs will be called ASDRSs.

The essence of stability is better understood by the following lemma, which extends the [stability] axiom from one step reductions to any co-initial external reductions, that is, reductions that do not contact redexes having common residuals.

Definition 2.5 • Let u ∈ U ⊆ t and P : t → → . We call P external to U (resp. u) if P does not contract residuals of redexes in U (resp. residuals of u).

• Let P : t_{0} → →^{P_{i}} t_{i}→^{u_{i}}t_{i+1} → → and Q : t_{0} = s_{0} → →^{Q_{j}} s_{j}→^{v_{j}}s_{j+1} → → . We call P external to Q

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

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

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

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

Lemma 2.6 (Stability) Let P : t → → s be external to Q : t → → e, in an SDRS, and let P create redexes W ⊆ s. Then the residuals W/(Q/P) of redexes in W are created by P/Q, and Q/P is external to W.

Similarly, the following lemma extends the [weak acyclicity] axiom to many-step external reductions:

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

We refer to [GK96, KG98] for proofs of Stability and Weak Acyclicity Lemmas.

Next we recall an axiomatization of Lévy’s concept of redex-family for DRSs. All family and sharing concepts for orthogonal reduction systems known to us (such as [Lév78, Lév80, KS89, Mar92, AL94, Oos96]) satisfy our family axioms, which allow for abstract non-trivial proofs of Relative Normalization and Optimality Theorems [GK96].

Definition 2.8 A Deterministic Family Structure (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 if P ⊴_{L} Q, i.e., P + Q/P ≈_{L} Q, and v is a Q/P - residual of u; the zig-zag relation ≃_{z} is the symmetric and transitive closure of the copy relation. The family relation ≃ is an equivalence relation among redexes with histories containing ≃_{z}. A family is an equivalence class of the family relation; families are ranged over by ϕ, ψ, . . .. F am( ) denotes the family of its argument.

(2) Further, ≃ and ↪ satisfy the following axioms (where FFD stands for Finite Family Developments):

• [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] Any reduction that contracts redexes of a finite number of families is terminating.

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]).

Definition 2.9 • We call a DFS F a zig-zag DFS, ZDFS, if its family relation is the zig-zag ≃_{z}. Affine ZDFSs will be called AZDFSs.

• We call an affine DFS separable if, for any redex P v, v cannot create two different redexes in the same family, i.e., if v creates w′, w′′ and w′ ≠ w′′, then F am((P +v)w′) ≠ F am((P +v)w′′).

As already mentioned in the introduction, DFSs can be interpreted into AZDFSs. Since this interpretation allows us to restrict our investigation into the independence concept to AZDFSs, we will now give a precise definition. We recall first that a family-reduction is a multi-step reduction contracting in each multi-step a set of redexes in a single family; and a familyreduction is complete if each multi-step contracts all redexes in a single family [Lév80].

Convention Below we assume that the term set of any DRS is the reduction graph of a term, called the initial term, t_{∅} (i.e., the set of terms consists of the reducts of t_{∅}). Further, in DFSs, families will always be considered relative to the initial term, i.e., all histories start with t_{∅}.

Definition 2.10 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 complete family-reductions starting from t_{∅}, 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 complete 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).

The proof of the fact that F_{I} is an AZDFS is long and non-trivial; it constitutes the second half of [KG98], and the details can also be found in [KG97c]. The proof consists of several stages, and is based on an extraction algorithm in ASDRSs, which transforms any redex P v into an extraction normal form P′v′ by omitting all steps in P which ‘do not contribute’ to the creation of v, where the contribution relation on redexes is derived from the contribution relation on families (axiomatized in DFSs). The properties of the extraction procedure and extraction normal forms is summarized in the following theorem [KG97, KG97c, KG98]; it uses a concept of standard reduction to be defined in subsection 3.1:

Theorem 2.11 (Affine Extraction) Every redex P v in an ASDRS R has a zig-zag related redex P′v′ in canonical form, meaning that P′ is standard, its last step creates v′, and for any P′′v′′ ≃_{z} P v, there is N′ such that P′′ ≈_{L} P′ + N′ and v′′ = v′/N. For any other canonical form P^{∗}v^{∗} of P v, P′ ≈_{L} P^{∗} and v′ = v^{∗}.

We furthermore prove that extraction is adequate for zig-zag, i.e., P v ≃_{z} Qu iff there canonical forms are the same (modulo ≈_{L}-equivalence on standard histories), and this allows us to show that ASDRSs, AZDFSs and affine separable DFSs are equivalent transition models:

Theorem 2.12 (Affine Families) Let R be an ASDRS. Then F_{R} = (R, ≃_{z}, ↪_{z}) is an affine zig-zag DFS, called the corresponding ZDFS of R, and both ≃_{z} and ↪_{z} are decidable. Further, F_{R} is the only separable DFS with R as the underlying SDRS, and in general, an affine DFS is separable iff it is a zig-zag DFS.

Finally, given a DFS F, we show that F_{I} is an affine DFS by verifying all DFS axioms for F_{I}. In particular, the following lemma implies that the residual relation on F_{I} is well defined:

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

Moreover, we show that F_{I} is separable, thus it is a AZDFS by Theorem 2.12:

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

Remark 2.15 Note that there is actually an isomorphism between complete family-reductions in F and reductions in F_{I}. Thus all definitions and results in this paper concerning reductions in ASDRSs can be read as definitions or results concerning complete family-reductions in arbitrary DFSs.

3 Decomposition of Reductions in ASDRSs

In this section, we define projection of a reduction onto another one, and its restriction to a redex-set, study their properties, and use them to decompose reductions as the sum of their restrictions to non-overlapping redex sets. The projection concept is based on a relative standardization algorithm.

3.1 Relative Standardization

In this subsection, we define a somewhat non-standard concept of standardization. Firstly, our standard reductions are whose in which later steps ‘do not erase’ preceding ones. in DFSs we cannot define a ‘left-to-right’ and/or ‘outside-in’ concept of standard reduction familiar from the λ-calculus and orthogonal rewriting systems [Bar84, HL91, Klo80], but we do not need such a standardization concept either. Secondly, we define a relativized standardization algorithm which standardizes any reduction Q in an ASDRS w.r.t. any other, co-initial with Q, reduction P.

Definition 3.1 ([KG96]) • Let P : t → → and u ⊆ t. We call u P -needed if there is no Q ≈_{L} P that is external to u, and call it P -unneeded otherwise.

• Let Q : t → → , P : t → →^{P′} s → → , and u ⊆ s. We call u (or rather P′u) 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 or standard if it is P -needed. We write Q ≈_{ST A} P if Q ≈_{L} P and Q, P ∈ ST A, where ST A denotes the set of all standard reductions. We call N a standard variant of P if P ≈_{L} N and N ∈ ST A.

Note that P -neededness does not depend on the choice of a reduction in the class of reductions Lévy-equivalent to P, since u/P = u/Q when P ≈_{L} Q, by the Cube Lemma.

The following definition gives a relative standardization algorithm for reductions in ASDRSs.

Definition 3.2 ([KG96]) Let P, Q : t → → . The canonical P -needed variant of Q, written ST_{P} (Q), is defined as follows: let v ⊆ t be such that it is P -needed and its residual is contracted in Q first among P -needed residuals of P -needed redexes in t (note that v need not be Q-needed). Then ST_{P} (Q) = v + ST_{P/v}(Q/v). If there is no such a redex in t, then ST_{P} (Q) = ∅.

If Q = P, then we refer to the above algorithm as the standardization algorithm; we will write ST (Q) for ST_{Q}(Q), and call ST (Q) the canonical standard variant of Q.

The main result of this subsection is the Relative Standardization Theorem (Theorem 3.8). To prove it, we need a few simple lemmas.

Lemma 3.3 If u⊴_{L}P ⊴_{L}Q and u is Q-needed, in an ASDRS, then it is P -needed. Consequently, if P is Q-needed, then it is standard.

Proof Suppose on the contrary that u is P -unneeded, i.e, there is P′ ≈_{L} P that is external to u. Since u is P -erased, P′ discards u, hence there is a finite initial part P′′ of P′ that discards u. But Q ≈_{L} P′′ + Q′′ for some Q′′, contradicting Q-neededness of u. Thus u is P -needed, and the rest is immediate from Definition 3.1.

Lemma 3.4 Let P : s → → s′→^{w}o, in an SDRS. Then w ∈ s′ is P -needed.

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

Lemma 3.5 Let P v ≃_{z} Qw, in an ASDRS. Then v/(Q/P) = w/(P/Q).

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

Lemma 3.6 Let t→^{u}s, P : t → → , and v′ = v/u, in an ASDRS. Then, if v is P -unneeded, so is v′. If moreover u ⊴_{L} P, then the converse is also true.

Proof Let Q : t_{∅} → → t. Since v is P -unneeded, there is P^{∗} ≈_{L} P that is external to v. If on the contrary v′ was P -needed, P^{∗}/u would contract a residual v′′ of v′, and P^{∗} would contract a redex v^{∗}, say P^{∗} = P_{1}^{∗} + v^{∗} + P_{2}^{∗}, such that (Q + P_{1}^{∗})v^{∗} ≃_{z} Qv, implying by Lemma 3.5 that P^{∗} contracts a residual v^{∗} of v – a contradiction.

[figure: t_{∅}; Q; t; P_{1}^{∗}; ·; v^{∗}; ·; P_{2}^{∗}; ·; s; u; ·; v′′; ·; ·]

Now let u⊴_{L}P and let v′ be P -unneeded. If on the contrary v was P -needed, for any N ≈_{L} P/u, u + N would contract a residual of v (since u + N ≈_{L} P), thus N would contract a residual of v′, implying P -neededness of v′ – a contradiction.

Note that without the condition u ⊴_{L} P the converse of the above lemma is not valid: Let t = u = (λx.w)v and P = v ⊔ w, where w = Kyx and K = λx.λy.x. Then v is P -needed,

P/u : Kyv′→^{v′}Kyo→^{K}y, and v′ is P/u-unneeded.

Lemma 3.7 Let t→^{u}s, P : t → → , let u create v ⊆ s, and let u be P -unneeded, in an ASDRS R. Then, v is P -unneeded too. (Note that u ⊴_{L} P is not assumed.)

Proof Let Q : t_{∅} → → t. Let P^{∗} ≈_{L} P be external to u. If on the contrary v was P -needed, P^{∗}/u would contract a residual v′′ of v, hence P^{∗} would contact a redex v^{∗}, say P^{∗} = P_{1}^{∗} + v^{∗} + P_{2}^{∗}, such that (Q + P_{1}^{∗})v^{∗} ≃_{z} (Q + u)v (see the diagram for Lemma 3.6). Since P^{∗} is external to u, by Lemma 3.5 it does not contract redexes in the family of Qu (i.e., for any w contracted in P^{∗}, say P^{∗} = P′ + w + P′′, (Q + P′)w ≄_{z} Qu), contradicting [creation] (as R is a zig-zag DFS by Theorem 2.12).

Theorem 3.8 (Relative Standardization) (1) For any co-initial reductions Q, P, finite or infinite, in an ASDRS, ST_{P} (Q) is a P -needed, standard, reduction whose length coincides with the number of P -needed steps in Q, and ST_{P} (Q) ⊴_{L} Q, P.

(2) Further, if Q is finite, then Q ≈_{L} ST (Q); otherwise, Q ≈_{L} ST (Q) need not hold.

Proof (1) Let Q : t = t_{0} → →^{Q_{i}} t_{i}→^{u_{i}}t_{i+1} → →^{Q_{i+1}^{∗}} , and let u_{i_{0}}, u_{i_{1}}, … be all the P -needed steps in Q (i_{0} < i_{1} < …). Since u_{i_{0}} is the first P -needed step in Q, it follows from Lemmas 3.6 and 3.7 that u_{i_{0}} is (the only) residual of some P -needed redex v_{0} ⊆ t_{0}. Hence v_{0} is P -erased. Thus ST_{P} (Q) = v_{0} + ST_{P/v_{0}}(Q/v_{0}) where v_{0} is P -needed and v_{0} ⊴_{L} P, Q. Similarly, we show that

SE_{P} (Q) : t_{0} = s_{0}→^{v_{0}}s_{1}→^{v_{1}}s_{2} → → , where u_{i_{j}} is the first P′_{j}-needed step in Q′_{j} = Q/(v_{0} + v_{1} + … +

v_{j−1}), where P′_{j} = P/(v_{0} + v_{1} + … + v_{j−1}), and u_{i_{j}} is the only residual of some P′_{j}-needed, thus P′_{j}-erased, redex v_{j} ∈ s_{j} along Q′_{j} (see the figure). Hence ST_{P} (Q) ⊴_{L} P, Q and is P -needed, thus is standard by Lemma 3.3.

[figure: t_{0} = s_{0}; Q_{i_{j}}; t_{i_{j}}; u_{i_{j}}; t_{i_{j}+1}; Q_{i_{j}+1}^{∗}; Q′_{0} = Q]

[figure: s_{j}; t_{i_{j}}; ∅; u_{i_{j}}; t_{i_{j}+1}; Q_{i_{j}+1}^{∗}; Q′_{j}]

[figure: s_{j+1}; v_{j}; t_{i_{j}}; u_{i_{j}}; ∅; t_{i_{j}+1}; ∅; Q_{i_{j}+1}^{∗}; Q′_{j+1}]
v_{j+1}^{}

(2) By (1), ST (Q) ⊴_{L} Q. If on the contrary Q/ST (Q) ≠ ∅, it should contract at least one Q/ST (Q)-needed redex by Lemma 3.4, contradicting the standardization algorithm.

Now consider the OTRS R = {r_{1} : f(x) → g(h(x)), r_{2} : g(x) → f(h(x)), r_{3} : h(x) → a} and the reductions Q : f(x) → g(h(x)) → g(a) → f(h(a)) → f(a) → g(h(a)) → g(a) → … and Q′ : f(x) → g(h(x)) → f(h(h(x))) → g(h(h(h(x)))) → . . .. Then it is easy to check that Q′ = ST (Q), but Q/Q′ ≠ ∅.

It has been shown in [KG97] that, in ASDRSs, all standard variants of a finite reduction P can be constructed effectively (as P -neededness is decidable and there are only a finite number of such reductions, all of the same length), and that ≈_{ST A} is decidable. So finite standard reductions can be used as canonical representatives of their Lévy-equivalence classes (which may have an infinite number of elements). This is no longer true for infinite reductions in general, and we need to be careful in our proofs when considering standard variants of infinite reductions. Such problems do not arise, however, when one restricts to strongly convergent infinite reductions [KKSV95, Ken96], but we want to be as general as possible in this paper.

3.2 Characterizing relative standardization using families

In this subsection, we first give a characterization of ⊴_{L} and ≈_{L} in ASDRSs via families of contracted redexes in corresponding reductions, and use it to give a similar characterization for the relative standardization concept. These characterizations significantly simplify our proof of the Decomposition Theorem – the main result of this section.

Notation 3.9 Below, F AM(P) (resp. SF AM(P)) denotes the set of families whose member (resp. P -needed) redexes are contracted in P, in a DFS. (When we speak of families in an ASDRS, we always mean zig-zag families of the corresponding AZDFS.)

Lemma 3.10 Let P and Q be standard co-initial reductions. Then P ≈_{L} Q iff F AM(P) = F AM(Q).

Proof

(⇒) Let v be a contracted redex in P, say P = P′ + v + P′′. Then v is Q/P′-needed. Hence F AM(P′v) ∈ F AM(Q/P′) ⊆ F AM(Q), and the converse is proved similarly.

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

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

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

Q′′^{}

Lemma 3.11 Let P be a reduction in an ASDRS. Then SF AM(P) = F AM(ST (P)).

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

…). Then, by Definition 3.2, ST (P) : t_{0} = s_{0}→^{v_{0}}s_{1}→^{v_{1}}s_{2}→^{u_{2}} …, 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(v_{j}) = F AM(u_{i_{j}}), and the lemma follows (since SF AM(P) = {F AM(u_{i_{j}}) | j = 0, 1, …, k} and F AM(ST (P)) = {F AM(v_{j}) | j = 0, 1, …, k}).

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

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

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

Lemma 3.12 Let P ≈_{L} Q, in an ASDRS. Then SF AM(P) = SF AM(Q) and ST (P) ≈_{ST A} ST (Q).

Proof Let P′u ∈ SF AM(P). Then u is Q/P′-needed, thus it has a residual Q^{∗}v^{∗} contracted in Q/P, implying that there is a redex Q′v contracted in Q such that v^{∗} = v/(P′/Q′). By Lemma 3.6, v is Q-needed, implying that F AM(Q′v) = F AM(P′u) ∈ SF AM(Q). Thus SF AM(P) = SF AM(Q). The rest is immediate by Lemmas 3.10 and 3.11 (since ST (P) and ST (Q) are standard by Theorem 3.8).

The following proposition summarises our characterization of ⊴_{L} and ≈_{L} vis zig-zag families:

Proposition 3.13 Let P and Q be co-initial reductions in an AZDFS. Then

(1) If F AM(P) ⊆ F AM(Q), then P ⊴_{L} Q.

(2) if P, Q ∈ ST A, then P ≈_{L} Q iff F AM(P) = F AM(Q).

(3) If P ≈_{L} Q, then SF AM(P) = SF AM(Q). If moreover both P and Q are finite, then the converse is also true.

Proof (1) We need to show that, for any redex v contracted in P, say P = P′ + v + P′′, v/(Q/P′) = ∅. Since F AM(P) ⊆ F AM(Q), Q contracts a redex Q′w zig-zag related to P′v, and we have by Lemma 3.5 that v/((Q′ + w)/P′) = ∅, thus v/(Q/P′) = ∅.

(2) By Lemma 3.10.

(3) By Lemma 3.12, we only need to show that, if P and Q are finite and SF AM(P) = SF AM(Q), then P ≈_{L} Q. By Lemma 3.11, F AM(ST (P)) = F AM(ST (Q)), implying ST (P) ≈_{ST A} ST (Q) by Theorem 3.8 and (2). But P ≈_{L} ST (P) and Q ≈_{L} ST (Q) by Theorem 3.8, and (3) follows.

3.3 The Projection Concept

Now we define the projection concept and show it is invariant under ≈_{L}.

Definition 3.14 We call ST_{P} (ST (Q)) the projection of Q onto P, written Q|P.

Lemma 3.15 Let P, Q be co-initial (not necessarily finite) reductions in an ASDRS. Then (1) F AM(ST_{P} (Q)) = SF AM(ST_{P} (Q)) = F AM(Q) ∩ SF AM(P);

(2) If moreover Q ⊴_{L} P or Q ∈ ST A, then (S)F AM(ST_{P} (Q)) = (S)F AM(Q) ∩ SF AM(P). Proof Let Q : t_{0}→^{u_{0}}t_{1}→^{u_{1}} → …, and let u_{i_{0}}, u_{i_{1}}, … be all P -needed steps in Q.

(1) It is enough to show that ST_{P} (Q) = t_{0} = s_{0}→^{u′_{0}}s_{1}→^{u′_{1}} …, where Q_{i_{k}}u_{i_{k}} ≃_{z} Q′_{k}u′_{k} and Q_{i_{k}}

and Q′_{k} are the corresponding initial parts of Q and ST_{P} (Q), respectively. Assume that indeed

Q′_{m} : t_{0} = s_{0}→^{u′_{0}}s_{1}→^{u′_{1}} … →^{u′_{m−1}}s_{m}, where Q_{i_{k}}u_{i_{k}} ≃_{z} Q′_{k}u′_{k} for all 0 ≤ k < m. Since F AM(Q′_{m}) ⊆

F AM(Q_{i_{m}}), we have by Proposition 3.13 that Q′_{m} ⊴_{L} Q_{i_{m}}. Hence u_{i_{m}} ⊆ ft(Q_{i_{m}}/Q′_{m}). By Lemma 3.6, Q_{i_{m}}/Q′_{m} is P -unneeded, hence it cannot create u_{i_{m}} by Lemma 3.7, i.e., u_{i_{m}} = u′_{m}/(Q_{i_{m}}/Q′_{m}) for some u′_{m} ⊆ s_{m}. Now, by the definition of ST_{P} (Q), u′_{m} is its m + 1-st step, and Q_{i_{m}}u_{i_{m}} ≃_{z} Q′_{m}u′_{m}, implying (by induction) that F AM(ST_{P} (Q)) = F AM(Q)∩SF AM(P). Note that SF AM(ST_{P} (Q)) = F AM(ST_{P} (Q)) since ST_{P} (Q) is standard by Theorem 3.8, and (1) follows.

[figure: t_{0} = s_{0}; Q_{i_{m}}; t_{i_{m}}; u_{i_{m}}]

[figure: s_{m}; Q′_{m}; Q_{i_{m}}/Q′_{m}; ∅; u_{i_{m}}]
[figure: s_{m+1}; u′_{m}; ∅; ∅]

(2) If Q ⊴_{L} P, SF AM(Q) ∩ SF AM(P) = F AM(Q) ∩ SF AM(P) since P -needed redexes of Q are Q-needed by Lemma 3.3; and if Q ∈ ST A, F AM(Q) = SF AM(Q) by Proposition 3.13;

(2) follows.

The next example shows that the requirement that Q ⊴_{L} P or Q ∈ ST A, in the above lemma, is necessary for SF AM(ST_{P} (Q)) = SF AM(Q) ∩ SF AM(P) to hold.

Example 3.16 Let P = u and Q = u + v, where u is Q-unneeded. Then Q is not standard, and Q ⋬_{L}P. Further, ST_{P} (Q) = u, F AM(ST_{P} (Q)) = F AM(Q) ∩ SF AM(P) = F am(u), but SF AM(Q) ∩ SF AM(P) = F am(uv) ∩ F am(u) = ∅.

Corollary 3.17 Let P, Q be co-initial (not necessarily finite) reductions in an ASDRS. Then F AM(P |Q) = SF AM(P |Q) = SF AM(Q) ∩ SF AM(P).

Lemma 3.18 Let P, P′ : t → → , Q, Q′ : t → → , P ≈_{L} P′, Q ≈_{L} Q′, and Q⊴_{L}P or Q, Q′ ∈ ST A, in an ASDRS. Then ST_{P} (Q) ≈_{ST A} ST_{P′}(Q′). Proof We have SF AM(ST_{P} (Q)) = SF AM(Q) ∩ SF AM(P) = SF AM(Q′) ∩ SF AM(P′) = SF AM(ST_{P′}(Q′)) by Lemma 3.15 and Proposition 3.13, implying by Proposition 3.13 that ST_{P} (Q) ≈_{L} ST_{P′}(Q′). By Theorem 3.8, both reductions are standard, hence ST_{P} (Q) ≈_{ST A} ST_{P′}(Q′).

Corollary 3.19 The projection concept is invariant under ≈_{L}.

Note that, if we had defined Q|P as ST_{P} (Q) rather than ST_{P} (ST (Q)), the above corollary would fail: just take P and Q as in Example 3.16, and take Q′ = v′ where v = v′/u. Then Q ≈_{L} Q′, Q|P = u, but Q′|P = ∅.

3.4 The Restriction Concept

We start with a simple definition.

Definition 3.20 Let P : t → → be a reduction in a DRS, and let U ⊆ t be a set of redexes in t. We call P internal to U or a U-reduction if it is external to \overline{U}, that is, if it contracts residuals of redexes in U and created redexes. We call such redexes U-redexes.

Definition 3.21 (Restrictions of reductions to redex-sets) (1) Let t be a term in an ASDRS R, let U ⊆ t, and let P : t → → s be standard. The concepts P respects U and the restriction of P to U, written P |U, are defined by induction on n = |P | as follows. If n = 0, then P respects U and P |U = ∅. Now let P = P′ + v and let P′ respect U. Assume that P′|U and P′|\overline{U} are defined as reductions internal to U and \overline{U}, respectively, such that P′ ≈_{ST A} P′|U ⊔P′|\overline{U}. Then we say that P respects U if either v = v′/(P′|\overline{U}/P′|U) for v′ ⊆ ft(P′|U) such that (P′|U) + v′ is still internal to U, or v = v′/(P′|U/P′|\overline{U}) for v′ ⊆ ft(P′|\overline{U}) such that (P′|\overline{U}) + v′ is still internal to \overline{U}. In the first case (depicted on the picture below), we define P |U = P′|U +v′ and P |\overline{U} = P′|\overline{U}, and define P |U = P′|U and P |\overline{U} = P′|\overline{U} + v′ in the second case.

[figure: P′|U; v′; e]
[figure: P′]
[figure: P′|\overline{U}; P′|U/P′|\overline{U}; P′|\overline{U}/P′|U; v]

(2) We say that a finite reduction Q respects U if so does ST (Q), and define Q|U = ST (Q)|U. We say that Q respects ℑ = {U_{i}}_{i∈I} if it respects every U_{i}.

The intuition is that, Q respects U iff ST (Q) contracts only redexes to which either only redexes in U contribute, or only those in \overline{U}, but not redexes in both U and \overline{U}. This intuition will be made precise in Lemma 3.24 below. Clearly, Q-respects U iff it respects \overline{U}.

In the above definition, we need to take a standard variant of Q before restricting it to U to ensure that the restriction notion is invariant under Lévy-equivalence. As shown by the following simple example, this is necessary. Let R = {f(x) → a, g(x) → x}, let P : f(g(x))→^{v}f(x)→^{u}a, and let U = {v}. Then ‘direct restriction’ of P to U is v, while P |U = ST (P)|U = ∅, and v ≉_{L} ∅.

Lemma 3.22 Definition 3.21 is correct, that is, ST (P) ≈_{ST A} P |U ⊔ P |\overline{U}. (Hence, P |U is P -needed.)

Proof Suppose that P = P′ + v respects U and that v = v′/(P′|\overline{U}/P′|U) for v′ ⊆ ft(P′|U) such that (P′|U) + v′ is internal to U. Then P = P′ + v ≈_{ST A} (P′|U ⊔ P′|\overline{U}) + v = P′|U + P′|\overline{U}/(P′|U) + v ≈_{L} P′|U + v′ + P′|\overline{U}/(P′|U + v′) = P |U + P |\overline{U}/(P |U) = P |U ⊔ P |\overline{U}. The case when v = v′/(P′|U/P′|\overline{U}) for v′ ⊆ ft(P′|\overline{U}) such that (P′|\overline{U}) + v′ is internal to \overline{U} is similar. By Lemma 3.6, P |U and P |\overline{U} are P -needed, and so is P |U ⊔ P |\overline{U}, i.e, P |U ⊔ P |\overline{U} is standard, and the lemma follows. \{Zurab:Finally, P |U and P |U ⊔ P |\overline{U} are P -needed, hence standard, by Lemma 3.6 and Lemma 3.3.} As for the projection concept, we need to give a characterization of the restriction concept via families in order to allow for simpler proofs in the sequel.

Notation 3.23 Below, for any U ⊆ t_{∅} in a DFS, F AM_{0}(U) will denote the set of families (relative to t_{∅}) of redexes in U, and F AM^{+}(U) will denote the minimal set of families containing F AM_{0}(U) and closed under the contribution relation ↪_{z}.

Lemma 3.24 Let U ⊆ t and P : t → → s, in an ASDRS. Then P respects U iff SF AM(P) ⊆ F AM^{+}(U) ∪ F AM^{+}(\overline{U}). In the latter case, SF AM(P |U) = F AM(P |U) = SF AM(P) ∩ F AM^{+}(U) and SF AM(P) = F AM(P |U) ∪ F AM(P |\overline{U}).

Proof By Proposition 3.13 and Definition 3.21, we can assume that P ∈ ST A. The first part is proved by induction on |P | by simply using Definition 3.21. That P |U and P |\overline{U} are standard follow from Lemma 3.22. F AM(P |U) = F AM(P) ∩ F AM^{+}(U) and F AM(P) = F AM(P |U) ∪ F AM(P |\overline{U}) also follow immediately from Definition 3.21 by induction on |P |, since P, P |U ∈ ST A.

Lemma 3.25 If P respects U and Q ≈_{L} P, in an ASDRS, then so does Q, and P |U ≈_{ST A} Q|U.

Proof By Lemma 3.24 and Proposition 3.13.

The restriction concept enjoys nice algebraic properties:

Lemma 3.26 Let P : t → → s respect U_{1}, U_{2} ⊆ t. Then

(1) P respects U_{1} ∪ U_{2} and P |U_{1} ∪ U_{2} ≈_{ST A} P |U_{1} ⊔ P |U_{2};

(2) P respects U_{1} ∩ U_{2}, P |U_{1} respects U_{2}, and P |U_{1} ∩ U_{2} ≈_{ST A} (P |U_{1})|U_{2}.

(3) P respects U_{1} \ U_{2}, P |U_{1} respects \overline{U_{2}}, and P |U_{1} \ U_{2} ≈_{ST A} (P |U_{1})|\overline{U_{2}}.

Proof We can assume that P is standard.

(1) Since P respects U_{i}, we have by Lemma 3.24 that ∀ϕ ∈ F AM(P) : ϕ ∈ F AM^{+}(U_{i}) ∨ F AM^{+}(\overline{U_{i}}). In each of the four cases, ϕ ∈ F AM^{+}(U_{1} ∪ U_{2}) or ϕ ∈ F AM^{+}(\overline{U_{1} ∪ U_{2}}), implying by Lemma 3.24 that P respects U_{1} ∪ U_{2}. (For example, if ϕ ∈ F AM^{+}(U_{1}) and ϕ ∈ F AM^{+}(\overline{U_{2}}), then ϕ ∈ F AM^{+}(U_{1} \ U_{2}), hence ϕ ∈ F AM^{+}(U_{1} ∪ U_{2}).) Since P |U_{i} ⊴_{L} P and are P -needed, P |U_{1} ⊔ P |U_{2} ⊴_{L} P and is P -needed too, and therefore standard, by Lemma 3.3 and Lemma 3.6. Thus F AM(P |U_{1}) ∪ F AM(P |U_{2}) = F AM(P |U_{1} ⊔ P |U_{2}). If there was a family ψ ∈ F AM(P) ∩ (F AM^{+}(U_{1} ∪ U_{2}) \ (F AM^{+}(U_{1}) ∪ F AM^{+}(U_{2}))), then there would be ψ_{1}, ψ_{2} ↪_{z} ψ such that ψ_{1} ∈ U_{1} and ψ_{2} ∈ U_{2} \U_{1} ⊆ \overline{U_{1}}, which is impossible by Lemma 3.24 since P respects U_{1}. So F AM(P |U_{1} ∪ U_{2}) ⊆ F AM(P |U_{1}) ∪ F AM(P |U_{2}) = F AM(P |U_{1} ⊔ P |U_{2}), implying by Proposition 3.13 that P |U_{1} ∪ U_{2} ≈_{ST A} P |U_{1} ⊔ P |U_{2} (since P |U_{1} ∪ U_{2}) is standard by Lemma 3.22).

(2) Clearly, \overline{U_{1} ∩ U_{2}} = \overline{U_{1}} ∪ \overline{U_{2}}, hence P respects U_{1} ∩ U_{2} (and \overline{U_{1} ∩ U_{2}}) by (1). Further, since P ≈_{ST A} P |(U_{1} ∪ \overline{U_{1}}) ≈_{ST A} P |U_{1} ⊔ P |\overline{U_{1}} by (1) and P respects U_{2}, P |U_{1} also respects U_{2} by Lemma 3.25. Finally, we have by Lemma 3.24 that SF AM(P |U_{1} ∩ U_{2}) = SF AM(P) ∩ F AM^{+}(U_{1} ∩ U_{2}) = SF AM(P) ∩ F AM^{+}(U_{1}) ∩ F AM^{+}(U_{2}) = SF AM(P |U_{1}) ∩ F AM^{+}(U_{2}) = SF AM((P |U_{1})|U_{2}), implying P |U_{1} ∩ U_{2} ≈_{ST A} (P |U_{1})|U_{2} by Proposition 3.13 and Lemma 3.22.

(3) By (1) and (2), since U_{1} \ U_{2} = U_{1} ∩ \overline{U_{2}}.

3.5 The Decomposition Theorem

Lemma 3.27 If Q|P is finite, then so is P |Q, and P |Q ≈_{ST A} Q|P.

Proof Immediate from Corollary 3.17 and Proposition 3.13.

The following lemma relates the restriction and projection concepts.

Lemma 3.28 Let U ⊆ t, in an ASDRS, and let P and \overline{P} be finite reductions internal to U and \overline{U}, respectively. Then P ⊔ \overline{P} respects U and (P ⊔ \overline{P})|U ≈_{ST A} (P ⊔ \overline{P})|P ≈_{ST A} P |(P ⊔ \overline{P}).

Proof We have by Lemma 3.24 and Lemma 3.15 that SF AM((P ⊔ \overline{P})|U) = SF AM(P ⊔ \overline{P}) ∩ F AM^{+}(U) = (by Definition 3.2, since \overline{P} is external to U) SF AM(ST_{P ⊔\overline{P}} (P)) = SF AM(P |P ⊔ \overline{P}). Now the lemma follows from Lemma 3.27 and Proposition 3.13.

Definition 3.29 Let U_{i} with i ∈ I be nonempty sets of redexes in t such that ∪_{i∈I}U_{i} contains each redex of t and U_{i} ∩U_{j} = ∅ when i ≠ j. Then we call the set ℑ = {U_{i}}_{i∈I} a (redex-)covering of t.

We can now prove the main result of this section.

Theorem 3.30 Let ℑ = {U_{i}}_{i∈I} be a redex-covering of a term t in an ASDRS R.

(1) Let P_{i} be finite reductions internal to U_{i}, and let P = ⊔_{i}P_{i}. Then P respects ℑ and P |U_{i} ≈_{ST A} P |P_{i}.

(2) Let P : t → → s respect ℑ. Then P ≈_{L} ⊔_{i}P |U_{i}.

Proof (1) Let \overline{P_{i}} = ⊔_{j≠i}P_{j} (i ∈ I). Then P ≈_{L} P_{i} ⊔ \overline{P_{i}} and \overline{P_{i}} is internal to \overline{U_{i}}. Hence, by Lemma 3.28 and Lemma 3.25, P respects U_{i}, thus P respects ℑ, and P |U_{i} ≈_{ST A} P |P_{i}.

(2) Let I = {1, …, n}. Then, since P respects ℑ, we have by Lemma 3.26.(1) that P ≈_{L} P |(U_{1} ∪ … ∪ U_{n}) ≈_{L} P |U_{1} ⊔ P |(U_{2} ∪ … ∪ U_{n}) ≈_{L} … ≈_{L} P |U_{1} ⊔ … ⊔ P |U_{n}.

Now, Remark 2.15 allows us to derive a counterpart of Theorem 3.30 for DFSs in general. Let us take a closer look say at the definition of the restriction concept, and spell out explicitly the corresponding definition for DFSs.

Definition 3.31 (Restrictions of reductions to redex-sets) (1) Let t be a term in a DFS F, let U ⊆ t, and let P : t → → s be standard complete family-reduction. The concepts P respects U and the restriction of P to U, written P |U, are defined by induction on the number n of multi-steps in P as follows. If n = 0, then P respects U and P |U = ∅. Now let P = P′ +V and let P′ respect U. Assume that P′|U and P′|\overline{U} are defined as complete family-reductions internal to U and \overline{U}, respectively, such that P′ ≈_{ST A} P′|U ⊔P′|\overline{U}. Then we say that P respects U if either V = V′/(P′|\overline{U}/P′|U) for V′ ⊆ ft(P′|U) such that (P′|U) + V′ is still internal to U, or V = V′/(P′|U/P′|\overline{U}) for V′ ⊆ ft(P′|\overline{U}) such that (P′|\overline{U}) + V′ is still internal to \overline{U}, where V′ is the maximal set of redexes in ft(P′|U) that belong to the family of P′v, v ∈ V. In the first case (depicted on the picture below), we define P |U = P′|U + V′ and P |\overline{U} = P′|\overline{U}, and define P |U = P′|U and P |\overline{U} = P′|\overline{U} + V′ in the second case.

[figure: P′|U; V′; e]
[figure: P′]
[figure: P′|\overline{U}; P′|U/P′|\overline{U}; P′|\overline{U}/P′|U; V]

(2) We say that a finite complete family-reduction Q respects U if so does ST (Q), and define Q|U = ST (Q)|U. We say that Q respects ℑ = {U_{i}}_{i∈I} if it respects every U_{i}.

In the above definition, a complete family-reduction P is standard if every multi-step in P is P -needed, i.e., contracts at least one P -needed redex. And when standardizing complete family-reductions, entire multi-steps are swapped. Lemma 2.13 insures that this can be done ‘safely’. (Clearly, a sequentialization of a standard multi-step reduction need not be a standard reduction.) The meanings of ST ( ) and ≈_{ST A} for multi-step reductions change respectively. Again from Lemma 2.13 we know that, in the above definition, it is correct to take for V′ the set of all redexes in ft(P′|U) in the family of V as such a V′ is a (complete) family multi-step.

Corollary 3.32 (Decomposition Theorem) Let ℑ = {U_{i}}_{i∈I} be a redex-covering of a term t in a DFS F.

(1) Let P_{i} be finite complete family-reductions internal to U_{i}, and let P = ⊔_{i}P_{i}. Then P respects ℑ and P |U_{i} ≈_{ST A} P |P_{i}.

(2) Let P : t → → s be a complete family-reduction that respect ℑ. Then P ≈_{L} ⊔_{i}P |U_{i}.

4 The Geometry of Conflict-free Reduction Spaces

In this section, we introduce the Reduction Geometry and prove the Independent Decomposition Theorem, which reflects the main analogy of orthogonal reduction spaces with the Euclidean Geometry.

Definition 4.1 Let P : t → → . We call the strict domain of P, written SDom(P), the minimal set of redexes U ⊆ t such that P is internal to U. We call the domain of P, written Dom(P), the set ∪_{Q≈_{L}P} SDom(Q), i.e., the minimal set of redexes U ⊆ t such that any Q that is Lévyequivalent to P is internal to U. And we call the minimal domain of P, written MDom(P), the set ∩_{Q≈_{L}P} SDom(Q).

It is easy to see that Dom(P) is SDom(P) augmented by all P -erased redexes not contracted in P; MDom(P) is the set of all P -needed redexes in t; and D0m(P) \ MDom(P) is the set of all P -unneeded P -erased redexes in t. Obviously P ≈_{L} Q implies Dom(P) = Dom(Q) and MDom(P) = MDom(Q), but not SDom(P) = SDom(Q). It follows from Theorem 3.8 (and also from Proposition 3.13 in the finite case) that MDom(P) = SDom(ST (P)) for any P.

Definition 4.2 We call a U-reduction P U-fair if each U-redex is erased in P, and call strongly U-cofinal if, for any U-reduction Q, Q ⊴_{L} P. If U is the set of all redexes in t, then U-fair reductions are called fair, and strongly U-cofinal reductions will be called strongly cofinal.

Lemma 4.3 A U-reduction P in an ASDRS is strongly U-cofinal iff it is U-fair.

Proof (⇒) Let Q be a U-reduction. We want to show that Q ⊴_{L} P. Then Q = Q′ + u + Q′′, where Q′/P/ = ∅ and u/(P/Q′) ≠ ∅. Let P = P′ + P′′, where P′ is finite and Q/P′ = ∅, and let u′ = u(P′/Q′) (see the figure). Then by U-fairness of P, u′/P′′ = ∅, contradicting u/(P/Q′) ≠ ∅.

(⇐) Suppose on the contrary that P is not U-fair. Then P = P′ + P′′ where P′ is finite and ft(P′) contains a U-redex u that is not erased in P′′. Clearly P^{∗} = P′ + u ⊔ P′′ is also a U-reduction and P^{∗} ⊴_{L} P – a contradiction.

The following lemma will not be used in the following, but it helps in understanding the relationship between the projection and restriction concepts: projection of Q onto P has an effect similar to restriction of Q to the set of P -needed redexes.

Lemma 4.4 (1) Let Q : t → → s and P : t → → . Then Q|P ≈_{ST A} (Q|MDom(P))|P.

(2) If moreover P is Mdom(P)-fair {Zurab:which is equivalent to saying that SF AM(P) = F AM^{+}(Mdom(P))}, then Q|P = Q|MDom(P).

Proof (1) By Lemma 3.24 and Corollary 3.17, F AM((Q|MDom(P))|P) = (S)F AM(Q|MDom(P))∩ SF AM(P) = SF AM(Q) ∩ F AM^{+}(MDom(P)) ∩ SF AM(P) = SF AM(Q) ∩ SF AM(P) (Since SF AM(P) ⊆ F AM^{+}(MDom(P))) = F AM(Q|P), implying by Proposition 3.13 that Q|P ≈_{ST A} (Q|MDom(P))|P. Since both reductions are standard by Theorem 3.8, (1) follows.

(2) By (1), Q|P ≈_{ST A} (Q|MDom(P))|P. Hence SF AM(Q|P) = SF AM((Q|MDom(P))|P) = (by Corollary 3.17) = SF AM(Q|MDom(P))∩SF AM(P) = (by Lemma 3.24) = SF AM(Q)∩ F AM^{+}(MDom(P)) ∩ SF AM(P) = (since SF AM(P) ⊆ F AM^{+}(MDom(P)) by the assumption) = SF AM(Q) ∩ F AM^{+}(MDom(P)) = (by Lemma 3.24) = SF AM(Q|MDom(P)).

Definition 4.5 (The Reduction Geometry) Let t be a term in an ASDRS R.

• Let P : t → → s, Q : t → → e and MDom(P) ∩ MDom(Q) = ∅. We say that P and Q are independent or do not interact, written P ⊥ Q, if any created redex in ft(P ⊔ Q) is a residual of a redex either from ft(P) or from ft(Q). Otherwise, P and Q interact, P ⊥̸ Q.

• We call a set Π = {P_{i}}_{i∈I} of reductions starting from t independent if P′_{i} ⊥ ⊔_{i≠j}P′_{j} for every i ∈ I and any finite initial parts P′_{i} of P_{i}. We call Π a basis of R at t if Π is independent and for any P : t → → , P ⊴_{L} ⊔P_{i}.

• The distance ∥P, Q∥ between co-initial reductions P, Q : t → → is the number of families whose essential member redexes are contracted either in P or in Q (but not in both). Here a redex v ⊆ s is essential [Kha88, Kha93] (or equivalently, Maranget-needed [Mar92]) if in any fair reduction starting from s a residual of v is contracted.

• The independence degree of U ⊆ t is the length of a shortest finite P internal to U such that there exists a reduction Q external to U that interacts with P, and is ∞ otherwise.

• We call U ⊆ t independent if every pair of finite U- and \overline{U}-reductions is so. We call ℑ = \{U_{i}\}_{i∈I} an independent covering if ℑ is a covering of t and each U_{i} is independent.

Example 4.6 (Bases) Consider a term t containing three redexes u, v, w, let w/(u ⊔ v) = ∅, w/u ≠ ∅, w/v ≠ ∅, and assume no redexes can be created by contraction of these redexes. Then Π_{1} = {u, v}, Π_{2} = {u, v, w}, Π_{3} = {u, w ⊔ v} and Π_{4} = {u, v ⊔ w} are all bases at t (there are others too), as all reductions are independent, and u⊔v ≈_{L} u⊔v⊔w ≈_{L} u⊔(w⊔v) ≈_{L} u⊔(v⊔w) are all normalizing, hence strongly cofinal. For Π_{1}, the strict domains of the axes do not form a covering of t, while for other bases they do. Note also that for Π_{4}, u erases the second step of v ⊔ w – (w/v)/(u/v) = ∅.

Note that, in the definition of P ⊥ Q, a created redex in ft(P ⊔ Q) cannot be a residual of redexes from both ft(P) and ft(Q), as otherwise the same redex would be a residual of redexes from ft(ST (P)) and ft(ST (Q)), which is impossible by the Stability Lemma, since MDom(P) ∩ MDom(Q) = ∅ implies that ST (P) and ST (Q) are external. Note that, in general, SDom(P) ∩ SDom(Q) = ∅ implies that P and Q are external, but not conversely. For example, let t = u = (λx.Kxy)v, where K = λx.λy.x; then P : t→^{u}Kvy→^{v}Koy and Q : t→^{K}(λx.y)v→^{v}(λx.y)o are external since v does not have u ⊔ K-residuals, while SDom(P) ∩ SDom(Q) = {v} ≠ ∅.

Further, the Cube Lemma implies that ⊥ is invariant under Lévy-equivalence. Note also that, if P ⊥ Q, Dom(P) ∩ Dom(Q) = ∅ need not hold. Indeed, consider the modified example from [Lév80]: take t = (λx.K_{a}(xu))K_{b} where K_{a} = λx.a, K_{b} = λx.b, and u is a redex, and con-

sider the reductions P : t→^{t}K_{a}(K_{b}u)→^{u}K_{a}(K_{b}o)→^{K_{b}}K_{a}b and Q : t→^{u}(λx.K_{a}(xo))K_{b}→^{K_{a}}(λx.a)K_{b},

where o is the contractum of u. Then u ∈ Dom(P), Dom(Q), but u ∉ MDom(P), MDom(Q), since u is not needed either in P or in Q.

In the definition of distance between reductions P and Q, one might think that it would be more appropriate to consider P ⊔ Q-needed redexes only. The following example shows that the distance would not be a metric. Indeed, take t = Kxω, P : t→^{ω}t→^{ω}t→^{ω}t→^{ω}t, Q : t→^{ω}t, and N : t→^{ω}t→^{ω}t→^{ω}t→^{ω}t→^{K}x. Then ∥P, Q∥ = 3 and ∥P, N∥ = ∥N, Q∥ = 1. It is easy to check that our distance measure on finite co-initial reductions satisfies the triangle inequality. To make it a metric, we define for co-initial finite reductions P, Q, P ≈_{f} Q iff F F AM(P) = F F AM(Q), where F F AM(P) denotes the set of families of essential redexes in P. Clearly, ≈_{f} is an equivalence relation, and the (co-initial) reduction space quotiented w.r.t. it is a metric, as |P, Q| = 0 implies P ≈_{f} Q. Note that ≈_{L}⊆≈_{f}, but not conversely.

The independence degree of U ⊆ t, if finite, characterizes the minimal amount of work that can be performed in U independently from the rest of the computation. Clearly the independence degree of an independent redex set is ∞.

Lemma 4.7 U ⊆ t is independent iff any finite reduction P : t → → s respects it.

Proof (⇐) Let U not be independent. Then there are reductions N and Q respectively internal and external to U that interact, i.e., there is a new redex u in ft(N ⊔ Q) that is not a residual of a redex either in ft(N) or in ft(Q). If N ⊔ Q does not respect U, then we are done. Otherwise, N ⊔ Q|U ⊔ N ⊔ Q|\overline{U} + u does not respect U.

(⇒) Let not every reduction respect U, and let P = P′+u be a shortest standard reduction that does not respect U. Since P′ respects U, we have that P′ ≈_{ST A} P′|U ⊔ P′|\overline{U} by Lemma 3.22. Since P does not respect U, u is not the residual of a redex either in ft(P′|U) or in ft(P′|\overline{U}). But this means that P′|U and P′|\overline{U} interact, i.e., U is not independent.

Proposition 4.8 Let U_{1}, U_{2} ⊆ t be independent. Then so are U_{1} ∪ U_{2}, U_{1} \ U_{2}, and U_{1} ∩ U_{2}; and for any finite P : t → → s:

(1) P |U_{1} ∪ U_{2} ≈_{ST A} P |U_{1} ⊔ P |U_{2};

(2) P |U_{1} ∩ U_{2} ≈_{ST A} (P |U_{1})|U_{2}.

(3) P |U_{1} \ U_{2} ≈_{ST A} (P |U_{1})|\overline{U_{2}}.

Proof Immediate from Lemma 3.26 and Lemma 4.7.

Theorem 4.9 Let ℑ = {U_{i}}_{i∈I} be an independent redex-covering of a term t in an ASDRS R, let P : t → → s, and let P_{i} be U_{i}-fair. Then P ≈_{L} ⊔_{i}P |U_{i}. Further, B = {P_{i}}_{i∈I} is a basis at t, and there are U_{i}-reductions P′_{i} ⊴_{L} P_{i} such that P ≈_{L} ⊔_{i}P′_{i}.

Proof Since ℑ is an independent covering of t, P respects ℑ by Lemma 4.7, and P ≈_{L} ⊔_{i}P |U_{i} follows from Theorem 3.30.(2). Since P_{i} is U_{i}-fair and P |U_{i} is an U_{i}-reduction, we have P |U_{i} ⊴_{L} P_{i} by Lemma 4.3. Hence P ⊴_{L} ⊔P_{i}. It follows immediately from Definition 4.5 that B is independent, thus is a basis at t, and we can take P |U_{i} for P′_{i}.

Corollary 4.10 (Independent Decomposition Theorem) Let ℑ = {U_{i}}_{i∈I} be an independent redex-covering of a term t in a DFS F, let P : t → → s be a complete family-reduction, and let P_{i} be U_{i}-fair complete family-reduction. Then P ≈_{L} ⊔_{i}P |U_{i}. Further, B = {P_{i}}_{i∈I} is a basis at t, and there are complete family-reductions P′_{i} ⊴_{L} P_{i} internal to U_{i} such that P ≈_{L} ⊔_{i}P′_{i}.

We have seen in Example 4.6 that not all bases are of the form described in Theorem 4.9. That is, if {P_{i}}_{i∈I} is a basis at t, P_{i} need not be an U_{i}-fair reduction for some independent covering ℑ = {U_{i}}_{i∈I} of t, as it is the case for Π_{1} (since w/u ≠ ∅ and w/v ≠ ∅). We could exclude this situation, by requiring in the definition of independence of U ⊆ t that for any pair of finite reductions P, Q respectively internal and external to U, Q does not erase any steps of P, that is, |P | = |P/Q|. We have chosen not to do so, since also in the relativized bases which we introduce in the next section, axes do not need to be maximal reductions on their strict domains.

Note that every term t in an ASDRS has an independent redex covering – {U(t)}, where U(t) is the set of all redexes of t, and has an independent basis – a fair reduction starting from t. Lemma 3.26 allows us to construct finer bases from existing ones, as if ℑ = {U_{i}}_{i∈I} and ℑ′ = {U′_{j}}_{j∈J} are bases, then ℑ ∩ ℑ′ = {U_{i} ∩ U′_{j}}_{(i,j)∈(I,J)} is a basis too, by Proposition 4.8. It is interesting to note that for any P : t → → s and any created redex u ⊆ s, the history of an extraction normal form of P u is internal to some finest independent set of redexes in t.

5 The Optimal Decomposition Theorem

In this section, we recall results concerning relative normalization in DFSs from [GK96, KG98], and prove the Optimal Decomposition Theorem: an optimal computation of a term t in a DFS, relative to a stable set of results S, can be decomposed into optimal computations of S-independent redex-sets of t.

Definition 5.1 ([GK94]) Let R be an SDRS.

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

(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 doesn’t 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.

For simplicity, we only consider stable sets that are closed under reduction (which implies closure under parallel moves). Note that since all terms, in particular, terms in a stable set S, in an SDRS R, are reducts of the initial term t_{∅}, we have immediately from CR and closure of S under reduction that every term in R is S-normalizable. The following theorem combines the Relative Normalization and Optimality Theorems for DFSs [GK96, KG98]).

Theorem 5.2 Let S be a stable set of terms in a DFS F, and let t ∉ S be an S-normalizable term in F. Then t contains a S-needed redex, and any S-needed reduction starting from t is eventually S-normalizing. Furthermore, any S-needed S-normalizing complete-family reduction a shortest S-normalizing reduction starting from t is shortest among S-normalizing (complete) family-reductions starting from t.

Definition 5.3 (Stable embedding [KG98a]) Let S be a set of reductions in an ASDRS, and let P, Q be co-initial reductions. Then P ⊴_{S} Q iff F AM_{S}(P) ⊆ F AM_{S}(Q), and P ≈_{S} Q iff F AM_{S}(P) = F AM_{S}(Q). We call ⊴_{S} and ≈_{S} respectively S-embedding and S-equivalence.

In [Kha98] a different (but equivalent) definition of ⊴_{S} is introduced which works for duplicating SDRSs as well. In particular, if P and Q are both finite, then P ⊴_{S} Q if P/Q is S-unneeded; otherwise, P ⊴_{S} Q if for any finite P′ ≤ P there is a finite Q′ ≤ Q such that P′ ⊴_{S} Q′. And P ≈_{S} Q iff P ⊴_{S} Q and Q ⊴_{S} P. It is immediate from this definition that ⊴_{L} ⊆ ⊴_{S}, thus ≈_{L}⊆≈_{S}.

The concepts introduced in Definition 4.5 (independence of reductions and redex sets, covering, basis, etc.) immediately relativize w.r.t. any stable set S, simply by replacing ‘independence’, ‘covering’, ‘basis’, etc. by ‘S-independence’, ‘S-covering’, ‘S-basis’, etc., respectively, and by replacing ‘(essential) redex’ and ‘reduction’ with ‘S-needed redex’ and ‘S-needed reduction’. We could as well relativize our Reduction Geometry w.r.t. stable sets of (finite or infinite) reductions [Kha98] which would be more general as stable sets of results can be given as the endpoints of reductions in stable sets of finite reductions. We do not consider here stable sets of infinite reductions since the aim of this section is to prove the Optimal Decomposition Theorem.

Definition 5.4 Let P : t → → in an ASDRS R, and let S be a stable set of terms in R. The S-domain of P, Dom_{S}(P), is the set of S-needed redexes in MDom(P). The set of families whose S-needed member redexes are contracted in P will be denoted by F AM_{S}(P).

It is easy to see that Dom_{S}(P) = SDom(P) ∩ U_{S}(t) = Dom(P) ∩ U_{S}(t), where U_{S}(t) is the set of all S-needed redexes in t. This follows from the fact that if u ⊆ t → →^{P} and u is P -erased and P -unneeded, then it is S-unneeded. To show the letter, let P^{∗} ≈_{L} P be external to u, and let P′ : t → → s be a finite initial part of P^{∗} that erases u. If P′ is S-normalizing, then u is clearly S-unneeded (by Definition 5.1); otherwise, for any S-normalizing reduction P′′ : s → → e, P′ + P′′ is S-normalizing and external to u, thus again u is S-unneeded (recall that every term is S-normalizable in an ASDRS).

Definition 5.5 (Relativized Reduction Geometry) Let t be a term in an ASDRS R.

• Let P : t → → s, Q : t → → e and Dom_{S}(P) ∩ Dom_{S}(Q) = ∅. We say that P and Q are Sindependent or do not S-interact, written P ⊥_{S} Q, if any created S-needed redex in ft(P ⊔ Q) is a residual of an S-needed redex either from ft(P) or from ft(Q). Otherwise, P and Q not S-interact, P ⊥̸_{S} Q.

• We call a set Π = {P_{i}}_{i∈I} of reductions starting from t S-independent if P′_{i} ⊥_{S} ⊔_{i≠j}P′_{j} for every i ∈ I and any finite initial parts P′_{i} of P_{i}. We call Π an S-basis of R at t if Π is S-independent and for any P : t → → , P ⊴_{S} ⊔P_{i}.

• The S-distance ∥P, Q∥ between co-initial finite reductions P, Q : t → → is the number of families whose S-needed member redexes are contracted either in P or in Q (but not in both).

• The S-independence degree of U ⊆ t is the length of a shortest finite P internal to U such that there exists a reduction Q external to U that S-interacts with P, and is ∞ otherwise.

• We call U ⊆ t S-independent if every pair of finite (equivalently, S-needed) U- and \overline{U}- reductions is so. We call ℑ = {U_{i}}_{i∈I} an S-independent covering if ℑ is a covering of {Zurab:U_{S}(t)} and each U_{i} is S-independent.

In [GK96], we defined an algorithm associating to a reduction P an S-needed reduction [P]_{S} such that P ≈_{L} [P]_{S} + [P]_{S}^{−}, where [P]_{S}^{−} is S-unneeded. The algorithm works for regular stable sets of terms S in any SDRS, where regular means that S-unneeded redexes cannot duplicate S-needed once. Thus it applies for any stable set S in an ASDRS, and for any P one has F AM_{S}(P) = F AM([P]_{S}). The algorithm simply pushes all S-needed steps of P before S-unneeded steps, which is possible by the following lemma:

Lemma 5.6 ([GK96]) (1) Residuals of S-unneeded redexes in a term t ∉ S remain S-unneeded.

(2) Let t ∉ S, t→^{u}t′, let u be S-unneeded, and let u′ ⊆ t′ be a created redex. Then u′ is S-unneeded.

(3) Let t be S-normalizable, v ⊆ t be S-needed, t→^{u}s, and v ≠ u. Then v has an S-needed residual in s.

Note also that any S-needed reduction P, in an ASDRS, is standard, implying SDom([P]_{S}) = MDom([P]_{S}). Indeed, if on the contrary P contracts a P -unneeded redex P′u (where P = P′ + u + P′′), then there is P^{∗} ≈_{L} u + P′′ that discards u, and for any finite Q such that P^{∗} + Q is S-normalizing (Q may be empty), P^{∗} +Q is external to Q, which contradicts S-neededness of u. Using this observation, we can give an equivalent definition of independence using S-needed reductions:

Lemma 5.7 Let P, Q be finite co-initial reductions in an ASDRS. Then P ⊥ Q iff MDom([P]_{S})∩ MDom([Q]_{S}) = ∅ and any created S-needed redex in ft([P]_{S} ⊔ [Q]_{S} is a residual of a S-needed redex created by [P]_{S} or by [Q]_{S}.

Proof Indeed, Dom_{S}(P) = MDom(P) ∩ U_{S}(t) = SDom(P) ∩ U_{S}(t) = (by definition of [P]_{S}) = SDom([P]_{S}) = (since [P]_{S} is standard) = MDom([P]_{S}), hence Dom_{S}(P) ∩ Dom_{S}(Q) = ∅ iff MDom([P]_{S}) ∩ MDom([Q]_{S}) = ∅. Further, if ft(P ⊔ Q) contains a created S-needed redex u, then by Lemma 5.6 u must be a residual of an S-needed redex u′ ∈ ft([P]_{S} ⊔ [Q]_{S}) (since P ⊔ Q ≈_{L} [P]_{S} ⊔ [Q]_{S} + N for some S-unneeded N (see the figure below). And conversely, any S-needed redex u′ ∈ ft([P]_{S} ⊔ [Q]_{S}) has an S-needed N-residual u ∈ ft(P ⊔ Q) by Lemma 5.6. Finally, if u is a residual of a redex u^{∗} say in ft(P), then by Lemma 5.6 u^{∗} must be S-needed and must be a residual of a S-needed u^{′∗} ∈ ft([P]_{S}) and u′ must be a residual of u^{′∗} by Lemma 3.5. Conversely, if an S-needed redex u′ ∈ ft([P]_{S} ⊔ [Q]_{S}) is a residual of u^{′∗} ∈ ft([P]_{S}), then by Lemma 5.6 u^{′∗} is S-needed, it has an S-needed residual u^{∗} ∈ ft(P), u′ has an S-needed N-residual u ∈ ft(P ⊔ Q), and u is a residual of u^{∗} by Lemma 3.5, and we are done.

[figure: ·; [P]_{S}; · ∋ u^{′∗}; [P]_{S}^{−}; · ∋ u^{∗}]
[figure: ·; [Q]_{S}; · ∋ u′]
[figure: N]
[figure: ·; [Q]_{S}^{−}; · ∋ u]

Similar observations can be made for the other concepts in Definition 5.5. For example, in the third item, it can be shown that S-distance between P, Q coincides with the number of families whose member redexes are contracted either in [P]_{S} or in [Q]_{S} (but not in both); and, in the fourth item, it can be shown that P must be S-needed, and that Q can be chosen S-needed too. In general, all concepts in Definition 5.5 are invariant under S-equivalence ≈_{S}.

Note that the relativized independence concept allows in general for a finer independent covering of a term, hence allows for more independence in computation. For example, let S be the set of head-normal forms, in the λ-calculus, and let t = (λx.\underline{(λy.x′′y)(\underline{(λx′.x)a}b)})(\underline{(λz.(λz′.z′′))c}). t contains four redexes, u_{1} = t, u_{2}, u_{3} and u_{4}, underlined and enumerated from left to right. u_{1} and u_{2} are on the left-spine, and are S-needed, i.e., head-needed. Their contraction yields a head-normal form (no new head-needed redexes are created), therefore U_{h} = {{u_{1}}, {u_{2}}} is a head-independent covering of t. However, contraction of all four redexes creates a new redex (λz′.z′′)b in x′′((λz′.z′′)b), and therefore no proper subset of U = {u_{1}, u_{2}, u_{3}, u_{4}} is independent, i.e., {U} is the only independent covering of t.

We will need the following relativized version of U-fairness:

Definition 5.8 Let S be a stable set of terms in a DRS R, t be a term in R, and U ⊆ t. We call a U-reduction P : t → → s (U, S)-fair if s does not contain S-needed U-redexes. (Note that s may contain S-unneeded U-redexes, thus P need not be U-fair.)

Lemma 5.9 Let ℑ = {U_{i} | i ∈ I} be an S-independent covering of t, in an ASDRS.

(a) If P : t → → s is an S-normalizing S-needed reduction, then P_{i} = P |U_{i} : t → → s_{i} are (U_{i}, S)- fair S-needed U_{i}-reductions.

(b) If P_{i} : t → → s_{i} are (U_{i}, S)-fair S-needed U_{i}-reductions, then P = ⊔_{i∈I}P_{i} : t → → s is an S-normalizing S-needed reduction.

Proof (a) By Definition 3.21, P_{i} is an U_{i}-reduction, and it contracts residuals of redexes contracted in P, hence is S-needed by Lemma 5.6.(3). Suppose on the contrary that say P_{j} is not (U_{j}, S)-fair, i.e., there is v ⊆ s_{j} that is an U_{j}-redex and is S-needed. Since \overline{P_{j}}/P_{j}, where \overline{P_{j}} = P |\overline{U_{j}}, is external to v, it follows from Lemma 5.6.(3) that v has an S-needed residual in s – contradiction, since s ∈ S.

(b) Since every P_{i} is S-needed, so is P by Lemma 5.6.(3). Since ℑ = {U_{i} | i ∈ I} is an Sindependent covering of t and ⊔_{i}P_{i} ≈_{L} P, every S-needed redex in s is a \overline{P_{i}}-residual of a redex in s_{i} for some i (where \overline{P_{i}} = P |\overline{U_{i}}), which is S-needed by Lemma 5.6.(1). Since every P_{i} is an (U_{i}, S)-fair U_{i}-reduction, any S-needed redex u ⊆ s_{i} is a residual of a redex v ∈ U_{j} for some j ≠ i, which is S-needed by Lemma 5.6.(1). But since P_{j} is (U_{j}, S)-fair, v does not have P_{j}- residuals. Hence, by the Cube Lemma, u does not have \overline{P_{i}}-residuals. Thus s does not contain S-unneeded redexes, and by Theorem 5.2, s ∈ S.

Lemma 5.10 Let P : t → → s be an (U, S)-fair U-reduction, let t→^{u}e, where u ∈ U ⊆ t and let U′ be the set of U-redexes in e. Then P′ = P/u : e → → o is an (U′, S)-fair U′-reduction.

Proof Since P is (U, S)-fair, there are no S-needed U-redexes in s. Thus if u has a P -residual in s, it is S-unneeded, therefore, by Lemma 5.6.(2), all the redexes in o created by u/P are S-unneeded. Again by Lemma 5.6.(1), u/P -residuals of U-redexes in s remain S-unneeded. Thus any U-redex in o is S-unneeded. But the sets of U-redexes and U′-redexes in o coincide by the Cube Lemma, because both sets consist precisely of redexes not in \overline{U}/(u ⊔ P). Hence P′ is an (U′, S)-fair U′-reduction.

Lemma 5.11 Let t ∉ S be S-normalizable, and let U ⊆ t, in an ASDRS R. A reduction starting from t is an optimal (U, S)-fair U-reduction iff it is an S-needed (U, S)-fair U-reduction.

Proof (⇐) Let Q and P be (U, S)-fair U-reductions, and let Q be S-needed. We show |Q| ≤ |P | by induction on |Q|. If |Q| = 0, then (⇐) is clear. So let Q : t→^{v}s → →^{Q′} e. Since v is S-needed and P is (U, S)-fair, it follows from Lemma 5.6.(3) that any residual of v along P is S-needed and P must contract a residual of v. Hence, by affineness, |P′| ≤ |P | − 1, where P′ = P/v. Let U′ be the set of U-redexes in s. Then, by Lemma 5.10, P′ and Q′ are (U′, S)-fair U′-reductions. Hence, by the induction assumption, |Q′| ≤ |P′|. Thus, |Q| ≤ |P |.

(⇒) Let Q and P be (U, S)-fair U-reductions, let Q be S-needed, but P not be S-needed. We show that |Q| < |P | by induction on |P |. If |P | = 0, then |Q| = 0. So let P = u + P′. Since Q is S-needed, so is Q′ = Q/u by Lemma 5.6.(3). Suppose first that u is S-unneeded. Then so is every residual of it along Q by Lemma 5.6.(1). Hence Q is external to u. Since S-unneeded redexes cannot erase S-needed ones, |Q′| = |Q|. But, by (⇐), |Q′| ≤ |P′|, since both Q′ and P′ are (U′, S)-fair U′-reductions by Lemma 5.10, where U′ is the set of U-redexes in ft(u), and Q′ is S-needed. Hence |Q| < |P | in that case. Now assume u is S-needed. Then |Q′| = |Q| − 1, as we have shown above (in the proof of (⇐)). Thus, by the induction assumption, |Q′| < |P′|. And we have again |Q| < |P |.

We are now ready to prove the Optimal Decomposition theorem for ASDRSs:

Theorem 5.12 Let S be a stable set of terms in an ASDRS R, let ℑ = {U_{i}}_{i∈I} be an Sindependent covering of an S-normalizable term t in R, let ℑ′ = {U_{j}}_{j∈J⊆I} contain all U_{i} that contain at least one S-needed redex of t, and let P_{j} be internal to U_{j}. Then P_{j} are optimal (i.e., shortest) (U_{j}, S)-fair reductions iff P = ⊔_{j}P_{j} is an optimal S-normalizing reduction starting from t.

Proof An immediate consequence of Lemma 5.9, Theorem 5.2, and Lemma 5.11.

It is shown in [KG97c, KG98] that S-needed complete family-reductions in a DFS precisely correspond to S_{I}-needed reductions in F_{I}, where S_{I} = S ∩ T er(F_{I}) is stable in F_{I} (T er(F_{I}) is the set of terms in F_{I}). Hence we have immediately from Remark 2.15 and Theorem 5.12 the following Optimal Decomposition Theorem for DFSs:

Corollary 5.13 (Optimal Decomposition) Let S be a stable set of terms in a DFS F, let ℑ = {U_{i}}_{i∈I} be an S-independent covering of an S-normalizable term t in F, let ℑ′ = {U_{j}}_{j∈J⊆I} contain all U_{i} that contain at least one S-needed redex of t, and let P_{j} be internal to U_{j}. Then P_{j} are optimal (i.e., shortest) (U_{j}, S)-fair complete family-reductions iff P = ⊔_{j}P_{j} is an optimal S-normalizing complete family-reduction starting from t.

6 Conclusions

We have defined concepts similar to those in Vector Spaces for orthogonal rewrite systems, and described how these can be used in distributive evaluation of sequential programs. The constructed Reduction Geometry is not just a nice piece of mathematics. Obviously, (relative) independence of redex-sets is undecidable in general, as is neededness. However, we hope that decidable approximations for independence can be defined which will yield decidable concepts for large classes of rewrite systems, as is the case for the neededness [HL91].

For example, all the introduced concepts are decidable for Recursive Program Schemes (RPSs), both in first [Kha93] and higher order [Kha94] cases. Several kinds of RPS were extensively studied in the literature, mainly in the seventies [Cou90]. Our (first-order) RPSs correspond to Applicative RPSs in [Cou90]. The left-hand sides of RPS-rules contain one defined symbol only, and RPSs do not have full computational power as the if − then − else operator is only evaluated semantically (i.e., there is no rewrite rule for it). Actually, because of a specific simple form of redex-creation in such systems – created redexes are determined by the rewrite rules only, and the arguments or the context in which a redex is contracted do not contribute to redex-creation – one has maximal possible independence there: any redex forms an independent redex-set. It is shown (very briefly) in [Kha94] how computation of the normal form of a term t in a higher-order RPS can be decomposed into (concurrent) computation of its redexes, and how can the latter be combined to yield the normal form of t (for first-order RPSs this is much simpler since there are no β-like substitution steps involved). This technique even yields a method of transforming RPSs into simpler irreducible ones where the right-hand sides of rules are in normal form. All these are based on the concept of essential similarity of redexes, which contains a ‘minimal information’ determining the normalization behaviour of redexes in higherorder RPSs (essentiality is a refinement of neededness that makes sense for all subterms, not for redexes only).

Another important example where independent redex-sets can be found effectively is the set of hyperbalanced λ-terms [KP98]. Hyperbalanced terms form the smallest subset of λ-terms, closed under β-reduction, such that for any maximal subterm of the form (λx_{1} … x_{n}.s)t_{1} … t_{m} one has m = n, and whenever t_{1} is an abstraction λy_{1} … y_{l}.o, every free occurrence of x_{1} in s is in the subterm of the form x_{1}o_{1} … o_{l}. All simply typable terms, up to a restricted η-expansion, are hyperbalanced. All hyperbalanced terms are strongly normalizing, and in such terms all unneeded (rather, inessential) subterms can be statically detected. Among other things, these are due to the fact that only two kinds of redex-creation, out of three possible kinds of redexcreation in the λ-calculus [Lév76], is possible in the setting of hyperbalanced terms. Like in RPSs, any redex in a hyperbalanced term forms an independent redex-set, and our theory suggests that they can be evaluated independently – every redex uses only a substructure of a given term, and these substructures for different redexes do not ‘overlap’. However, unlike RPSs, it is not clear what constitute these substructures (i.e., ‘minimal information’), and an appropriate implementation techniques evaluating redexes independently from each other in hyperbalanced terms is at present not known.

There is an obvious relationship between the independence concept and modularity of properties in TRSs (see [Klo92] for a survey) which we think is worth investigating. For example, in the simple case when two orthogonal rewrite systems R_{1} and R_{2} have disjoint alphabets Σ_{1} and Σ_{2}, and their rules are non-collapsing (i.e., right-hand sides contain a function symbol), then in any term constructed from symbols in Σ_{1} ∪ Σ_{2}, the sets consisting of respectively R_{1}-redexes and R_{2}-redexes are independent, therefore for example SN is a modular property: R_{1} ∪ R_{2} is SN iff R_{1} and R_{2} are SN. This result for (not-necessarily orthogonal) TRSs is proved in [Rus87].

Acknowledgments We thank J. R. Kennaway, V. van Oostrom and F.-J. de Vries for useful comments. Diagrams were drawn using Paul Taylor’s diagram package.

References

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

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

[BeLé79] Berry G., Lévy J.-J. Minimal and optimal computations of recursive programs. JACM, vol. 26, pp. 148-175, 1979.

[Cou90] Courcelle B. Recursive Applicative Program Schemes. In: J. van Leeuwen ed. Handbook of Theoretical Computer Science, Chapter 9, vol.B, 1990, p. 459-492.

[Gir91] Girard J.-Y. On the unity of logic. INRIA Report 1467, 1991.

[GK94] Glauert J.R.W., Khasidashvili Z. Relative Normalization in Orthogonal Expression Reduction Systems. In: Proc. of the 4^{th} International workshop on Conditional (and Typed) Term Rewriting Systems, CTRS’94, Springer LNCS, vol. 968, N. Dershowitz, N. Lindenstrauss eds. Jerusalem, 1994, p. 144-165.

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

[GLM92] Gonthier G., Lévy J.-J., Melliès P.-A. An abstract Standardisation theorem. In: Proc. 7th IEEE Symp. on Logic in Computer Science, LICS’92. 1992, p. 72-81.

[GAL92] Gonthier G., Abadi M., Lévy J.-J. Linear Logic without boxes. In: Proc. 7th IEEE Symp. on Logic in Computer Science, LICS’92, 1992, p. 223-234.

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

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

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

[Ken96] Kennaway J.R. Transfinite rewriting, Int. School on Type Theory and Term Rewriting, Glasgow, 1996. (Invited survey paper.)

[KS89] Kennaway J.R., Sleep M.R., Neededness is hypernormalizing in regular combinatory reduction systems, Preprint, School of Information Systems, UEA Norwich, 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., eds. Term Graph Rewriting: Theory and Practice. John Wiley, 1993.

[KKSV94] Kennaway J. R., Klop J. W., Sleep M. R, de Vries F.-J. On the adequacy of Graph Rewriting for simulating Term Rewriting. ACM Transactions on Programming Languages and Systems, 16(3):493-523, 1994.

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

[Kha88] Khasidashvili, Z., β-reductions and β-developments of λ-terms with the least number of steps. In: Proc. of the Int. Conf. on Computer Logic, COLOG’88, Springer LNCS, vol. 417, p. 105-111, 1990.

[Kha93] Khasidashvili Z. Optimal normalization in orthogonal term rewriting systems. In: Proc. of the 5^{th} International Conference on Rewriting Techniques and Applications, RTA’93, Springer LNCS, vol. 690, C. Kirchner, ed. Montreal, 1993, p. 243-258.

[Kha94] Khasidashvili Z. On higher order recursive program schemes. In: Proc. of the 19^{th} International Colloquium on Trees in Algebra and Programming, CAAP’94, Springer LNCS, vol. 787, S. Tison, ed. Edinburgh, 1994, p. 172-186.

[Kha98] Khasidashvili Z. Stable Computational Semantics of Conflict-free Rewrite Systems. (Conference submission.)

[KG96] Khasidashvili Z., Glauert J. R. W. Discrete normalization and Standardization 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.

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

[KG97] Khasidashvili Z., Glauert J.R.W. Zig-zag, extraction and separable families in nonduplicating stable deterministic residual structures. Report IR-420, Free University, February 1997.

[KG97a] Khasidashvili Z, Glauert J. R. W. The Geometry of Orthogonal Reduction Spaces. In Proc. of the 24^{th} International Colloquium on Automata, Languages, and Programming, 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. In Proc. of the 22^{nd} International Symposium on Mathematical Foundations of Computer Science, MFCS’94, Springer LNCS, To appear.

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

[KG98] Khasidashvili Z., Glauert J.R.W. An abstract theory of optimal evaluation (Journal submission). Available at http://www.sys.uea.ac.uk/˜ zurab.

[KG98a] Khasidashvili Z., Glauert J.R.W. Relating conflict-free stable transition and event models (Journal submission). Available at http://www.sys.uea.ac.uk/˜ zurab.

[KP98] Khasidashvili Z., Piperno A. Normalization of Typable Terms by Superdevelopments. Submitted.

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

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

[Laf90] Lafont Y. Interaction nets. In: Proc. of POPL’90, p. 95-108.

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

[Lév76] Lévy J.-J. An algebraic interpretation of the λβκ-calculus and a labelled λ-calculus. Theoretical Computer Science, 2:97-114, 1976.

[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 λ-calculus. In: To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalizm, Hindley J. R., Seldin J. P. eds, Academic Press, 1980, p. 159-192.

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

[Mil92] Milner R. Functions as processes. MSCS 2(2):119–141, 1992.

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

[Rus87] Rusinowitch M. On termination of the direct sum of term rewriting systems. Information Processing Letters 26, p. 65-70, 1987.

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

[Win89] Winskel G. An introduction to Event Structures. Springer LNCS, vol. 354, 1989, p. 364-397.