The (Conflict-free) Reduction Geometry ⋆

Zurab Khasidashvili

Department of Mathematics and Computer Science, Bar-Ilan University Ramat-Gan 52900, Israel khasidz@cs.biu.ac.il

John Glauert

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

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 in the framework of Deterministic Family Structures, which are Abstract Reduction Systems with an axiomatized residual and family relations on redexes, and model all orthogonal rewrite systems.

1 Introduction

Efficient evaluation of expressions benefits from concurrent evaluation of subexpressions. In computation in general, it is normal that intermediate results of

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

Preprint submitted to Elsevier Preprint 8 December 1999

different subexpressions are used by other subexpressions, and contribute to creation of new computable subexpressions. In concurrent languages like the π-calculus [30] this is expressed explicitly 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 independent subexpressions can be conducted concurrently, in isolation from computations elsewhere in the expression, 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 [2] is the prime example. 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 is neither duplication nor erasure of redexes. The main analogy is the following: in a Euclidean 3dimensional 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}, up to Lévy or permutation-equivalence, ≈_{L}. Here the ‘sum’ operation is the least upper bound operation, ⊔, in the reduction space ordered by Lévy’s embedding relation ⊴_{L}, and ≈_{L}= ⊴_{L} ∩ ⊵_{L} [28]. And 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 reduction P_{i} is a maximal reduction internal to a redex-set U_{i} in t, i.e, P_{i} contracts only residuals of redexes in U_{i} and newly created redexes (which we call U_{i}-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 [28], 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 were to 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 | 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) [35], 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 leftclosed 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 configurations 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 leftmost 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 Term Rewriting System (TRS) 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 [27,28]. 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 [25] and Kathail [9]. 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 seems 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 result 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 [11] or directed acyclic graphs (DAGs) [29] 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).

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, headnormal forms, weak-head-normal forms, etc. In [4], we have characterized all reasonable sets of finite ‘(partial) results’ as stable sets S of terms, and have shown that 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 P_{i} need not be normalizing even if S is the set of normal forms, as the S-unneeded redexes in the final terms of P_{i} will not be present in the final term of the sum of P_{i}. But P_{i} are (U_{i}, S)-fair, meaning that the final terms of P_{i} do not contain S-needed U_{i}-redexes.

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 [6]. DFSs are Abstract Reduction Systems (ARSs) with axiomatized residual and family relations, which model all orthogonal rewriting systems and cover all existing concepts of redex-family in the literature [27,28,10,29,1,32]. Important standard results such as the Standardization and Normalization Theorems of Curry and Feys [2], or Lévy’s Optimality Theorem [27,28], can be proven using only the abstract framework of DFSs [6,15]. 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 [18,19]. 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évy-equivalence, we work with standard reductions, which in DFSs are reductions in which later steps ‘do not erase’ the preceding ones (we ignore outside-in and left-to-right order of contraction of redexes, as there are no such concepts in DFSs, and these are actually inappropriate) [15]. Even if restricted to standard reductions, the reduction space of an AZDFS ordered by permutation embedding need not be isomorphic to the domain generated by a PES. Therefore, instead of PESs, we will (by necessity) use event models with axiomatized erasure relation developed in [17,20] to give more intuitive interpretetion of our constructions in terms of events (or equivalntly, in terms of distributedness in computation). This interpretation also shows that our Geometry metaphor can be seen as a further development of the Event Structure approach in modelling distributedness.

To conclude, we note that in any DFS F, we can define independent redex sets U_{i} ⊆ t via interpreting F into the corresponding AZDFS F_{I}, and compute the sets U_{i} independently in F (not necessarily using complete family-reductions, if Lévy-style optimality is not a concern). Indeed, we can easily show that for any set Q_{i} of (U_{i}, S)-fair reductions in F, ⊔_{i∈I}Q_{i} is S-normalizing. Hence our restriction to affine systems when developing the (intermediate) independent decomposition results has no implications for the applicability of our results to duplicating and/or erasing orthogonal systems when one is interested in independent computations of (relative) normal forms.

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

2 Preliminaries

In this section, we quickly recall Deterministic Family Structures (DFSs) [6,19] and Deterministic Erasure Event Structures (DEESs) [17,20]. We assume that the reader is familier with the concepts related to Lévy Permutation equivalence [27,8,28,2]. Related abstract residual models are studied in [34,7,31].

We start by introducing Abstract Reduction Systems (ARSs). Our definition is slightly different from the usual one [24]. We then define Deterministic Residual Structures (DRSs) which are ARSs with an axiomatized notion of residual. Deterministic Family Structures (DFSs) are then defined as DRSs with an axiomatized concept of redex-family [27].

Definition 1 An ARS is a triple A = (Ter,Red,→) where Ter is a set of terms, ranged over by t, s, o, e; Red is a set of redexes (or redex occurrences), ranged over by u, v, w; and →: Red ↦ (T er × T er) is a function such that for any t ∈ T er there is only a finite set of u ∈ Red such that ↦ (u) = (t, s), written t→^{u}s. This set will be known as the redexes of term t. Note that → is a total function, so one can identify u with the triple t→^{u}s. ^{1} A reduction is a (finite

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

or infinite) sequence t→^{u_{1}}t_{2}→^{u_{2}} . . ..

Notation 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, and write P : t → → if P may be infinite. P + Q denotes the concatenation of P and Q ((when P is finite and its final term coincides with the initial term of 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; if moreover Q is finite, we write Q ≤_{fin} P. Finally, 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 in t. If U ⊆ t, then \overline{U} will denote the complement of U, i.e., the set of redexes in t not in U.

Definition 3 (1) 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 finite 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 it is finite and 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] ([7]) 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] ([34]) Let u, v ⊆ t, let u ≠ v, and let u/v = ∅. Then

v/u ≠ ∅.

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

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

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

In a DRS R, the residual relation /, Lévy permutation embedding ⊴_{L}, and Lévy permutation equivalence ≈_{L}, on finite co-initial reductions are defined exactly as in syntactic orthogonal rewrite systems, see [2,8,28,34]. And these concepts naturally extend to infinite reductions as well (except N/P is only defined for finite P), see e.g. [15]. We only recall that the Strong Church-Rosser property stetes that for any co-initial finite reductions P, Q, P ⊔ Q ≈_{L} Q ⊔ P, where P ⊔ Q = P + Q/P. And another usefull property, the Cube Lemma, states that for any finite co-initial reductions P, Q and N, N/(P ⊔Q) = N/(Q⊔P). In the particular, when N = v, the Cube Lemma implies that the residuals of v in ft(Q ⊔ P) along Q ⊔ P and P ⊔ Q are the same redexes.

We remark that, for finite co-initial reductions P and Q, P/Q is defined uniquely if we regard it as a multi-step reduction, where a multi-step contracts simultaneously a set of redexes in a term. 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.

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

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

(2) Further, ≃ and ↪ satisfy the following axioms:

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

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

in ϕ.

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

[FFD] (Finite Family Developments) Any reduction that contracts redexes

of a finite number of families is terminating.^{2}

(3) 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]). Affine ZDFSs will be called AZDFSs.

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

All concepts of family for orthogonal reduction systems known to us (such as [27,28,10,29,1,32]) satisfy our family axioms ([FFD] is not easy to prove for concreate systems, while the other family axioms can easily be varified using the labelling definitions of these family concepts). These axioms allow for example for abstract proofs of Relative Normalization and Optimality Theorems [6,19].

As already mentioned in the introduction, DFSs F can be interpreted into AZDFSs F_{I}. Since this interpretation allows us to restrict our investigation into the independence concept to AZDFSs, we very breifly recall the construction from [18,19]. Recall that a family-reduction in F is a multi-step reduction contracting in each multi-step a set of redexes in a single family; and a family-reduction is complete if each multi-step contracts all redexes in a single family (in the corresponding term) [28]. Complete family-reductions in F are interpreted as reductions in the corresponding AZDFS F_{I}. Since whether a redex set U ⊆ s is a family depends on the history of redexes in U, the interpretation requires all histories to be co-initial, i.e., an initial term is to be fixed in F, and only complete family-reductions relative to that term will have corresponding reductions in F_{I}. Thus the reduction graph of F_{I} consists of (some of the) reducts of the initial term, and the residual in F_{I} is induced by that of F.

Theorem 5 ([18,19]) For any DFS F, F_{I} is an AZDFS.

Remark 6 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 AZDFSs can be read as definitions or results concerning complete family-reductions in arbitrary DFSs.

In AZDFSs, any term contains at most one member redex of a family:

Proposition 7 ([18,19]) Let P v ≃_{z} Qw, in an AZDFS. Then v/(Q/P) = w/(P/Q). In particular, if P ≈_{L} Q, then v = w.

This allows us to isomorphically embed AZDFSs into DEESs [17,20].

Recall that a Deterministic (or Conflict-free) Prime Event Structure (DPES) [35] is a couple E = (E, ≤), where E is a set of events, ranged over by e, e_{1}, …, and the causal dependency relation ≤ is a partial order on E. Finite configurations of E are finite left-closed subsets α, β, … of E, i.e., subsets L_{fin}(E) = {α ⊆_{fin} E | e ∈ α ∧ e′ < e ⇒ e′ ∈ α}; they represent stages of computation.

Definition 8 A Deterministic Erasure Event Structure (DEES) is a triple C = (E, ≤, ⊳), where E = (E, ≤) is a conflict-free PES and ⊳ ⊆ L_{fin}(E) × E is inessentiality or erasure relation (read α ⊳ e as: ‘e is α-inessential’), satisfying the following axioms, where α, β ∈ L_{fin}(E):

[E0] ∀e ∈ E : ∅ ⋫e; [E1] α ⊳ e ∧ α ⊆ β ∈ L_{fin}(E) ⇒ β ⊳ e;

[E2] α ⊳ e′ ∧ α ⊳ e ∧ α − e′ ∈ L_{fin}(E) ⇒ α − e′ ⊳ e;

[E3] α ⊳ e ∧ e < e′ ⇒ α ⊳ e′;

[E4] α ∪ ⌈e^{<}⌉ ⊳ e ⇒ α ⊳ e, where ⌈e^{<}⌉ = {e′ | e′ < e}.

The erasure relation is extended to infinite configurations α by: α ⊳ e iff ∃α′ ⊆_{fin} α : α′ ⊳ e.

We will call events that are smallest w.r.t. the causal dependency relation, ≤, initial. The set of all initial events in E will be denoted by Init(E), and similarly for any subset of events (e.g., Init(α)). We will use X, Y to range over sets if intial events. We will assume that Init(E) is finite.

The equivalence of AZDFSs and DEESs [17,20] allows us to freely choose between the two models as a formalizm for developing our (intermediate) decomposition results. Since our goal is to study the decomposition properties for duplicating systems (the restriction to AZDFSs is only a technical tool simplifying the proofs), we feel it is important to demonstrate our constructions on the operational (semantics) level (AZDFSs). But we also interpret our constructions on the events (semantics) level (DEESs), to support our claim of distributedness or parallelism in computation offered by our independence concept.

3 Decomposition of Reductions in AZDFSs

In this section, we define the 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 [15].

3.1 Standardization

In this subsection, we define a somewhat non-standard concept of standardization. Firstly, our standard reductions are those 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 [2,8,23], but we do not need such a standardization concept either. Secondly, we define a relativized standardization algorithm which standardizes any reduction Q in an AZDFS w.r.t. any other reduction P, co-initial with Q.

Definition 9 (Standard Reductions [15]) Let a DRS be given.

• Let U ⊆ t and P : t → → (so P may be infinite). We call P external to U if P does not contract residuals of redexes in U. If U = {u}, then P is called external to u. We say that u is erased in P or is P -erased), and that P erases u, if u/P′ = ∅ for some P′ ≤_{fin} P. If P is external to u and erases it, then P discards u.

• 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- (un)needed if u is Q/P′-(un)needed. We call P Q-(un)needed if every redex contracted in P is Q-(un)needed.

• 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 same holds true for P -erasure, but not for the concepts ‘external’ and ‘discards’.

Definition 10 (1) 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 (not necessarily P -needed) residual is contracted in Q first among 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) = ∅.

(2) 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 above algorithm and the Standardization Theorem below differ slightly from the ones in [15] since, unlike [15], here we cannot restrict ourselves to the case when Q ⊴_{L} P. However, when Q ⊴_{L} P (or Q ≈_{L} P), the two algorithms are equivalent.

Lemma 11 If u ⊴_{L} P ⊴_{L} Q and u is Q-needed, in an AZDFS, 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 P′′ ≤_{fin} 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 9.

Lemma 12 Let t→^{u}s, P : t → → , and v′ = v/u, in an AZDFS.

(1) If v is P -unneeded, then so is v′.

(2) ([15]) If moreover u/P = ∅, then the converse is also true.

Proof We only prove (1). 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 P_{1}^{∗}v^{∗} ≃_{z} ∅v, implying by Proposition 7 that P^{∗} contracts a residual v^{∗} of v – a contradiction.

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

Note that without the condition u/P = ∅, Lemma 12.(2) 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 → → y, and v′ is P/u-unneeded.

Theorem 13 (Standardization) Let an AZDFS be given.

(1) For any co-initial reductions Q, P, finite or infinite, ST_{P} (Q) is a P -needed, and standard, reduction such that ST_{P} (Q) ⊴_{L} Q, P.

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

Proof We only prove (1). By Definition 10, we have

ST_{P} (Q) = v_{0} + ST_{P/v_{0}}(Q/v_{0})
= v_{0} + v_{1} + ST_{P/(v_{0}+v_{1})}(Q/(v_{0} + v_{1}))
= v_{0} + v_{1} + v_{2} + …

where v_{i} is P/(v_{0} + v_{1} + … + v_{i−1})-needed and its residual is contracted in Q/(v_{0} + v_{1} + … + v_{i−1}). Denote N_{i} = v_{0} + v_{1} + … + v_{i−1}. Then v_{i} ⊴_{L} P/N_{i}, v_{i} ⊴_{L} Q/N_{i}, ST_{P} (Q) is P -needed (by Definition 9), and ST_{P} (Q) ⊴_{L} Q, P. Hence ST_{P} (Q) is standard by Lemma 11.

It has been shown in [18,19] that, in AZDFSs, all standard variants of a finite reduction P can be constructed effectively (as P -neededness is decidable and there is 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). As we have seen above, this is not true for infinite reductions in general, and we need to be careful in our statements and proofs when considering standard variants of infinite reductions.

3.2 Characterizing permutation-equivalence using families

In this subsection, we give a characterization of permutation-equivalence in AZDFSs via families of contracted redexes in corresponding reductions, and use it in the next subsection 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, and allow us to interpret that theorem in PEESs.

Notation 14 Below, F AM(P) (resp. SF AM(P)) denotes the set of families of which at least one (resp. P -needed) member redex is contracted in P, in a DFS. The initial term (from which all histories start) will be clear from the context. For example, if P : t_{0}→^{u_{0}}t_{1}→^{u_{1}} … is an initial reduction, then

F AM(P) = ∪_{i}{F am(P_{i}u_{i})}, where P_{i} : t_{0}→^{u_{0}} … →^{u_{i−1}}t_{i}, and if Q is a non-initial

part of an initial reduction N = Q′ + Q, then F AM(Q) is the corresponding subset of F AM(N).

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

Proof

(⇒) Let w be a contracted redex in P, say P = P′ +w +P′′. Then w is Q/P′- needed. Hence F AM(P′w) ∈ 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′. Hence, by Proposition 7, 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; ·]
[figure: ·; Q′; ·; u′; ·]
[figure: ·; v; ·; v′; ·]

Lemma 16 Let u ∈ t → →^{P} and let u be P -needed, in an AZDFS. Then SF AM(P) = SF AM(P/u) ∪ {F am(∅u)}.

Proof Let v be a redex contracted in P that is not a residual of u, say P = P′ + v + P′′, and let v^{∗} = v/(u/P′) (see the diagram). Then it is enough to prove that F am(P′v) ∈ SF AM(P) iff F am((P′/u)v^{∗}) ∈ SF AM(P/u).

But the latter is immediate from Lemma 12.

[figure: t; P′; ·; v; ·; P′′; ·; u′; ·; s; u; P′/u; ·; v^{∗}; ·; ·; u′; ∅; ·; ∅]

Lemma 17 Let P be a (finite or infinite) reduction in an AZDFS. Then SF AM(P) = F AM(ST (P)).

Proof Immediate from Lemma 16 and Theorem 13.(1).

Lemma 18 (1) Let P ≈_{L} Q, in an AZDFS. Then SF AM(P) = SF AM(Q)

(or equivalently, ST (P) ≈_{ST A} ST (Q)).

(2) If both P and Q are finite, then the converse is also true.

Proof

(1) Let F am(P′u) ∈ SF AM(P), where P′ + u ≤ 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 12, 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 of (1) is immediate by Lemmas 15 and 17 (since ST (P) and ST (Q) are standard by Theorem 13).

(2) By Lemma 17, F AM(ST (P)) = F AM(ST (Q)), implying ST (P) ≈_{ST A} ST (Q) by Theorem 13 and Lemma 15. But P ≈_{L} ST (P) and Q ≈_{L} ST (Q) by Theorem 13.(2), and (2) follows.

The following proposition summarises our characterization of ≈_{L} via zig-zag families in Lemmas 15, 17 and 18:

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

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

(2) SF AM(Q) = F AM(ST (Q)) = SF AM(ST (Q)).

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

3.3 The Projection Concept

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

Definition 20 Let P and Q be co-initial reductions in an AZDFS. Then we call ST_{P} (ST (Q)) the projection of Q onto P, written Q|P.

Lemma 21 Let P, Q : t → → , in an AZDFS. Then the first residual of a P - needed redex in t that is contracted in Q (if any) is the first step of Q in SF AM(P).

Proof Let Q : t→^{u_{0}}t_{1}→^{u_{1}} …, let u_{i} be the first contracted residual of a P -needed redex in t, say of v ⊆ t, and let u_{j} be the first step of Q in SF AM(P). Since v is P -needed, its P -needed residual is contracted in P by Lemma 12, hence F am(u_{i}) ∈ SF AM(P). Therefore, j ≤ i. If u_{j} is a residual of a redex v′ ⊆ t, then F am(v′) ∈ SF AM(P), and by Proposition 7 the step of P in the family of v′ must be a residual of v′, thus v′ is P -needed by Lemma 12; therefore in this case i ≤ j by the minimality of i, hence i = j. Otherwise, if (an ancestor of) u_{j} is created by u_{k} (k < j), then by [creation] F am(u_{k}) ↪ F am(u_{j}); thus F am(u_{k}) ∈ SF AM(P) (since SF AM(P) = F AM(ST (P)) by Proposition 19.(2), and is downwards closed, w.r.t. ↪, by [contribution]), contradicting the minimality of j. Hence i = j and the lemma follows.

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

Proof Let Q : t_{0}→^{u_{0}}t_{1}→^{u_{1}} → …, let u_{i_{0}}, u_{i_{1}}, … be all steps of Q in SF AM(P)

(i_{0} < i_{1} < …), and let ST_{P} (Q) = v_{0} + v_{1} + . . .. Then by Lemma 16 and Lemma 21 we have the following situation:

[figure: t_{0} = s_{0}; t_{i_{0}}; u_{i_{0}}; ·; t_{i_{1}}; u_{i_{1}}; ·; t_{i_{2}}; Q_{0} = Q]
[figure: s_{1}; v_{0}; ·; u_{i_{0}}; ∅; ·; ∅; t_{i_{1}}; u_{i_{1}}; ·; t_{i_{2}}; Q_{1}]
[figure: s_{2}; v_{1}; ·; ∅; ·; ·; u_{i_{j}}; ∅; ·; ∅; t_{i_{2}}; Q_{2}]
s_{3} v_{2}_{}

where u_{i_{j}} is a residual of v_{j} along Q_{j} = Q/(v_{0} + … + v_{j−1}), and u_{i_{j}}, u_{i_{j+1}}, … are all steps of Q_{j} in SF AM(P_{j}), where P_{j} = P/(v_{0} + … + v_{j−1}). Hence F AM(ST_{P} (Q)) = F AM(Q) ∩ SF AM(P) and it remains to apply Proposition 19.(2).

Note in the above lemma that if Q is standard, then F AM(ST_{P} (Q)) = SF AM(Q) ∩ SF AM(P). The same holds if we require Q ⊴_{L} P instead of Q ∈ ST A; this can easily be shown using Lemma 11 and Lemma 12. The next example shows that the requirement that Q ⊴_{L} P or Q ∈ ST A is necessary for the above equation to hold.

Example 23 Let P = u and Q = u+v′, where v′ = v/u for some v and u/v = ∅. Then u is Q-unneeded, 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 24 Let P, Q be co-initial reductions in an AZDFS. Then P |Q is standard, and F AM(P |Q) = SF AM(P |Q) = SF AM(Q)∩SF AM(P). Hence P |Q ≈_{ST A} Q|P.

Lemma 25 Let P ≈_{L} P′ and Q ≈_{ST A} Q′, in an AZDFS. 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 22 and Proposition 19, implying by Proposition 19 and Theorem 13 that ST_{P} (Q) ≈_{L} ST_{P′}(Q′).

Corollary 26 The projection concept is invariant under ≈_{L}. (That is, if P, Q are co-initial reductions, in an AZDFS, such that P ≈_{L} P′ and Q ≈_{L} Q′, then P |Q ≈_{L} P′|Q′.)

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 23, and take Q′ = v. Then Q ≈_{L} Q′, Q|P = u, but Q′|P = ∅.

Remark 27 The (isomorphic) translation of an AZDFSs F into the corresponding PEESs C [17,20] interprets a reduction P in F into the configuration F AM(P) of C (families in F are events in C). Hence, by Corollary 24, the projection concept for configurations in PEESs can be defined as follows: α|β = ST (α) ∩ ST (β), where ST (α), the standard variant of α, is defined by ST (α) = {e ∈ α | α ⋫e}.

3.4 The Restriction Concept

We start with a simple definition.

Definition 28 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 29 (Restrictions of reductions to redex-sets) Let t be a term in an AZDFS F, let U ⊆ t, and let P : t → → .

(1) Assume first that P is finite and 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: t; P′|U; ·; v′; ·]
[figure: P′]
[figure: ·; P′|\overline{U}; P′|U/P′|\overline{U}; ·; P′|\overline{U}/P′|U; v; ·]

(2) Now let P be infinite and standard. Then P respects U iff every P^{∗} ≤_{fin} P does, and P |U is the reduction whose finite initial parts are of the form P^{∗}|U, for all P^{∗} ≤_{fin} P.

(3) We say that a (finite or infinite) 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 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 Proposition 32 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évyequivalence. The following simple example shows why this step 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 30 (1) Definition 29 is correct, that is, for any finite and standard

P in an AZDFS , P ≈_{ST A} P |U ⊔ P |\overline{U}.

(2) Furthermore, ST (P) ≈_{ST A} P |U ⊔ P |\overline{U} is true for any (finite or infinite) P as well. (In particular, P |U is P -needed and standard.)

Proof

(1) Assume first that P is finite and standard. 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 ≈_{L} (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. Finally, P |U ⊔P |\overline{U} is P -needed, hence standard, by Lemma 12, and (1) follows.

(2) If P is finite, then (2) follows immediately from (1) (since ST (P) is standard by Theorem 13, and P |U = ST (P)|U and P |\overline{U} = ST (P)|\overline{U} by Definition 29.(3)). So let P be infinite. Since, for any P^{∗} ≤_{fin} P, ST (P^{∗}) ≈_{ST A} P^{∗}|U ⊔ P^{∗}|\overline{U} ⊴_{L} ST (P)|U ⊔ ST (P)|\overline{U}, we have immediately, by definition of ⊴_{L}, that ST (P) ⊴_{L} ST (P)|U ⊔ ST (P)|\overline{U}. For the converse, let P′ ≤_{fin} ST (P)|U ⊔ ST (P)|\overline{U}. Then there is a reduction P^{′∗} ≤_{fin} P such that P′⊴_{L}ST (P^{′∗})|U ⊔ST (P^{′∗})|\overline{U} ≈_{L} ST (P^{′∗})⊴_{L}ST (P). Hence ST (P)|U ⊔ ST (P)|\overline{U} ⊴_{L} ST (P). Thus ST (P)|U ⊔ ST (P)|\overline{U} ≈_{L} ST (P) = P |U ⊔ P |\overline{U}. But ST (P)|U ⊔ ST (P)|\overline{U} is ST (P)-needed, hence standard, by Lemma 12, and the lemma follows.

As in the case of the projection concept (see Corollary 24), we need to give a characterization of the restriction concept via families in order to allow for simpler proofs in the sequel.

Notation 31 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_{0}^{+}(U) will denote the minimal set of families containing F AM_{0}(U) and closed under the contribution relation.

Proposition 32 Let U ⊆ t and P : t → → , in an AZDFS. Then P respects U iff SF AM(P) ⊆ F AM_{0}^{+}(U) ∪ F AM_{0}^{+}(\overline{U}). In the latter case, SF AM(P |U) = F AM(P |U) = SF AM(P) ∩ F AM_{0}^{+}(U) and SF AM(P) = F AM(P |U) ∪ F AM(P |\overline{U}).

Proof By Proposition 19 and Definition 29, we can assume that P ∈ ST A. Furthermore, we can assume that P is finite. Then the first part is proved by induction on |P | by simply using Definition 29. And F AM(P |U) = F AM(P)∩ F AM_{0}^{+}(U) and F AM(P) = F AM(P |U) ∪ F AM(P |\overline{U}) also follow immediately from Definition 29 by induction on |P |, since P, P |U, P |\overline{U} ∈ ST A by Lemma 30.

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

Proof By Proposition 32 and Proposition 19 (since P |U, Q|U are standard by Lemma 30).

The restriction concept enjoys nice algebraic properties:

Lemma 34 Let P : t → → respect U_{1}, U_{2} ⊆ t, in an AZDFS. 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 By Definition 29, we can assume that P is standard and finite.

(1) Since P respects U_{i}, we have by Proposition 32 that ∀ϕ ∈ F AM(P) : ϕ ∈ F AM_{0}^{+}(U_{i})∨ϕ ∈ F AM_{0}^{+}(\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 Proposition 32 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 11 and Lemma 12. 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_{0}^{+}(U_{1} ∪ U_{2}) \ (F AM_{0}^{+}(U_{1}) ∪ F AM_{0}^{+}(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 Proposition 32 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 19 that P |U_{1} ∪U_{2} ≈_{ST A} P |U_{1} ⊔P |U_{2} (since P |U_{1} ∪ U_{2}) is standard by Lemma 30).

(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 33. Finally, we have by Proposition 32 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 19 and Lemma 30.

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

Remark 35 Let α be a configuration in a PEES C and let X be a set of initial events in C. By Proposition 32, we can define that α respects X if ST (α) ⊆ ⌈X^{≥}⌉ ∪ ⌈\overline{X}^{≥}⌉, and in the latter case, define α|X = ST (α) ∩ ⌈X^{≥}⌉, where ⌈X^{≥}⌉ = {e | ∃e′ ∈ X : e ≥ e′}.

3.5 The Decomposition Theorem

The following lemma relates the restriction and projection concepts:

Lemma 36 Let U ⊆ t, in an AZDFS , and let P and \overline{P} be 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 Proposition 32 and Corollary 24 that F AM((P ⊔ \overline{P})|U) = SF AM(P ⊔ \overline{P}) ∩ F AM^{+}(U) = (by Definition 10, since \overline{P} is external to U) F AM(P)∩SF AM(P ⊔\overline{P}) = (since P ⊔\overline{P} -needed redexes contracted in P are P -needed by Lemma 11) = SF AM(P) ∩ SF AM(P ⊔ \overline{P}) = SF AM(P |P ⊔ \overline{P}). Now the lemma follows from Proposition 19 and Corollary 24.

Definition 37 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 38 Let ℑ = {U_{i}}_{i∈I} be a redex-covering of a term t in an AZDFS F.

(1) Let P_{i} be 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 → → respect ℑ. Then ST (P) ≈_{ST A} ⊔_{i}P |U_{i}. If moreover P is finite, 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 36 and Lemma 33, 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 34.(1) that ST (P) ≈_{ST A} P |(U_{1} ∪ … ∪ U_{n}) ≈_{ST A} P |U_{1} ⊔ P |(U_{2} ∪ … ∪ U_{n}) ≈_{ST A} … ≈_{ST A} P |U_{1} ⊔ … ⊔ P |U_{n}. If moreover P is finite, then we apply Theorem 13.(2).

Now Remark 6 allows us to derive a counterpart of Theorem 38 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 39 (Restrictions of complete family-reductions to redexsets) Let t be a term in a DFS F, let U ⊆ t, and let P : t → → be a complete family-reduction

(1) Assume first that P is finite and standard. 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) or ft(P′|\overline{U}), respectively, 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: t; P′|U; ·; V′; ·]
[figure: P′]
[figure: ·; P′|\overline{U}; P′|U/P′|\overline{U}; ·; P′|\overline{U}/P′|U; V; ·]

(2) Now let P be infinite and standard. Then P respects U iff every complete family-reduction P^{∗} ≤_{fin} P does, and P |U is the complete family-reduction reduction whose finite initial parts are of the form P^{∗}|U, for all P^{∗} ≤_{fin} P.

(3) We say that a 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. It is shown in [18,19] that in any DFS: (a) if U, V ⊆ s are complete sets of redexes of families ϕ and ψ in s, respectively, and s → →^{V} o, then U′ = U/V is the complete set of redexes of ϕ in o. And this ensures that the swapping of multi-steps can be done ‘safely’. (Clearly, a sequentialization of a standard multi-step reduction need not be a standard reduction.) The meanings of ≤_{fin}, ST ( ) and ≈_{ST A} for multi-step reductions change respectively. Again from the property (a) above we know that, in the above definition, it is correct to take for V′ the set of all redexes in ft(P′|U) (respectively, ft(P′|\overline{U})) in the family of V as such a V′ is a (complete) family multi-step.

Thus, we can equivalently define the relative standardization, projection, and restriction concepts for complete family reductions in a DFSs F by first mapping the corresponding complete family-reductions onto reductions in the corresponding AZDFS F_{I}, then performing the corresponding operations on these reductions, in F_{I}, and finally mapping the result back onto the corresponding complete family-reduction in F. Hence the following is a corollary of Theorem 38.

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

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

(2) Let P : t → → be a complete family-reduction that respects ℑ. Then ST (P), P |U_{i} are complete family-reductions such that ST (P) ≈_{ST A} ⊔_{i}P |U_{i}. If moreover P is finite, then P ≈_{L} ⊔_{i}P |U_{i}.

Remark 41 The Decomposition Theorem has its counterpart in PEESs. Let ℑ = {X_{i}}_{i∈I} be a covering of the set of initial events in a PEES C.

(1) Let α ⊆ ⌈X_{i}^{≥}⌉, i ∈ I, and let α = ∪_{i∈I}α_{i}. Then α respects (all sets in) ℑ and α|X_{i} = α|α_{i}.

(2) Let α respect ℑ. Then ST (α) = ∪_{i∈I}(α|X_{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 42 Let P : t → → . We call the strict domain of P, 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évy-equivalent 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 with all P -erased redexes not contracted in P; MDom(P) is the set of all P -needed redexes in t; and Dom(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 13 (and also from Proposition 19 in the finite case) that MDom(P) = SDom(ST (P)) for any P.

Definition 43 We call a U-reduction P U-fair if each U-redex in a term in P is erased in P, and call P 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 44 A U-reduction P, in an AZDFS , is U-fair iff it is strongly Ucofinal.

Proof

(⇒) Let Q be a U-reduction. We want to show that Q⊴_{L}P. Suppose it is not. It follows from the definition of Q ⊴_{L} P (for possibly infinite reductions P, Q) that Q has the form Q = Q′ + u + Q′′, where Q′/P = ∅ and u/(P/Q′) ≠ ∅. Let P = P′ + P′′, where P′ is finite and Q/P′ = ∅ (such a P′ must exist by definition of ⊴_{L}), and let u′ = u/(P′/Q′) (see the figure). Then by U-fairness of P, u′/P′′ = ∅ (note that u′ is a redex in a term in P), contradicting u/(P/Q′) ≠ ∅.

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

[figure: ·; Q′; P′/Q′; ·; ∅; P′′]

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

(⇐) 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 below, 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. See [21] for the proof.

Lemma 45 Let Q and P be co-initial reductions in an AZDFS F. Then Q|P ≈_{ST A} (Q|MDom(P))|P. If moreover SF AM(P) = F AM_{0}^{+}(MDom(P)) (e.g., if F is linear and P is MDom(P)-fair), then Q|P ≈_{ST A} Q|MDom(P).

Definition 46 (The Reduction Geometry) Let an AZDFS F be given.

• Two co-initial reductions P : t → → s and Q : t → → e are said not to interact, written P ⊥ Q, if, first, MDom(P)∩MDom(Q) = ∅, and, second, any created redex in ft(P ⊔ Q) is a residual of a redex either from ft(P) or from ft(Q). Otherwise, we say that P and Q (with MDom(P)∩MDom(Q) = ∅0 interact, written 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 P′_{i} ≤_{fin} P_{i}. We call Π a basis of F at t if Π is independent and ⊔P_{i} is maximal w.r.t. ≤.

• 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 [12,13] (or equivalently, Maranget-needed [29]) 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 no (finite) U-reduction interacts with a \overline{U}- reduction. We call ℑ = {U_{i}}_{i∈I} an independent covering if ℑ is a covering of t and each U_{i} is independent.

Example 47 (Bases) Consider a term t containing three redexes u, v, w, let w/(u ⊔ v) = ∅, w/u ≠ ∅, w/v ≠ ∅, and assume no redex 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 Π_{i} 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) = ∅.

Definition 48 (Externality) Let P : t_{0} → →^{P_{i}} t_{i}→^{u_{i}}t_{i+1} → → t_{n} and Q : t_{0} =

s_{0} → →^{Q_{j}} s_{j}→^{v_{j}}s_{j+1} → → s_{m}. Let U_{i,j} = u_{i}/(Q_{j}/P_{i}) and V_{i,j} = v_{j}/(P_{i}/Q_{j}) (see

diagram). We call P external to Q if for any i, j, U_{i,j} ∩ V_{i,j} = ∅.

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

[figure: s_{j}; Q_{j}; P_{i}/Q_{j}; ·; Q_{j}/P_{i}; U_{i,j}; ·]

[figure: s_{j+1}; v_{j}; ·; V_{i,j}; ·]

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

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)) (the Cube Lemma implies that ⊥ is invariant under Lévy-equivalence), which is impossible by the Stability Lemma ^{3} (since MDom(P) ∩ MDom(Q) = ∅ implies that ST (P) and ST (Q) are external).

In general, SDom(P) ∩ SDom(Q) = ∅ implies that P and Q are external, but not conversely. For example, let t = u = (λz.Kyz)v, where K = λx.λy.x; then

P : t→^{u}Kyv→^{v}Kyo and Q : t → →^{K} (λz.y)v→^{v}(λz.y)o are external since v does

not have u ⊔ K-residuals, while SDom(P) ∩ SDom(Q) = {v} ≠ ∅.

Note also that, if P ⊥ Q, Dom(P) ∩ Dom(Q) = ∅ need not hold: Consider the modified example from [28], taking t = (λx.K_{a}(xu))K_{b} where K_{a} = λx.a,

3 The Stability Lemma [6,19] states that if P : t → → s is external to Q : t → → e, in an SDRS, and P creates 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.

K_{b} = λx.b, and u is a redex, and consider 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: 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 ≈_{E} Q iff EF AM(P) = EF AM(Q), where EF AM(P) denotes the set of families of essential redexes in P. Clearly, ≈_{E} is an equivalence relation, and the (co-initial) reduction space quotiented w.r.t. it is a metric, as |P, Q| = 0 implies P ≈_{E} Q. Note that ≈_{L}⊆≈_{E}, 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 49 In an AZDFS , U ⊆ t is independent iff any reduction P : t → → respects it.

Proof By Definition 29, we can assume that P is standard and finite.

(⇒) Suppose on the contrary that not every reduction starting from t respects 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 30. 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 (since by the Cube Lemma u is a created redex), i.e., U is not independent.

(⇐) 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, say (N ⊔ Q)|U ⊔ (N ⊔ Q)|\overline{U} + u does not respect U.

Proposition 50 Let U_{1}, U_{2} ⊆ t be independent, in an AZDFS. Then so are U_{1} ∪ U_{2}, U_{1} \ U_{2}, and U_{1} ∩ U_{2}.

Proof Immediate from Lemma 34 and Lemma 49.

Theorem 51 Let ℑ = {U_{i}}_{i∈I} be an independent redex-covering of a term t in an AZDFS F, let P : t → → , and let P_{i} be U_{i}-fair. Then ST (P) ≈_{ST A} ⊔_{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 ST (P) ≈_{ST A} ⊔_{i}P′_{i}. If moreover P is finite, then P ≈_{L} ⊔_{i}P |U_{i} ≈_{L} ⊔_{i}P′_{i}.

Proof Since ℑ is an independent covering of t, P respects ℑ by Lemma 49, and ST (P) ≈_{ST A} ⊔_{i}P |U_{i} follows from Theorem 38.(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 44. Hence P ⊴_{L} ⊔P_{i}. It follows immediately from Definition 46 that B is independent, thus is a basis at t, and we can take P |U_{i} for P′_{i}. If moreover P is finite, then we apply Theorem 13.(2).

By Remark 6, Definition 46 induces the concepts of a basis, an independent redex-covering, etc. for complete family-reductions in DFSs. Hence the following is an immediate corollary of Theorem 51.

Corollary 52 (Independent Decomposition Theorem) Let ℑ = {U_{i}}_{i∈I} be an independent redex-covering of a term t in a DFS F, let P : t → → be a complete family-reduction, and let P_{i} be U_{i}-fair complete family-reductions. Then P |U_{i} are complete family-reductions such that ST (P) ≈_{ST A} ⊔_{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 ST (P) ≈_{ST A} ⊔_{i}P′_{i}. If moreover P is finite, then P ≈_{L} ⊔_{i}P |U_{i} ≈_{L} ⊔_{i}P′_{i}.

We have seen in Example 47 that not all bases are of the form described in Theorem 51. 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 and 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 in order to avoid a trivial concept of independence (see also the introduction). Also in the case of 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 AZDFS 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. Theorem 51 and Proposition 50 allow us to construct finer independent coverings and finer bases from existing ones, as if ℑ = {U_{i}}_{i∈I} and ℑ′ = {U′_{j}}_{j∈J} are independent coverings, then ℑ ∩ ℑ′ = {U_{i} ∩ U′_{j}}_{(i,j)∈(I,J)} is a one too. Thus t has a unique finest independent covering (consisting of finest independent redex sets). ^{4}

4 It is interesting to note that for any redex P u, the history of an extraction normal form of P u [18] is internal to some finest independent set of redexes in t.

We conclude this section by translating the concept of Reduction Geometry and Theorem 51 in the terminology of PEESs.

Definition 53 Let a PEES C = (E, ≤, ⊳) be given.

• We say that two configurations α and β do not interact, written α ⊥ β, if, first, Init(ST (α)) ∩ Init(ST (β)) = ∅, and, second, for any event e such that α ∪ β ∪ {e} is a configuration, at least one of α ∪ {e}, β ∪ {e} is a cofiguration too. Otherwise, α and β interact, written α ⊥̸ β.

• We call a set Π = {α_{i}}_{i∈I} of configurations independent if α′_{i} ⊥ ∪_{j≠i}α′_{j} for any i ∈ I and α′_{i} ⊆_{fin} α_{i}. We call Π a basis for C if it is independent and α ⊆ ∪_{i∈I}α_{i} for any configuration α.

• An event e is called essential if α ⋫e for any configuration α. The distance ∥α, β∥ between α and β is the number of essential events that belong to either α or β (but not to both).

• The independence degree of X ⊆ Init(E) is the cardinality of a smallest configuration α ⊆_{fin} ⌈X^{≥}⌉ such that there exists a configuration β ⊆_{fin} ⌈\overline{X}^{≥}⌉ that interacts with α, and is ∞ otherwise. (Here \overline{X} = Init(E) \ X.)

• We call X ⊆ Init(E) independent if for any configurations α ⊆_{fin} ⌈X^{≥}⌉ and β ⊆_{fin} ⌈\overline{X}^{≥}⌉, one has α ⊥ β. We call a collection ℑ = \{X_{i} | X_{i} ⊆_{fin} Init(E)}_{i∈I} an independent covering of E if Init(E) ⊆ ∪_{i∈I}X_{i} and each X_{i} is independent.

Theorem 54 Let C = (E, ≤, ⊳) be a PEES, let ℑ = {X_{i} | X_{i} ⊆_{fin} Init(E)}_{i∈I} be an independent covering of E, and let α_{i} = ⌈X_{i}^{≥}⌉. Then for any configuration α, ST (α) = ⊔_{i}α|X_{i}. Further, B = {α_{i}}_{i∈I} is a basis for C, and there are configurations α′_{i} ⊆_{fin} α such that ST (α) = ∪_{i}α′_{i}. If moreover α is finite, then α = ⊔_{i}α|X_{i} = ∪_{i}α′_{i}.

5 The Optimal Decomposition Theorem

In this section, we recall results concerning relative normalization in DFSs from [6,19], 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 55 ([4,5]) Let S be a set of terms in an SDRS R.

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

(2) We call a set S of terms stable if:

(a) S is closed under reduction: t ∈ S and t → s implies s ∈ S;

(b) S is closed under unneeded expansion: for any e→^{u}o such that e ∉ S

and o ∈ S, u is S-needed.

As already mentioned in the introduction, stability of a set of ‘values’ is a natural sufficient condition for a normalization theory via needed reduction to be developed. The most important examples of stable sets are normal forms, head-normal forms and weak-head-normal forms in the λ-calculus, and root stable forms in orthogonal TRSs. Many more examples can be found in [19]. The following theorem combines the Relative Normalization and Optimality Theorems for DFSs [6,19]).

Theorem 56 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 an S-needed redex, and any S-needed reduction starting from t is eventually S-normalizing, even if finite sequences of consecutive S-unneeded steps are also allowed. Furthermore, any S-needed S-normalizing complete-family reduction starting from t is shortest among S-normalizing family-reductions starting from t.

The concepts introduced in Definition 46 (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; by replacing ‘(essential) redex’ with ‘S-needed redex’, and by replacing ’maximal w.r.t. ≤’ with S-normalizing. In the definition of Relativized Geometry, below, we will omit definitions of Sdistance and S-independence degree since we will not need these in the sequel. The definition then makes sense for all SDRSs.

Below S will always denote a stable set of terms in a DRS. Further, we will only consider S-normalizable terms (since if a term is not S-normalizable all redexes in it are trivially S-needed). Note that the set of S-normalizable terms is closed under reduction (by CR and the closure of S under reduction).

Definition 57 The S-domain of a reduction P in a DRS, written Dom_{S}(P), is the set of S-needed redexes in MDom(P).

Definition 58 (Relativized Reduction Geometry) Let t be a term in an AZDFS F.

• Two co-initial reductions P : t → → s and Q : t → → e are said not to S-interact, written P ⊥_{S} Q, if, first, Dom_{S}(P)∩Dom_{S}(Q) = ∅, and, second, 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, we say that P and Q (with Dom_{S}(P)∩Dom_{S}(Q) = ∅) 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 P′_{i} ≤_{fin} P_{i}. We call Π an S-basis of F at t if Π is S-independent and ⊔_{i∈I}P_{i} is S-normalizing.

• We call U ⊆ t S-independent if no (finite) U-reduction can S-interact with an \overline{U}-reduction. We call ℑ = \{U_{i}\}_{i∈I} an S-independent covering of t if ℑ is a covering of the set U_{S}(t) of S-needed redexes in t and each U_{i} is S-independent.

It is easy to see that Dom_{S}(P) = SDom(P) ∩ U_{S}(t) = Dom(P) ∩ U_{S}(t). This follows from the following lemma:

Lemma 59 Let u ⊆ t → →^{P} , in an AZDFS, and let u be P -erased and P - unneeded. Then it is S-unneeded (i.e., every step of P is S-unneeded).

Proof 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 55); 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 any reduct of an S-normalizable term remains S-normalizable).

In [6,19], we defined an algorithm which associates with a reduction P an Sneeded 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 ones. Thus it applies for any stable set S in an AZDFS, 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 Sunneeded steps, which is possible by the following lemma:

Lemma 60 ([6,19]) Let t ∉ S, in a DFS F.

(1) Residuals of S-unneeded redexes in t remain S-unneeded.

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

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

Since any S-needed reduction P in an AZDFS is standard by Lemma 59, SDom([P]_{S}) = MDom([P]_{S}). Using this observation, we can give an equivalent definition of S-interaction using S-needed reductions:

Lemma 61 Let P, Q be finite co-initial reductions in an AZDFS. Then P and Q S-interact iff [P]_{S} and [Q]_{S} do.

Proof We need to show that P ⊥_{S} Q iff MDom([P]_{S}) ∩ MDom([Q]_{S}) = ∅ and any created S-needed redex in ft([P]_{S} ⊔[Q]_{S}) is a residual of an S-needed redex created by [P]_{S} or by [Q]_{S}. 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 60.(1)-(2) 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 60.(3). Finally, if u is a residual of a redex u^{∗} say in ft(P), then by Lemma 60.(1)-(2) u^{∗} is S-needed and is a residual of an S-needed u^{′∗} ∈ ft([P]_{S}), and u′ is a residual of u^{′∗} by Proposition 7 (as u′ and u^{′∗} are zig-zag related). Conversely, if an S-needed redex u′ ∈ ft([P]_{S} ⊔ [Q]_{S}) is a residual of u^{′∗} ∈ ft([P]_{S}), then by Lemma 60 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 Proposition 7, and we are done.

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

Similar reformulations can be given for the other concepts of the relativized geometry.

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.

Lemma 62 In an AZDFS , U ⊆ t is S-independent iff any S-needed reduction P : t → → respects it.

Proof First note that P is finite by Theorem 56 (since we only consider S-normalizable terms t), and it is standard by Lemma 59.

(⇒) Suppose on the contrary that not every S-needed reduction starting from t respects U, and let P = P′ + u be a shortest one. Since P′ respects U, we have that P′ ≈_{ST A} P′|U ⊔ P′|\overline{U} by Lemma 30. 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} S-interact (since by the Cube Lemma u is a created redex, and it is S-needed), i.e., U is not S-independent.

(⇐) Let U not be S-independent. Then there are reductions N and Q respectively internal and external to U that S-interact, i.e., there is a created S-needed redex u in ft(N ⊔ Q) that is not a residual of a redex either in ft(N) or in ft(Q). By Lemma 61, N and Q can be chosen S-needed, and so is N ⊔ Q by Lemma 60.(3). If N ⊔ Q does not respect U, then we are done. Otherwise, say (N ⊔ Q) + u does not respect U.

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

Definition 63 Let U ⊆ t, in a DRS R. 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 64 Let ℑ = {U_{i} | i ∈ I} be an S-independent covering of t, in an AZDFS.

(1) 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.

(2) 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

(1) By Definition 29, P_{i} is an U_{i}-reduction, and it contracts residuals of redexes contracted in P, hence is S-needed by Lemma 60.(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. Let \overline{P_{j}} = P |\overline{U_{j}}. By Lemma 62, P respects U_{j} (and \overline{U_{j}}), hence by the Decomposition Theorem P ≈_{L} P_{j} ⊔ \overline{P_{j}}. Hence \overline{P_{j}}/P_{j} : t → → s and it is external to v, thus by Lemma 60.(3) v has an S-needed residual in s – contradiction, since s ∈ S.

(2) Since every P_{i} is S-needed, so is P by Lemma 60.(3). Since ℑ = {U_{i} | i ∈ I} is an S-independent covering of t and P_{i}⊔\overline{P_{i}} ≈_{L} P, where \overline{P_{i}} = ⊔_{j≠i}P_{j}, every S-needed redex in s is a \overline{P_{i}}/P_{i}-residual of an S-needed (by Lemma 60.(1)) redex in s_{i}, for some i (it can be shown using Proposition 32 that \overline{P_{i}} ≈_{L} P |\overline{U_{i}}). Since every P_{i} is an (U_{i}, S)-fair U_{i}-reduction, any S-needed redex u ⊆ s_{i} is a residual of an S-needed (by Lemma 60.(1)) redex v ∈ U_{j} for some j ≠ i. 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}}/P_{i}-residuals. Thus s does not contain S-unneeded redexes, and by Theorem 56, s ∈ S.

Lemma 65 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 60.(2), all the redexes in o created by u/P are S-unneeded. Again by Lemma 60.(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 66 Let U ⊆ t contain an S-needed redex, in an AZDFS F. A reduction starting from t is a shortest (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|. Since U contains an S-needed redex, |Q|, |P | ≠ 0. So let Q : t→^{v}s → →^{Q′} e. Since v is S-needed and P is (U, S)-fair, it follows from Lemma 60.(3) that the residuals of v along P are S-needed, hence P must contract one of them. Hence, by affineness, |P′| ≤ |P | − 1, where P′ = P/v. Let U′ be the set of U-redexes in s. Then, by Lemma 65, 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 |. So let P = u+P′ (we already know that |Q|, |P | ≠ 0). Since Q is S-needed, so is Q′ = Q/u by Lemma 60.(3). Suppose first that u is S-unneeded. Then so is every residual of it along Q by Lemma 60.(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 65, 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 |.

Now, as an immediate consequence of Lemma 64, Theorem 56, and Lemma 66, we have the following Optimal Decomposition Theorem for AZDFSs:

Theorem 67 Let S be a stable set of terms in an AZDFS 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 reductions iff P = ⊔_{j}P_{j} is an optimal S-normalizing reduction starting from t.

It is shown in [18,19] that S-needed complete family-reductions in a DFS F precisely correspond to S_{I}-needed reductions in the corresponding AZDFS 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 6 and Theorem 67 the following Optimal Decomposition Theorem for DFSs:

Corollary 68 (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 Sneeded redex of t, and let P_{j} be complete family-reductions internal to U_{j}. Then P_{j} are optimal (U_{j}, S)-fair complete family-reductions iff P = ⊔_{j}P_{j} is an optimal S-normalizing complete family-reduction starting from t.

Given a reduction N : t_{0}→^{v_{0}}t_{1}→^{v_{1}} … t_{n} in a DFS F, one can construct its corresponding complete family-reduction N^{c} : t_{0} = s_{0} → →^{V_{0}} s_{1} → →^{V_{1}} … s_{n}, where F am(v_{k}) = F am(V_{k}) for all k = 1, …, n; ∃N′_{k} : t_{k} → → s_{k} such that N_{k}^{c} ≈_{L} N_{k} + N′_{n}, and N_{k}^{c} and N_{k} are the initial parts of N^{c} and N of length k; and V_{k} contains all residuals of v_{k} in s_{k}, and possibly other redexes too. (Because of ersure of redexes, some of V_{k} may be empty if v_{k} is not S-needed.) Hence F AM(N) ⊆ F AM(N^{c}). Furthermore, if N is internal to W ⊆ t_{0}, then so is N^{c}, and if N is (W, S)-fair, so is N^{c}, and the reduction N′_{n} : t_{n} → → s_{n}, henceforth denoted N^{−}, is S-unneeded.

Using the above observations, we now show that one does not need to restrict to complete family-reductions in order to be able to compute independent redex sets of an S-normalizing term in parallel:

Theorem 69 (Relative independent 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 Q_{j} be reductions internal to U_{j}. Then Q_{j} are (U_{j}, S)-fair reductions iff ⊔_{j}Q_{j} is an S-normalizing reduction starting from t.

Proof

(⇒) Since all Q_{j} are (respectively) (U_{j}, S)-fair, so are all Q_{j}^{c}, and hence ⊔_{j∈J}Q_{j}^{c} is S-normalizing by Corollary 68. But Q_{j}^{c} ≈_{L} Q_{j} +Q_{j}^{−}, where Q_{j}^{−} are S-unneeded, and by Lemma 60 ⊔_{j∈J}Q_{j}^{c} ≈_{L} ⊔_{j∈J}Q_{j} + Q′ for some S-unneeded Q′. Since S-unneeded steps cannot enter S, ⊔_{j∈J}Q_{j} is S-normalizing.

(⇐) If at least one Q_{j_{0}} is not (U_{j_{0}}, S)-fair, then ft(Q_{j_{0}}) contains an S-needed U_{j_{0}}-redex, which must have an S-needed residual in ft(⊔_{j}Q_{j}) by Lemma 60 (since by the family axioms Q_{j} contract redexes in different families). Hence ft(⊔_{j}Q_{j}) ∉ S by Theorem 56.

As we have already remarked above, the definition of S-independence in Definition 58 makes sense for any co-initial reductions in DFSs (not only for complete family-reductions). And it is easy to see that N ⊥_{S} P iff N^{c} ⊥_{S} P^{c} (since every jointly created S-needed redex in ft(N ⊔ P), if any, has an S-needed residual in ft(N^{c} ⊔ P^{c}), by the construction of N^{c} and P^{c}). Thus, in the above theorem, ℑ = {U_{i}}_{i∈I} is an S-independent covering of t iff no reduction internal to U_{i} interacts with a reduction external to U_{i}, for every i ∈ I. Using this fact, a more direct proof of Theorem 69, similar to the proof of Lemma 64, can also be given.

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

For example, all the introduced concepts are decidable for Recursive Program Schemes (RPSs), both in first [13] and higher order [14] cases. Several kinds of RPS were extensively studied in the literature, mainly in the seventies [3]. Our (first-order) RPSs correspond to Applicative RPSs in [3]. 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 [14] 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 the latter can 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 higher-order 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 [22]. 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 normalizable, and in such terms all unneeded (or rather, inessential) subterms can be statically detected. Among other things, these properties arise from the fact that only two, of the three kinds of redex-creation in the λ-calculus [26], are possible in the setting of hyperbalanced terms. As 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 the 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 technique for evaluating redexes independently from each other in hyperbalanced terms is not known at present.

Finally, we remark that there is an obvious relationship between the independence concept and modularity of properties in TRSs (see [24] for a survey) which we think is worth investigating. For example, in the simple case where 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 [33].

Acknowledgments We thank J. R. Kennaway, V. van Oostrom, F.-J. de Vries, and the annonymous referees for useful comments. The diagrams were drawn using P. Taylor’s diagram package.

References

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

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

[3] B. Courcelle, Recursive applicative program schemes, in: J. van Leeuwen, ed., Handbook of Theoretical Computer Science, Vol. B (Elsevier, Amsterdam, 1990) 459-492.

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

[5] J.R.W. Glauert, J.R. Kennaway and Z. Khasidashvili, Stable results and relative normalization. Submitted for publication.

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

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

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

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

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

[11] J.R. Kennaway, J.W. Klop, M.R. Sleep and F.-J. de Vries, On the adequacy of graph rewriting for simulating term rewriting, ACM Transactions on Programming Languages and Systems 16(3) (1994) 493-523.

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

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

[14] Z. Khasidashvili, On higher order recursive program schemes, in: Proc. CAAP’94, Lecture Notes in Computer Science, Vol. 787 (Springer, Berlin, 1994) 172-186.

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

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

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

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

[19] Z. Khasidashvili and J.R.W. Glauert, An abstract theory of optimal evaluation (currently under revision). Available on request.

[20] Z. Khasidashvili and J.R.W. Glauert, Relating conflict-free stable transition and event models (Journal submission). Available on request.

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

[22] Z. Khasidashvili and A. Piperno, Normalization of typable terms by superdevelopments, in: Proc. CSL’98, Lecture Notes in Computer Science, vol. 1584, (Springer, Berlin, 1999) 260-282.

[23] J.W. Klop, Combinatory Reduction Systems (Mathematical Centre Tracts no. 127, Amsterdam, 1980).

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

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

[26] J.-J. Lévy, An algebraic interpretation of the λβκ-calculus and a labelled λcalculus, Theoret. Comput. Sci. 2 (1976) 97-114.

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

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

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

[30] R. Milner, Functions as processes, Mathematical Structures in Computer Science 2(2) (1992) 119–141.

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

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

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

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

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