Stable Computational Semantics of Conflict-free Rewrite Systems (Partial Orders with Duplication)

Zurab Khasidashvili^{1} and John Glauert^{2}

1 Logic and Validation Technology Design Technology Division Intel, IDC, Haifa, Israel

                      Zurab.Khasidashvili@intel.com

2 School of Computing Sciences, UEA Norwich NR4 7TJ, UK

                           J.Glauert@uea.ac.uk

Abstract. We study orderings ⊴_{S} on reductions in the style of Lévy reflecting the growth of information w.r.t. (super)stable sets S of ‘values’ (such as head-normal forms or Böhm-trees). We show that sets of co-initial reductions ordered by ⊴_{S} form finitary ω-algebraic complete lattices, and hence form computation and Scott domains. As a consequence, we obtain a relativized version of the computational semantics proposed by Boudol for term rewriting systems. Furthermore, we give a pure domain-theoretic characterization of the orderings ⊴_{S} in the spirit of Kahn and Plotkin’s concrete domains. These constructions are carried out in the framework of Stable Deterministic Residual Structures, which are abstract reduction systems with an axiomatized residual relations on redexes, that model all orthogonal (or conflict-free) reduction systems as well as many other interesting computation structures.

1 Introduction

The idea of representing or identifying a process (or a program, or a term) with the domain of all its computations is not new in semantics: for example, this idea is central in the study of event structure semantics of programming languages extensively developed by Winskel, Nielsen and Plotkin [Win80,NPW81,Win89]. Berry and Lévy [BL79] were the first who tried to base algebraic semantics [NR85] of recursive programs on an ordering on the set of computations rather than on the set of terms; they used Lévy’s [Lév78,Lév80] embedding relation ⊴_{L} on reductions for that purpose, which we will explain shortly; the transitive and reflexive closure of ⊴_{L} yields Lévy- or permutation-equivalence ≈_{L} on reductions. Permutation-equivalent reductions result from one another by permuting concurrent consecutive steps, hence the name. Developing this ideas further, Boudol [Bou85] proposed a computational approach to semantics of term rewriting systems [DJ90,Klo92] in general. Boudol’s idea was to define the semantics of a term t in a term rewriting system (Σ, R) (where Σ is an alphabet and R is a set of rewrite rules) via the set of ≈_{L}-classes of all ⊴_{L}-maximal computations starting from t. In the case of deterministic (or conflict-free or orthogonal) TRSs, a term has exactly one (up to ≈_{L}) ⊴_{L}-maximal computation, which corresponds to a fair computation [Klo92]. To support his computational approach to semantics, Boudol defined interpretations of TRSs in the usual algebraic style (i.e., the class of interpretations coincides with the class of Σ-algebras) and showed that the computational semantics coincides with the algebraic one.

However, Boudol [Bou85] remarked that, besides being a cpo, “⊴_{L} seems to have generally no ‘good’ properties (even for deterministic TRSs)”. To clarify the problem, we observe that, according to Kahn and Plotkin [KP93], a ‘good’ domain into which to interpret programs must be at least coherent and ω-algebraic; they call such domains computation domains.^{3} And according to Scott [Sco82], ‘good’ domains are consistently complete ω-algebraic cpos; such domains are called Scott domains. To quote Plotkin, ‘Algebraicity is an important idea which formalizes some intuitive ideas of finiteness and objects as limits of their finite approximations. Algebraicity allows definitions of computability to provide links with recursion function theory and allow results on definability. It allows easy consideration of constructions as powerdomains and enables us to visualise domains as completions of structures of finite information’ [Plo83]. Further, Kahn and Plotkin [KP93], Girard [Gir87], Winskel [Win89], and many others argue that it is reasonable to require ‘good’ domains to be finitary, because in this way finite elements are ‘really’ finite, i.e., represent only a finite amount of information (built up from a finite number of components), and thus cannot be decomposed infinitely. But ⊴_{L} is not finitary, and the ⊴_{L}-glb of two finite elements needs not be finite. To recover ‘good’ properties of the reduction space, Boudol [Bou85] studied the sub-space of all strongly needed reductions [HL91] and proved that a reduction space thus restricted is finitary and ω-algebraic, and conjectured that it corresponds to the domain of configurations of an event structure and moreover forms a concrete domain [KP93].

There had been other similar proposals to construct domains with rich algebraic properties out of the reduction space of a reduction system. For example, in order to construct an event structure semantics for orthogonal (term graph) rewriting systems with non-duplicating residual relation, Kennaway et al. [KKSV93] restrict themselves to needed reductions of normalizable terms; the resulting domain is finitary and distributive (or equivalently, prime algebraic). Finitary distributive domains (also called dI-domains or stable domains) are exactly domains of configurations/states (ordered by the subset relation) generated by stable event structures [Win80,NPW81,Win89], and are commonly accepted domains to model concurrency. Melliès [Mel97] restricts himself to external [HL91] reductions, after having factorised any reduction into an external part followed by an internal reduction, similar to often used factorization of reductions into needed and unneeded parts. In the case of deterministic systems, all external redexes are needed, and strongly needed redexes are all external.

Thus in all these cases, a linear subspace of reductions is identified on which ⊴_{L} forms dI-domains. This works because event structures are equivalent to linear reduction systems (where there is no erasure or duplication of redexes): in linear systems, ⊴_{L} corresponds to the subset ordering on states of an event structure, all permutation-equivalent reductions correspond to the same state, prime intervals of the event structure represent reduction steps [Win89], and events can be seen as equivalence-classes of prime-intervals [Win89], which are nothing but zig-zag-classes [Lév78,Lév80] of the corresponding reduction steps [Cur86]. This correspondence is further extended in [KG98] (for the case of stable conflictfree systems), where prime event structures (which are equivalent to stable ones [Win89]), with an axiomatized erasure relation, are defined. These are to non-duplicating reduction systems what event structures are to linear ones.

In order to achieve a stable event structure semantics, or equivalently, to construct a dI-domain out of a reduction space, rather than restricting the re-

3 Definitions of all order-theoretic concepts used in this paper can be found in the appendix A.

duction space, one could weaken permutation-equivalence into an equivalence relation whose equivalence classes would correspond to the same state of a stable event structure. This observation led Laneve [Lan94] to introduce distributive permutation equivalence in the λ-calculus which only equates reductions resulting one from another by permutation of steps that cannot erase or duplicate one another. The distributive equivalence coincides with permutation-equivalence on needed reductions in non-duplicating orthogonal rewriting systems, but is strictly weaker in the case of even λ_{I}-calculus, where there is no erasure of redexes. Similarly, Corradini et al [CGM95] based their construction on an equivalence relation generated by permutations of disjoint redexes only, in a general categorical model of rewriting.

In this paper we propose a general method to construct finitary computation domains from computation spaces based on new orderings which, unlike Lévy’s permutation embedding and Laneve’s distributive embedding, we believe truly express the growth of information along computations, in the spirit of Scott’s idea of Information Systems [Sco82] which underlies the whole theory of semantics of programming languages. We thereby further extend Boudol’s computational approach to semantics, and develop a ‘relativized’ version of it for calculi where redexes can be duplicated and/or erased. We restrict ourselves to the conflict-free case. Based on [Bou85,Mel96], we hope that our constructions can be generalized to the general case.

To fully understand the problem, let us examine once again Lévy’s hugely successful idea of ‘less work ⊴_{L}’ and of ‘the same work ≈_{L}’. For co-initial finite reductions P, Q in an orthogonal rewrite system (e.g. the λ-calculus), P is less than Q, written P ⊴_{L} Q, if what remains of P after Q, the residual P/Q of P after Q, is empty. And P and Q do the same work, P ≈_{L} Q, if P ⊴_{L} Q and Q ⊴_{L} P. The ‘real life’ counterparts of an ordering relation, such as ‘greater’, ‘older’, ‘stronger’, refers to, or is relative with respect to, a particular aspects of the object/subject one is interested in. But Lévy’s ordering lacks that relativity property: Suppose we are interested in computing the normal forms of a λ-term

t = Kx(IIx), where K = λx.λy.x and I = λx.x. Let P : t→^{I}Kx(Ix) and

Q : t→^{I}Kx(Ix)→^{I}Kxx. Clearly P ⊲_{L} Q. But both P and Q are unneeded, and neither makes progress towards computation of the normal form obtainable from t in one K-step t→^{K}x. In this circumstances, does it really make sense to say that ‘Q is greater (i.e., does more work) than P ’?

To correct this situation, we introduced in [GK02] orderings ⊴_{S} on reductions relative to particular sets S of finite or infinite values one may be interested in, such as normal forms, head-normal forms, weak head-normal forms, Böhmtrees [Bar84], Lévy-Longo-trees [Lév76,Lon83], or Berarducci-trees [Ber96], in the λ-calculus, or root-stable forms in orthogonal TRSs. Such values are expressed via super(stable) sets of reductions in Stable Deterministic Residual Structures (SDRSs) [GK96]. SDRSs are Abstract Reduction Systems [Hin69,Klo92] with an axiomatized residual relations on redexes, enabling one to define permutation equivalence on reductions. SDRSs cover all conflict-free term and (sharing-) graph/net rewrite systems, and many other interesting computational structures, and we abstract from inessential syntactic structure of the objects. In SDRSs one can give abstract proofs of the normalization and minimality theorems [GK96,GK02], relative to (super)stable sets of reductions. Recall from [Win89] that families of configurations in stable event structures whose enabling relation have a similar ‘minimality’ property generate dI-domains. The concept of stability of an event structure can be expressed in terms of our concept of stable reduction (configuration) sets: it is trivial to check that an event structure is stable [Win89] iff for any event e, the set of all configurations containing e is stable (according to our definition of stability).

Here we show that the orderings ⊴_{S}, which we call (temporarily) reduction orderings, form finitary ω-algebraic complete lattices on ≈_{S}-equivalence classes of co-initial reductions (where ≈_{S}= ⊴_{S} ∩ ⊵_{S}). An ordering ⊴_{S} need not be distributive in general, since for example if we take for S the set of all normalizing reductions in the λ_{I}-calculus, then ⊴_{S} coincides with ⊴_{L}, and Laneve [Lan94] has demonstrated that ⊴_{L} is not distributive (even) for the case of λ_{I}-calculus. However, any ⊴_{S} contains a substructure which is a dI-domain. This substructure corresponds to S-needed complete-family reductions [Lév78,Lév80]. (The subspace of complete-family reductions generates a non-duplicating computation space as families do not duplicate one another; as we have already mentioned, non-duplicating reduction systems are equivalent to event structures with erasure, and the glb operation can simply be expressed via ordinary set-theoretic intersection on S-needed events/families [KG98].) Thus the reduction orderings can be seen as a refinement of dI-domains which reflect computations more closely: they directly reflect duplication of redexes which dI-domains cannot, and this is the reason for the loss of the distributivity property.

Furthermore, we show that reduction orderings can be generated by the permutation ordering ⊴_{L} on non-erasing conflict-free reduction systems that are free from (syntactic) accidents (i.e., co-initial reductions that end at the same term are permutation-equivalent). Actually, in such systems, ⊴_{L} coincides with the reduction relation → → (hence the name – reduction ordering), which enables us to give an equivalent domain-theoretic definition of reduction orderings. This result is an analog of the well known representation theorems for concrete domains [KP93], dI-domains [Win89] and Scott-domains [Sco82,LW93], and the key idea is to equip partial orders with a well-behaved residual information.

The following example demonstrates the differences between the domain constructions for duplicating systems discussed above.

Example 11 Consider the λ_{I}-term t = (λx.xx)(Iz), where I = λx.x, used by Laneve [Lan94] to demonstrate that Lévy-equivalence need not generate a dI-domain from the reduction space of a λ-term. ^{4} Figures 1.(1)-(4) display the reduction space of t, and the Hasse diagrams corresponding to the reduction ordering (w.r.t. normal forms), to Laneve’s distributive permutation ordering, to Khasidashvili and Glauert’s [KG98] event ordering, and Boudol and Melliès’ [Bou85,Mel97] external ordering. Clearly, the reduction ordering describes the computation space of t most closely (the corresponding Hasse diagram coincides with the reduction graph of t). The distributive permutation ordering is not even a lattice (despite the fact that the λ-calculus is conflict-free), but the downward closure of any element is a distributive lattice. The external ordering (roughly) corresponds to call-by-name computation and cannot adequately account for either call-by-value computation from t or for all needed ones (note that call-by-value computation from t to normal form is shorter than the two external computations to normal form, hence is computationally interesting). The event ordering cannot adequately account for call-by-need computation; it accounts well for call-by-value and needed complete family computations from t, but this need not be true for all terms since complete family-reductions fail in general to compute minimal normal forms (see [GK96a,GK02] for a counter-example, as

4 Or else take t = 2 × (0 × 1) and consider the rewrite system with rules 2 × x → x + x and x × 1 → x (so for example we don’t have 0 + 0 → 0 and 0 + 0 is a normal form (=result).

well as for a characterization of reductions computing minimal normal forms). None of these orderings can account for unneeded steps, but such steps do not make any progress towards the normal form.

Fig. 1. The orderings

The paper is organized as follows. In the next section, we recall SDRSs and the reduction orderings. Section 3 contains the construction of finitary ωalgebraic complete lattices based on reduction orderings. In Section 4 we give a domain-theoretic definition of reduction orderings. In Section 5 we briefly discuss reduction ordering in SDRSs with an axiomatized family relation [Lév78,Lév80]. Conclusions appear in Section 6.

2 Preliminaries: Residuals, stability, and normalization

Since SDRSs [GK96] have been used in a number of papers, we do not discuss syntactic structures covered by SDRSs and do not give illustrating examples of introduced concepts.^{5} These structures are based on classical work of Lévy [Lév78,Lév80,BL79,HL91], and in recent years there have been many interesting discoveries around the subject of optimality, both of syntactic and semantic nature. The reader unfamiliar with these axiomatic frameworks might think of an SDRS as his or her favorite conflict-free reduction system, such as Combinatory Logic, λ-calculus, Interaction Nets, Interaction Systems, orthogonal Term-Graph (or DAG) Rewrite Systems, etc.

We recall that an Abstract Reduction Systems is a triple A = (T er, 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 redexes u ∈ Red such that → (u) = (t, s), written t→^{u}s. One can identify u with the triple t→^{u}s. A reduction is a sequence t→^{u_{1}}t_{2}→^{u_{2}} . . ..

Notation 21 We write u ∈ t if u is a member of the redexes of t, and write U ⊆ t if U is a subset of the redexes. Reductions are denoted by P, Q, N. We write P : t → → s or t → →^{P} s if P denotes a reduction from t to s. Q : t → → may be finite as well as infinite. P + Q denotes the concatenation of P and Q. u also denotes the reduction that contracts u. Further, for any reduction Q, ⌈Q⌉^{k} will denote the initial part of Q of length k, provided k ≤ |Q| (the length of Q), and ⌈Q⌉_{k} will denote the tail of Q starting from the (k + 1)th step; thus Q = ⌈Q⌉^{k} + ⌈Q⌉_{k}. Finally, we write P ≤ Q if P is an initial part of Q.

In a DRS R, the residual relation is extended to all co-initial finite reductions exactly as in syntactic orthogonal rewrite systems [HL91,Lév78,Lév80,Sta89]:

5 For convenience, we include formal definition in an appendix.

(P_{1} + P_{2})/Q = P_{1}/Q + P_{2}/(Q/P_{1}) and P/(Q_{1} + Q_{2}) = (P/Q_{1})/Q_{2}.^{6} Lévyequivalence or permutation-equivalence is defined as the smallest relation on co-initial reductions satisfying: U + V/U ≈_{L} V + U/V and Q ≈_{L} Q′ ⇒ P + Q + N ≈_{L} P + Q′ + N, where U and V are complete developments of redex sets in the same term. Further, one defines P ⊴_{L} Q iff P/Q = ∅, and can show that P ≈_{L} Q iff P ⊴_{L} Q and Q ⊴_{L} P; and P ⊴_{L} Q iff Q ≈_{L} P + N for some N. The strong Church-Rosser property states that, for any co-initial finite reductions P, Q, P ⊔ Q ≈_{L} Q ⊔ P, where P ⊔ Q = P + Q/P, and is ⊴_{L}-lub of P and Q. Finally, we will need the following Lemma: for any finite co-initial reductions P, Q and N, N/(P ⊔ Q) = N/(Q ⊔ P).

Given a set S of reductions in a DRS R and a term t in R, we call t Snormalizable if S contains a reduction P starting from t; P is then called Snormalizing.

Definition 22 Let S be a set of reductions in a DRS.

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

(2) We call u ∈ t S-unneeded if there is a reduction Q ∈ S staring from t that is external to u, and call it S-needed otherwise.

(3) Let P, Q be co-initial reductions. If P and Q are both finite, then we define P ⊴_{S} Q if P/Q is S-unneeded. Otherwise, P ⊴_{S} Q if for any finite P′ ≤ P there is a finite Q′ ≤ Q such that P′ ⊴_{S} Q′. Further, P ≈_{S} Q iff P ⊴_{S} Q and Q ⊴_{S} P. We call ⊴_{S} and ≈_{S} respectively S-embedding and S-equivalence. ⟨P ⟩_{S} denotes the ≈_{S}-equivalence class of P (we will show below that ≈_{S} is an equivalence relation). We write ⟨P ⟩_{S} ⊴_{S} ⟨Q⟩_{S} if P ⊴_{S} Q.

It is immediate from the definition that ⊴_{L} ⊆ ⊴_{S}.

Definition 23 Let S be a set of reductions in a DRS.

(1) We call S stable iff:

[CS] S is suffix-closed: if P′ ∉ S, then P′ + P′′ ∈ S implies P′′ ∈ S.

[CE] S is closed under S-embedding: P ∈ S and P ⊴_{S} Q implies Q ∈ S.

[CN] S is closed under neededness: every non-empty P ∈ S contracts at least one S-needed redex.

(2) Furthermore, we call S regular iff:

[Reg] In no term can an S-unneeded redex duplicate an S-needed one.

(3) Finally, we call S superstable iff:

[Min] For any S-normalizable term t, S contains a unique, up to ≈_{L}, ⊴_{L}- minimal element starting from t. Such reductions are called S-minimal.

We call a (regular, super) stable set of reductions in a DRS R a (regular, super) stable semantics of R. Below S will denote a stable (regular or superstable) semantics of a DRS.

Definition 24 (1) Let S be a stable semantics of an SDRS R and let P : t → → . The S-needed part of P, [P]_{S}, is a finite or infinite reduction defined by: [P]_{S} = u + [P/u]_{S}, where u ∈ t is the redex whose residual along P is contracted first among S-needed steps in P, if any.

(2) We call a reduction P : t_{0} → t_{1} → … S-needed fair if for any S-needed redex v_{i} ∈ t_{i}, v_{i} ⊴_{S} ⌈P ⌉_{i}.

6 Note that P/Q is defined uniquely only if it is viewed as a multi-step reduction, each multi-step being a complete development of a set of redexes. It is sound however to consider P/Q as a reduction obtained by sequentializations of the corresponding multi-step reduction, and we will freely switch between the two interpretations.

Theorem 25 ([GK02]) Let S be a regular stable semantics of an SDRS R, and let t be S-normalizable. Then any S-needed fair reduction is S-normalizing.

3 Properties of reduction domains

This section contains the construction of ω-algebraic finitary complete lattices from the reduction spaces of SDRSs.

First of all, we show that ⊴_{S} is a partial order, which requires the following simple characterization of ⊴_{S} via ⊴_{L}.

Lemma 31 Let P and Q be finite co-initial reductions in an SDRS R with regular stable semantics S. Then P ⊴_{S} Q iff P ⊴_{L}Q+Q′ for some S-unneeded Q′.

Lemma 32 Let P, Q and N be co-initial reductions in an SDRS R with regular stable semantics S, and let P ⊴_{S} Q ⊴_{S} N. Then P ⊴_{S} N.

Corollary 33 Let S be a regular stable semantics of an SDRS R. Then ≈_{S} is an equivalence relation, and consequently L^{⊴_{S}} (R) = (L^{≈_{S}} (R), ⊴_{S}) is a partial order, where L^{≈_{S}} (R) = L(R)/_{≈_{S}} and L(R) is a set of co-initial reductions in R.

Recall the definition of the ⊴_{L}-meet operation from [GK02]. Let Φ be a set of reductions starting from t, in a DRS. Then the ⊴_{L}-meet of reductions in Φ, written ⊓_{L}Φ, is defined as follows: Let U ⊆ t be the maximal subset such that U ⊴_{L} Φ, and let t → →^{U} s be a complete development of U (or the multi-step contracting U). Then ⊓_{L}Φ = U + ⊓_{L}(Φ/U).

Note that P ⊓_{L}Q need not be a ⊴_{S}-glb of P and Q even in a DRS corresponding to a Recursive Program Scheme: Let R = {g(x) → h(x, E(x)), E(x) → a}, let t = g(g(g(x))), let P : t → h(g(g(x)), E(g(g(x)))) → h(g(h(x, E(x))), E(g(g(x)))), and let Q : t → g(h(g(x), E(g(x)))) → g(h(h(x, E(x)), E(g(x)))). Then t contains three redexes: u, v and w, listed in the top-down order, and none of them are erased in both P and Q, thus P ⊓_{L} Q = ∅, while w ⊴_{S} P, Q for the set S of all normalizing reductions. This suggests the following definition:

Definition 34 Let S be a stable semantics of an SDRS R, and let Φ be a set of reductions in R starting from t. Then:

(1) (S-meet) S-meet of Φ, written ⊓_{S}Φ, is defined as follows: Let U ⊆ t be the maximal subset such that U ⊴_{S} Φ, and let t → →^{U} s. Then ⊓_{S}Φ = U +⊓_{S}(Φ/U).

(2) (S-join) S-join of reductions in Φ, written ⊔_{S}Φ, is defined as follows: Let V ⊆ t be the set of all redexes that are contracted in the first step of one of the reductions in Φ, and let t → →^{V} e. Then ⊔_{S}Φ = V + ⊔_{S}(Φ/V).

(3) (L-join) We define ⊔_{L}Φ = ⊔_{S}Φ.

We need the following two simple lemmas to prove that ⊓_{S} and ⊔_{S} are indeed meet and join operations for ⊴_{S}.

Lemma 35 Let P, Q be finite reductions in an SDRS with regular stable semantics S, let P ⊴_{L} Q, and let Q be S-unneeded. Then so is P.

Lemma 36 Let P ⊴_{S} Q in an SDRS with a regular stable semantics S, and let N be finite and co-initial with P. Then P/N ⊴_{S} Q/N.

Below we use Φ to denote sets of co-initial reductions. Further, for example we write P ⊴_{L} Φ iff ∀Q ∈ Φ. Q ⊴_{L} P; ⌈Φ⌉^{k} will denote the set of initial parts, of the length k, of reductions in Φ; etc.

First note that if Φ consists of two finite reductions P and Q, then P ⊔ Q ≈_{L} P ⊔_{L} Q, although P ⊔ Q and P ⊔_{L} Q are different as multi-step reductions. Further, since every term contains a finite number of redexes, a finite subset of Φ is enough to generate any particular step in ⊔_{L}Φ (even if Φ contains an infinite number of reductions). More precisely:

Lemma 37 Let Φ be a set of reductions in a DRS. Then for any k ≤ |⊔_{L}Φ|, there is a finite subset Φ[k] ⊆ Φ such that ⌈⊔_{L}Φ⌉^{k} = ⊔_{L}⌈Φ[k]⌉^{k} ≈_{L} ⊔⌈Φ[k]⌉^{k}.

Lemma 38 Let Φ be a set of co-initial reductions in a DRS. Then ⊔_{L}Φ is a (unique up to ≈_{L}) ⊴_{L}-lub of Φ. Proof It is immediate from the definition of ⊔_{L} that Φ ⊴_{L} ⊔_{L}Φ. Now let Φ ⊴_{L} P and let us show ⊔_{L}Φ ⊴_{L} P, i.e., that ⌈⊔_{L}Φ⌉^{k} ⊴_{L} ⌈P ⌉^{l_{k}} for any k and some l_{k}. By Lemma 37, ⌈⊔_{L}Φ⌉^{k} = ⊔_{L}⌈Φ[k]⌉^{k} ≈_{L} ⊔⌈Φ[k]⌉^{k}. Let l_{k} be such that ⌈Φ[k]⌉^{k} ⊴_{L} ⌈P ⌉^{l_{k}}. Then (⊔_{L}⌈Φ[k]⌉^{k})/⌈P ⌉^{l_{k}} ≈_{L} (⊔⌈Φ[k]⌉^{k})/⌈P ⌉^{l_{k}} ≈_{L} ⊔(⌈Φ[k]⌉^{k}/⌈P ⌉^{l_{k}}) = ∅, and we are done.

Theorem 39 Let S be a regular stable semantics of an SDRS R, and let Φ be a set of co-initial reductions in R. Then:

(1) ⊓_{S}Φ is a (unique up to ≈_{S}) ⊴_{S}-glb of Φ.

(2) ⊔_{S}Φ is a (unique up to ≈_{S}) ⊴_{S}-lub of Φ.

Proof (1) Let ⊓_{S}Φ = Q : t_{0} → →^{U_{0}} t_{1} → →^{U_{1}} t_{2} → → . . .. It is immediate from Definition 34 that Q ⊴_{S} Φ. Thus we need to show that for any P, P ⊴_{S} Φ ⇒ P ⊴_{S} Q, that is, for any n ≤ |P |, ⌈P ⌉^{n} ⊴_{S} Q. We show this by induction on n. The case n = 0 (i.e., P = ∅) is clear. So let n = k + 1, and let ⌈P ⌉^{k} ⊴_{S} Q. Then ⌈P ⌉^{k} ⊴_{S} ⌈Q⌉^{l_{k}} for some l_{k}. We can assume that ⌈Q⌉^{l_{k}} ends at t_{m} for some m. Now assume that the (k + 1)th step v of P has an S-needed residual v′ under ⌈Q⌉^{l_{k}}/⌈P ⌉^{k} (otherwise, there is nothing to prove). Since ⌈P ⌉^{k}/⌈Q⌉^{l_{k}} is S-unneeded, by Lemma 82.(2) there must be an S-needed redex v′′ in the final term t_{m} of ⌈Q⌉^{l_{k}} such that v′ is its (⌈P ⌉^{k}/⌈Q⌉^{l_{k}})-residual. Furthermore, v′ is the only (⌈P ⌉^{k}/⌈Q⌉^{l_{k}})-residual of v′′ by regularity of S, thus v′′ ⊴_{S} P/⌈Q⌉^{l_{k}}. But P ⊴_{S} Φ, hence P/⌈Q⌉^{l_{k}} ⊴_{S} Φ/⌈Q⌉^{l_{k}} by Lemma 36. Thus, v′′ ⊴_{S} Φ/⌈Q⌉^{l_{k}}, and v′′ must be contracted in U_{m} (by Definition 34). Hence v′/(U_{m}/(⌈P ⌉^{k}/⌈Q⌉^{l_{k}})) = ∅, and we are done.

[figure: t_{0}; ⌈P ⌉^{k}; ·; v]

[figure: t_{m}; ⌈Q⌉^{l_{k}}; ⌈P ⌉^{k}/⌈Q⌉^{l_{k}}; ·; v′]

[figure: v′′ ∈ U_{m}]

(2) By Lemma 38.(2), Φ⊴_{L}⊔_{S}Φ, implying Φ⊴_{S}⊔_{S}Φ. Now let Φ⊴_{S}P and let us show ⊔_{S}Φ⊴_{S} P, i.e., that ⌈⊔_{S}Φ⌉^{k} ⊴_{S} ⌈P ⌉^{l_{k}} for any k and some l_{k}. By Lemma 37, ⌈⊔_{S}Φ⌉^{k} = ⊔_{S}⌈Φ[k]⌉^{k} ≈_{L} ⊔⌈Φ[k]⌉^{k}, and Φ ⊴_{S} P implies ⌈Φ[k]⌉^{k} ⊴_{S} P. Let l_{k} be such that ⌈Φ[k]⌉^{k} ⊴_{S} ⌈P ⌉^{l_{k}}. Then (⊔_{S}⌈Φ[k]⌉^{k})/⌈P ⌉^{l_{k}} ≈_{L} (⊔⌈Φ[k]⌉^{k})/⌈P ⌉^{l_{k}} ≈_{L} ⊔(⌈Φ[k]⌉^{k}/⌈P ⌉^{l_{k}}), and ⊔(⌈Φ[k]⌉^{k}/⌈P ⌉^{l_{k}}) is S-unneeded by Lemma 82.(1). Thus (⊔_{S}⌈Φ[k]⌉^{k})/⌈P ⌉^{l_{k}} is S-unneeded by Lemma 35, i.e., ⊔_{S}⌈Φ⌉^{k} ⊴_{S} ⌈P ⌉^{l_{k}}, implying ⊔_{S}Φ ⊴_{S} P.

Corollary 310 Let S be a regular stable semantics of an SDRS R. Then L^{⊴_{S}} (R) is a complete lattice with meet and join operations ⊔_{S} and ⊓_{S} defined by: ⊔_{S}⟨Φ⟩_{S} = ⟨⊔_{S}Φ⟩_{S} and ⊓_{S}⟨Φ⟩_{S} = ⟨⊓_{S}Φ⟩_{S}.

Now we can soundly define the relativized stable computational semantics for an SDRS R as follows: Let S be a regular stable semantics of R, and let t be an S-normalizable term in R. Then the value of t in R w.r.t. S is the ⊴_{S}-maximal ≈_{S}-equivalence class of reductions starting from t, in L^{⊴_{S}} (R). Thus for example in the case of Böhm-semantics, the Böhm-tree BT (t) of t is represented by the set of all reductions computing BT (t), which form the ⊴_{S_{B}}-maximal ≈_{S_{B}}-class of reductions starting from t (where S_{B} is the set of all reductions computing Böhm-trees, see [GK02] for details).

Lemma 311 Let S be a regular stable semantics of an SDRS R, let U ∈ t be a set of S-needed redexes in t, let N : t → → be S-needed, and let N ⊴_{S} U. Then N is a development of U, thus is finite.

This lemma is used in the proof of the following crucial lemma for establishing finiteness of L^{⊴_{S}} (R).

Lemma 312 Let S be a regular stable semantics of an SDRS R, let P ⊴_{S} Q, and let [Q]_{S} be finite. Then so is [P]_{S}.

Hence, by Lemma 82.(4), we can soundly define ⟨P ⟩_{S} to be finite iff P contracts only a finite number of S-needed redexes, or equivalently if [P]_{S} is finite. The following lemma justifies our definition:

Lemma 313 Let S be regular stable semantics for an SDRS R. Then ⟨P ⟩_{S} is finite iff it is a finite element of L^{⊴_{S}} (R).

Now, using Lemmas 313 and 82.(4) and Theorem 39, we can prove finiteness and algebraicity of L^{⊴_{S}} (R):

Theorem 314 Let S be a regular stable semantics for an SDRS R. Then L^{⊴_{S}} (R) is a finitary ω-algebraic complete lattice. Proof (Algebraicity) Let Q be a reduction in R and let Φ = {N|⟨N⟩_{S} finite, N ⊴_{S} Q}. Then ⟨Φ⟩_{S} consists of all finite elements of L^{⊴_{S}} (R) dominated by ⟨Q⟩_{S}. It follows from Lemma 31 and Lemma 82.(1) that for any finite subset Φ′ ⊆ Φ, ⊔_{S}Φ′ ∈ Φ (since we can assume that all reductions in Φ are finite), thus ⟨Φ⟩_{S} is directed. Thus we want to prove that ⟨⊔_{S}Φ⟩_{S} = ⟨Q⟩_{S}. It is immediate from Definition 34 that Q = ⊔_{S}{⌈Q⌉^{n}|n ≤ |Q|}. But {⌈Q⌉^{n}|n ≤ |Q|} ⊆ Φ, thus Q = ⊔_{S}⌈Q⌉^{n}⊴_{S} ⊔_{S}Φ. On the other hand, ⊔_{S}Φ is the ⊴_{S}-lub of Φ by Theorem 39, thus ⊔_{S}Φ ⊴_{S} Q. Hence ⟨⊔_{S}Φ⟩_{S} = ⟨Q⟩_{S}.

(Finiteness) Let ⟨P ⟩_{S} be finite in L^{⊴_{S}} (R). By Lemmas 313 and 82.(4), we can assume P to be S-needed and finite. Suppose on the contrary that ⟨P ⟩_{S} dominates an infinite number of elements of L^{⊴_{S}} (R). Then by Lemma 82.(4) there is an infinite set Φ of S-needed reductions such that Φ ⊴_{S} P. Since the reduction tree corresponding to Φ is finitely-branching (because a term may contain only a finite number of redexes), Φ must contain an infinite S-needed reduction Q ⊴_{S} P (by König’s Lemma), contradicting Lemma 312.

The above theorem fails for (irregular) stable semantics S in general: Consider the DRS R generated by R = {f(x) → h(f(x), f(x)), a → b}, restricted to the reduction graph G(t) of t = f(a), and take for S_{ter} the set of terms not containing occurrences of a. Then the corresponding set S of S_{ter}-normalizing reductions is stable but not regular, and the set of ≈_{S}-classes of reductions in G(t) does not contain a finite element except the bottom element, implying that R is not algebraic. (Indeed, if a reduction P contracts infinitely many S-needed redexes, then, for any finite m, ⊔_{k≤m}⌈P ⌉^{k} ⊲_{S} ⊔_{k<∞}⌈P ⌉^{k} ≈_{S} P, thus ⟨P ⟩_{S} is not finite; And if P contracts a finite number of S-needed redexes, we can assume that the last step of P is S-needed, thus has the form C[f(a)]→^{u}C[f(b)]. But the step u is the ⊴_{S}-lub of the set of (strictly ⊲_{S}-smaller) finite initial parts of the reduction C[f(a)] → C[h(f(a), f(a))] → C[h(f(b), f(a))] → C[h(f(b), h(f(a), f(a)))] → C[h(f(b), h(f(b), f(a))] → . . .. Hence u, and thus P itself, are not finite.) ^{7}

4 A representation theorem for the reduction orderings

In previous sections, we defined reduction orderings ⊴_{S} as orderings generated by pairs (R, S), where S is a regular stable semantics for an SDRS R. Now we wish to give an equivalent definition in domain-theoretic terms. Such results in the literature are called representation theorems: for example, concrete domains (defined by restricting partial orders with a number of axioms) are exactly the domains generated by Information Matrices [KP93] (often called Concrete Data Structures [Cur86]), dI-domains are domains generated by Prime (or equivalently, Stable) Event Structures [Win89], and Scott domains are domains generated by Information Systems [Sco82,LW93].

To define (i.e., to fully characterize) orderings ⊴_{S} domain-theoretically, we note that ⊴_{S} is built from a pair (R, S), and in the transition from (R, S) to ⊴_{S} some information, namely the residual information, gets ignored. This suggests that, up to some isomorphism, (R, S) is nothing but ⊴_{S} equipped with an appropriate residual information. The idea of partial orders with residuals is not precisely new: all the above mentioned representation results implicitly use a linear residual concept. In the case of reduction orderings, the crucial step enabling us to define the correct residual relation is the observation that all reduction orderings can actually be generated as permutation orderings ⊴_{L} on some non-erasing SDRSs R_{S} that are (syntactic) accident-free (to be defined shortly).

The next definition shows how to define such ‘projections’ of ⊴_{S} onto ⊴_{L}. There, it is enough (and convenient) to consider only comma-SDRSs R, whose underlying ARSs are reduction graphs of a fixed initial term. The S-projection of any SDRS consists of (isomorphic copies) of projections of its comma-(sub)SDRSs.

Definition 41 (S-projection) Let R be a comma-SDRS with a regular stable semantics S. Then the S-projection of R is an SDRS R_{S} defined as follows:

• Terms in R_{S} are ≈_{S}-classes ⟨P ⟩_{S} of finite initial reductions P in R (that is, P starts with the initial term);

• Arrows in R_{S} are pairs ⟨P ⟩_{S} →_{S} ⟨P + u⟩_{S}, where u is an S-needed redex in the final term of P. (The empty redex in ⟨P ⟩_{S} can be defined as the pair

⟨P ⟩_{S} →^{∅}_{S}⟨P ⟩_{S}.)

• The residual relation /_{S} in R_{S} is defined as follows: Let ⟨P ⟩_{S} →^{u^{∗}}_{S}⟨P + u⟩_{S}

and ⟨P ⟩_{S} →^{v^{∗}}_{S}⟨P + v⟩_{S} in R_{S}. Then for any S-needed v′ ∈ v/u, ⟨P + u⟩_{S} →^{v^{′∗}}_{S}⟨P + u + v′⟩_{S}

is a u^{∗}-residual of v, written v^{′∗} ∈ v^{∗}/_{S}u^{∗}.

7 The same DRS was used in [GKK00] to demonstrate failure of the hypernormalization theorem w.r.t. irregular stable sets of results in general.

Thus any redex P u in R (whose history P is an initial reduction) is assigned a unique redex ⟨P ⟩_{S} →_{S} ⟨P + u⟩_{S} in R_{S}, although different redexes (with histories) in R may have the same corresponding redex in R_{S}. This assignment induces a function h from (parts of) initial reductions in R to initial reductions in R_{S} with the following properties:

• If P = P_{1}+P_{2} is an initial reduction in R, then h(P_{1}+P_{2}) = h(P_{1})+h(P_{2});

• If N is an initial reduction in R, then h(N) = ∅ iff N is S-unneeded.

Although the converse of h is not a function, for any initial reduction P′ in R_{S} there is a unique S-needed initial reduction in R, noted h′(P′), that contracts the ‘same’ redexes as P′, i.e., h(h′(P′)) = P′, and therefore h′(h(P)) = P for any S-needed initial reduction P in R. Thus (h, h′) gives an isomorphism between S-needed initial reductions in R and initial reductions in R_{S}. Using these properties of h, we can quite easily prove the correctness of Definition 41. First a definition:

Definition 42 Let R be a comma-SDRS. We call R good if it is non-erasing and accident-free:

• [NE]: for any co-initial distinct redexes t→^{u}s and t→^{v}e in R, v/u ≠ ∅.

• [AF]: for any initial reductions P and Q in R that end at the same term t, P ≈_{L} Q.^{8} Note that P ⊔ Q ends at t, too.

Lemma 43 Let R be a comma-SDRS with a regular stable semantics S. Then R_{S} is a good SDRS. (Hence in particular Definition 41 is sound.)

For a comma-SDRS R, assume that L^{⊴_{L}} (R) and L^{⊴_{S}} (R) denote the corresponding orderings w.r.t. the initial term. Now we can easily prove the desired result:

Theorem 44 Let S be a regular stable semantics of a comma-SDRS R. Then L^{⊴_{L}} (R_{S}) and L^{⊴_{S}} (R) are isomorphic. Proof Since initial reductions in R_{S} are exactly reductions h(P) for initial (Sneeded) reductions P in R, the lemma follows immediately from the fact that P ⊴_{S} Q in R iff h(P) ⊴_{L} h(Q) in R_{S} (for the latter, see the proof of Lemma 43).

In fact, in non-erasing SDRSs, ⊴_{L} coincides with the fair ordering ⊴_{fair}, i.e., the ordering ⊴_{fair} where S_{fair} is the set of all fair ([Klo92]) reductions; this follows immediately from the fact that at least one residual of any redex u ∈ t in a non-erasing SDRS must be contracted in every fair reduction starting from t (and from the fact that a reduction is fair iff so is any of its tails).

Furthermore, because of accident-freeness, in good SDRSs (differently from SDRSs in general) there is at most one step between any pair of terms (t, s), thus the reduction relation can be given as sets of pairs. That is, a good SDRS is a triple R = (T er, →, /), where T er is a set of objects (called terms) containing an initial term t_{∅}, → is a set of pairs, and / is a residual relation (satisfying SDRSaxioms). Furthermore, in good SDRSs R, ⊴_{L} on finite elements is isomorphic to → → , the reduction relation on R:

Theorem 45 Let R = (T er, →, /) be a good SDRS. Then L_{fin}^{⊴_{L}}(R) = (L_{fin}^{≈_{L}}(R), ⊴_{L}) is isomorphic to (T er, → → ), where L_{fin}(R) is the set of all finite initial reductions in R, and L^{⊴_{L}} (R) = (L^{≈_{L}}(R), ⊴_{L}) is isomorphic to ≤_{R}= IC(T er, → → ),

8 A simple pair of co-initial reductions, namely P : IIx→^{Ix}Ix and Q : IIx →^{IIx}Ix, that end at the same term but are not Lévy-equivalent was given by Lévy [Lév78], where this phenomenon is called a syntactic accident.

the ideal completion of (T er, → → ) (infinite ideals of ≤_{R} correspond to ≈_{L}- classes of infinite reductions in R). Proof By [AF], every term t ∈ T er uniquely determines exactly one element ⟨P_{t}⟩_{L} of L_{fin}^{≈_{L}}(R), where P_{t} is any initial reduction ending with t. Furthermore, t → → s iff ⟨P_{t}⟩_{L} ⊴_{L} ⟨P_{s}⟩_{L}: Indeed, if N : t → → s, then by [AF] P_{s} ≈_{L} P_{t} + N, implying P_{t} ⊴_{L} P_{s}; and conversely, P_{t} ⊴_{L} P_{s} implies P_{s} ≈_{L} P_{t} +P_{s}/P_{t} and clearly P_{s}/P_{t} : t → → s. By Lemma 313, L_{fin}^{≈_{L}}(R) coincides with the set of finite elements of L^{⊴_{L}} (R), hence L^{⊴_{L}} (R) is isomorphic to ≤_{R} (see e.g. [DP90], pages 82-83).

Thus, we need to provide a domain-theoretic characterization of (ideal completions of) orderings (T er, → → ) for good SDRSs R = (T er, →, /), which are finitary w-algebraic complete lattices of a special form. It is standard (after [KP93]) to associate with a partial order ≤ = (D, ≤_{D}) an ARS (or a transition system) A_{≤} = (T er_{≤}, →_{≤}) such that T er_{≤} = D and t →_{≤} s iff t −< _{D}s (in D), where t −< _{D}s iff t <_{D} s ∧ ∀o ∈ D : (t ≤_{D} o ≤_{D} s ⇒ t = o ∨ s = o)}. The relation −< _{D} is called covering. A sequence of the form t −< _{D}t_{1} −< _{D} … is called a covering chain, or a covering (t, s)-chain when t_{i} ≤_{D} s. We call a covering (t, s)-chain maximal if it is infinite or cannot be extended.

Since any algebraic cpo L is obtained as the ideal completion of its subset of finite elements (noted F (L)), it is enough to axiomatize properties of finite elements only. Therefore, following [Cur86], if in a pair t −< _{D}s in an algebraic cpo both t and s are finite, we write it as [t, s]_{D} (or simply as [t, s]) and call it a prime interval, although the definition of (prime) intervals [t, s] say in [KP93,Win80] does not require t and s to be finite. Similarly, if all t_{i} in a covering chain t −< _{D}t_{1} −< _{D} … are finite, we write it also as [t −< _{D}t_{1} −< _{D} …].

Note that in non-erasing SDRSs, the residual relation is defined uniquely by the corresponding lub operation: If t→^{u}s and v ∈ t, exactly the redexes v′ ∈ s such that u+v′⊴_{L}u⊔v are u-residuals of v. This is of course not true in erasing SDRSs. This observation allows us to define a residual relation in complete lattices as follows:

Definition 46 Let ≤ = (D, ≤_{D}, ⊔_{D}, ⊓_{D}), be a complete lattice.

(1) We define the residual relation /_{D} as the reflexive and transitive closure of the following relation:

• For any pair of co-initial prime intervals u = [t, o], v = [t, s] in D, u/_{D}v = {[s, e] | e ≤ s ⊔ o}.

(2) We write t −< _{D}s −<^{c} _{D}s^{∗} if, for any o ∈ D such that t −< _{D}o, s^{∗} ≰_{D} s ⊔_{D} o, and say that t −< _{D}s creates s −<^{c} _{D}s^{∗}. We write [t −< _{D}s −<^{c} _{D}s^{∗}] to indicate that t, s and s^{∗} are finite.

We now reformulate the axioms of good SDRSs in domain-theoretic terms.

Definition 47 Let ≤ = (D, ≤_{D}, ⊔_{D}, ⊓_{D}) be a (finitary ω-algebraic) complete lattice such that:

• [FB] (finite branching) For any t ∈ F (D), there are only a finite number of s ∈ D such that t −< _{D}s (such an s must be finite).

• [NT] (no triangles) For any pair of different co-initial prime intervals [t, s] and [t, o] in D, s, o <_{D} s ⊔ o.

• [SD] (semi-distributivity) For any triple of co-initial prime intervals [t, s], [t, e], and [t, o] in D, s ⊔_{D} (o ⊓_{D} e) = (s ⊔_{D} o) ⊓_{D} (s ⊔_{D} e). (Note here that, by [NT], s ⊔_{D} (o ⊓_{D} e) = s.)

• [FC] (finite chains) For any set of co-initial prime intervals [t, s_{i}], any maximal covering (t, ⊔_{D}s_{i})-chain is finite and ends with ⊔_{D}s_{i}.

• [S] (stability) For any t, s, s^{∗}, e, e^{∗} ∈ F (D) such that [t −< _{D}s −<^{c} _{D}s^{∗}]

and [t −< _{D}e −<^{c} _{D}e^{∗}], (s ⊔_{D} e^{∗}) ⊓_{D} (e ⊔_{D} s^{∗}) = e ⊔_{D} s.

Then we call ≤ a complete regular domain (CRD).

By Definition 46, we may as well refer to a CRD as a triple ≤ = (D, ≤_{D}, /_{D}). Using this definition, we can show that good SDRSs and CRDs are equivalent models. We need two simple lemmas first:

Lemma 48 Let (D, ≤, ⊔, ⊓) be a CRD, and let [t, s], [t, s_{i}] (0 ≤ i ≤ m) be prime intervals such that s ≠ s_{i}. Then s < s ⊔ (⊔s_{i}) and ⊔s_{i} < s ⊔ (⊔s_{i}).

Lemma 49 Let ≤ = (D, ≤_{D}, ⊔_{D}, ⊓_{D}) be a CRD, let [e_{0} −< _{D}e_{1} −< _{D} … −< _{D}e_{m}], and let [e_{0} −< e_{0}^{∗}]. Then [e_{m}, e_{m}^{∗}] is a residual, w.r.t. /_{D}, of [e_{0}, e_{0}^{∗}] iff e_{m}^{∗} ≤_{D} e_{0}^{∗} ⊔_{D} e_{m}, and the lub of all such e_{m}^{∗} is e_{0}^{∗} ⊔_{D} e_{m}.

The above lemma says that the residual relation is independent of a covering sequence between e_{0} and e_{m}.

Theorem 410 Good SDRSs and complete regular domains are equivalent models. More precisely:

(1) For any good SDRS R = (T er, →, /), ≤= IC(T er, → → ) is a CRD (where → → is the transitive reflexive closure of →).

(2) If ≤= (D, ≤_{D}, /_{D}) is a CRD, then R_{≤} = (F (D), −< _{D}, /_{D}) is a good SDRS and ≤ is isomorphic to IC(F (D), −< _{D}) (where −< _{D}, /_{D} in R_{≤} are restrictions, to F (D), of these relations in ≤). Proof

(1) By Theorems 314, 44 and 45, ≤= IC(T er, → → ) is a finitary w-algebraic complete lattice (we denote by ⊔_{≤} and ⊓_{≤} the corresponding lub and glb operations). Then [FB] is immediate. [NT] is immediate from [NE]. To show [SD] (in its simplified form), let [t, s], [t, e], and [t, o] be prime intervals in ≤. Then s → → s ⊔_{≤} e and s → → s ⊔_{≤} o, hence s → → (s ⊔_{≤} e) ⊓_{≤} (s ⊔_{≤} o) = s^{∗}. If on the contrary s → →^{+} s^{∗}, then for any s′ such that s → s′ → → s^{∗}, we would have that the redex [s, s′] is a [t, s]-residual of both redexes [t, o] and [t, e] in R – contradiction. To prove [FC], let [t_{0}, s_{i}] be prime intervals in ≤, and let P : t_{0} → t_{1} → … be a (t_{0}, ⊔_{≤}s_{i})-chain. Then P is a development of the set of redexes [t_{0}, s_{i}] in R by Lemma 49 (since the residual relation generated by (T er, → → ) coincides with /), and [FC] follows from [FD] for R. Finally, [S] follows immediately from

[NT] and stability of R.

(2) We need to prove that the residual relation in R_{≤} satisfies the axioms of good SDRSs. The fact that every term contains a finite number of redexes is immediate from [FB], and the fact that every redex is a residual of at most one redex follows from [SD]. The axiom [AF] follows from the fact in a complete lattice, the lub of two elements a and b does not depend on covering chains leading from the bottom element to a and b. By Lemma 49, [FD] implies [FC], and stability of R_{≤} follows from [S].

5 Imposing more structure on ⊴_{S}

In [GK96], Deterministic Family Structures were introduced on the top of DRSs, by imposing further axioms on the residual relation, enabling us to infer important properties of redex-families, such as the optimality theorem [Lév78,Lév80].

Formally, a DFS is a pair F_{S} = (R, ≃), where R is a DRS and ≃ is a family relation on redexes with histories P v (v is a redex in the final term of P), satisfying a number of axioms not listed here (see Appendix B).

The projection of pairs (R, S) onto SDRSs R_{S} induces a projection of pairs (F, S) onto F_{S} = (R_{S}, ≃_{S}), where v′ ≃_{S} w′ iff P v ≃ Qw, and v′ = (⟨P ⟩_{S}, ⟨P + v⟩_{S}) and w′ = (⟨Q⟩_{S}, ⟨Q + w⟩_{S}). Note here that, because of accident-freeness, in R_{S} redexes determine their histories uniquely up to ≈_{L}, thus ≃_{S} can simply be seen as a relation on redexes rather than redexes with histories; and although there may be other P^{∗}v^{∗}, Q^{∗}w^{∗} such that v′ = (⟨P^{∗}⟩_{S}, ⟨P^{∗} + v^{∗}⟩_{S}) and w′ = (⟨Q^{∗}⟩_{S}, ⟨Q^{∗} + w^{∗}⟩_{S}), one has P v ≃ P^{∗}v^{∗} and Qw ≃ Q^{∗}w^{∗} (since P v and P^{∗}v^{∗} must be the residuals of the same redex in the final term of [P]_{S}, by Lemma 82, and similarly for Qw and Q^{∗}w^{∗}), thus the definition of ≃_{S} is correct. It is easy to show that:

Theorem 51 For any DFS F with a regular stable semantics S, F_{S} is a DFS.

Thus orderings ⊴_{S} generated by pairs (F, S) are generated by good DFSs, i.e., DFSs F = (R, ≃) such that R is good. And furthermore the family relation ≃ induces an equivalence relation on prime intervals in ≤_{R} that is a family relation (when considering ≤_{R} as an SDRS). There may be more than one way to define a family relation on a (good) SDRS,^{9} so in general the family axioms do add strength to complete regular domains. Furthermore, we can impose the minimality property (the counterpart of superstability of reduction sets) on regular stable domains to obtain an even better behaved ordering.

6 Conclusions and future work

We have defined stable computational semantics for deterministic reduction systems based on very natural orderings ⊴_{S} reflecting the growth of information towards the value of an expression w.r.t. a semantics S specified by a set of computations. We showed that ⊴_{S} are finitary ω-algebraic complete lattices of a special form (containing dI-domains as substructures), and gave their equivalent domain-theoretic characterization. The proposed semantics unifies Boudol’s computational approach to semantics [Bou85] with Winskel’s stable Event Structure Semantics [Win89] (in the conflict-free case).We have learned that the ‘finest’ good domains to model functional calculi are actually the domains generated by the calculi themselves.

The importance of the concepts of stability and dI-domains for construction of models of functional calculi (based on the λ-calculus) and for the full abstraction problem [BCL85,Ong95], as well as for modeling polymorphism [Gir86,CGW89], is well understood, and we hope that our results will contribute to progress in these areas. The interpretation of DFSs into non-duplicating ones proposed in [KG97a,KG97] maps good DFSs into linear DFSs which generate dI-domains, and we can readily get denotational models for lambda-calculi with different stable semantics using Berry’s construction [Ber79]. However, more direct ways of using the orderings ⊴_{S} in the study of denotational models of λ- and related calculi deserve further investigation. The precise relevance of family axioms and the minimality for regular stable domains is presently unknown.

9 This is related to the separability problem: a redex may create a number of redexes that may be put in different families, as well as in the same family, without violating the family axioms [KG97].

References

[AGM] Abramsky S., Gabbay D., and Maibaum T., eds. Handbook of Logic in Computer Science, vol. 1-4, Oxford University Press, 1992-1995.

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

[Ber96] Berarducci A. Infinite lambda-calculus and non-sensible models. Logic and Algebra, Lecture Notes in Pure and Applied Mathematics 180, Marcel Dekker Inc., 1996, p. 339-378.

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

[BL79] Berry G., Lévy J.-J. Minimal and optimal computations of recursive programs. JACM 26, 1979, p. 148-175.

[BCL85] Berry G., Curien P.-L., Lévy J.-J. Full abstraction for sequential languages: the state of the art. In [NR85], p. 89-132.

[Bou85] Boudol G. Computational semantics of term rewriting systems. In [NR85], p. 169-236.

[CGW89] Coquand T., Gunter C.A., Winskel G. dI-domains as a model of polymorphism. In Proc. of MFPLS’87, Springer LNCS, vol. 298, 1987, p. 344-363.

[CGM95] Corradini A., Gadduchi F., Montanari U. Relating two categorical models of term rewriting. In: Proc. of RTA’95, springer LNCS, Vol. 914, 1995, p. 25-240.

[Cur86] Curien P.-L. Categorical combinators, Sequential algorithms and functional programming. John Wiley & Sons, 1986.

[DP90] Davey, B.A., Priestley H.A., Introduction to Lattices and Order Cambridge University Press, 1990.

[DJ90] Dershowitz N., Jouannaud J.-P. Rewrite Systems. In: J. van Leeuwen ed. Handbook of Theoretical Computer Science, Chapter 6, vol. B, 1990, p. 243-320.

[Gir86] Girard J.Y. The system F of variable types:fifteen years later. TCS 45:159-192, 1986.

[Gir87] Girard J.Y. Linear logic. TCS 50:1-101, 1987.

[GKK00] J. R. W. Glauert, J. R. Kennaway and Z. Khasidashvili. Stable results and relative normalization. Journal of Logic and Computation, vol. 10(3). Special Issue on Type Theory and Term Rewriting, F. Kamareddine and J.W. Klop, eds. Oxford University Press, 2000, p. 1-26.

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

[GK96a] Glauert J.R.W., Khasidashvili Z. Minimal relative normalization in orthogonal expression reduction systems. In: Proc. of FST&TCS’96, Springer LNCS, vol. 1180, 1996, p. 238-249.

[GK02] J. R. W. Glauert, Z. Khasidashvili. “An abstract Böhm-normalization”. in: Proc. of Second International Workshop on Reduction Strategies in Rewriting and Programming, WRS’02, Electronic Notes in Computer Science, Elsevier Science B.V., 2002.

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

[Gun93] Gunter C.A. Semantics of programming languages: structures and techniques. MIT Press, 1993.

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

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

[KP93] Kahn G., Plotkin G.D. Concrete domains. In: To Corrado Böhm, TCS 121:186-277, 1993.

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

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

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

[KG98] Khasidashvili Z., Glauert J.R.W. Relating conflict-free stable transition and event models. Available on request. (Conference version appears in Proc. of MFCS’97, Springer LNCS, vol. 1295, 1997, p. 269-278.)

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

[Klo92] Klop J. W. Term Rewriting Systems. In: [AGM], vol. 2, 1992, p. 1-116.

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

[LW93] Larsen K., Winskel G. Using information systems to solve recursive domain equations effectively. In: Proc. of Int. Symposium on the Semantics of Data Types, Springer LNCS, vol. 173, 1984.

[Lév76] Lévy J.-J. An algebraic interpretation of the λβK-calculus; and an application

of a labelled λ-calculus. TCS 2(1):97-114, 1976. [Lév78] Lévy J.-J. Réductions correctes et optimales dans le lambda-calcul, Thèse de

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

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

[Lon83] Longo G. Set theoretic models of lambda calculus: theories, expansions and isomorphisms. Annals of Pure and Applied Logic, 24:153-188, 1983.

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

[Mel97] Melliès P.-A. A factorization theorem in rewriting theory. In; Proc. of CTCS’97, Springer LNCS vol. 1290.

[Mel98] Melliès P.-A. A stability theorem in rewriting theory. In: Proc. of LICS’98, 1998.

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

[NR85] Nivat M., Reynolds J.C., eds. Algebraic methods in semantics. Cambridge Univ. Press, 1985.

[Ong95] Ong C.-H. Correspondence between operational and denotational semantics: the full abstraction problem for PCF. In: [AGM], vol. 4, 1995, p. 269-356.

[Plo83] Plotkin G. Domains. University of Edinburgh, 1983 (Manuscript).

[Sco82] Scott D. Domains for denotational semantics. In Proc. ICALP’82, Springer LNCS, vol. 140, pp. 577-613, 1982.

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

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

[Win89] Winskel G. An introduction to Event Structures. Springer LNCS, vol. 354, 1989, p. 364-397. Extended version appears as Cambr. Univ. Comp. Lab. Report n. 95, 1986.

7 Appendix A: Partial orders

Definition 71 • A partial order is a binary relation ⊑ on a set L which is reflexive: ∀x ∈ L : x ⊑ x; transitive: ∀x, y, z ∈ L : x ⊑ y ∧ y ⊑ z ⇒ x ⊑ z; and antisymmetric: ∀x, y ∈ L : x ⊑ y ∧ y ⊑ x ⇒ x = y.

• A complete lattice is a partial order L = (L, ⊑) which has least upper bounds (or joins) ⊔X and greatest lower bounds (or meets) ⊓X of arbitrary subsets X ⊆ L. (Actually, it is enough to require only existence of meets ⊓X, or equivalently, existence of a top element ⊤ and of meets ⊓X for all non-empty X.) We write x ⊔ y and x ⊓ y for the join and meet respectively of two elements x, y ∈ L.

• A subset X ⊆ L of a partial order L = (L, ⊑) is bounded or consistent if X has an upper bound in L. Further, X ⊆ L is pairwise bounded or compatible if each pair of elements in X is bounded. L is coherent if any pairwise bounded subset X ⊆ L has least upper bound, and is bounded complete or consistently complete if any bounded subset X ⊆ L has least upper bound.

• A directed subset of a partial order L is a subset Y ⊆ L with the property that for any finite set X ⊆ Y there is an element y ∈ Y such that ∀x ∈ X.x ⊑ y.

• A complete partial order (cpo) is a partial order L = (L, ⊑) that has a least element ⊥ and all least upper bounds of directed subsets of L.

• A finite element (also called isolated or compact) of a cpo is an element z with the property that, for all directed subsets Y, if z ⊑ ⊔Y, then there is some y ∈ Y for which z ⊑ y.

• A cpo L is algebraic if for any element d ∈ L the set {x ⊑ d | x is finite} is directed and has least upper bound d. If moreover L has only a denumerable number of finite elements, then L is called ω-algebraic.

• A computation domain is a coherent and ω-algebraic partial order. A Scott domain is a consistently complete ω-algebraic cpo.

• A complete prime of a complete lattice L is an element p ∈ L such that p ⊑ ∪X ⇒ ∃x ∈ X.p ⊑ x for any subset X ⊆ L. L is prime algebraic if, for all x ∈ L, x = ⊔{p ⊑ x | p is a complete prime}.

• An algebraic cpo is finitary iff every finite element dominates only a finite number of elements, i.e., {x | x ⊑ d} is finite for every finite element d.

• A complete lattice L is distributive if x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z), for all elements x, y, z ∈ L.

8 Appendix B: Properties of Residuals

Definition 81 A Deterministic Residual Structure (DRS) is a pair R = (A, /), where A = (T er, Red, →) is an ARS and / is a residual relation on redexes relating redexes in the source and target term of every reduction t→^{u}s ∈ A, such that for v ∈ t, the set v/u of residuals of v under u is a set of redexes of s; a redex in s may be a residual of only one redex in t under u, and u/u = ∅. If v has more than one u-residual, then u duplicates v. If v/u = ∅, then u erases v; and if moreover v ≠ u, then u discards v. A redex of s which is not a residual of any v ∈ t under u is said to be u-new or created by u. The set u/P of residuals of u under any finite P : t → → o 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 if P 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] ([GLM92]) All developments are terminating; all complete developments of U ⊆ t end at the same term; and residuals of a redex v ∈ t under all complete developments of U are the same.

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

We call a DRS R stable (SDRS) if:

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

Lemma 82 ([GK02]) Let S be a stable semantics of an SDRS, and let P :

t→^{u}s → → ∈ S. Further:

(1) Let v′ be a u-residual of v ∈ t, and let v be S-unneeded. Then so is v′.

(2) Let u create v ∈ s, and let u be S-unneeded. Then so is v.

(3) Let S be regular, let u ≠ v ∈ t, and let v be S-needed. Then v has at least one S-needed residual in s.

(4) Let S be regular. Then [P]_{S} is an S-needed reduction whose length coincides with the number of S-needed steps in P, and P ≈_{S} [P]_{S}.

Remark 83 Note that without regularity [P]_{S} ⊴_{S} P need not hold in general: Consider the DRS generated by the rewrite system R = {f(x) → g(x, x), a → b}, restricted to the reduction graph of t = f(a), let S_{ter} be the set of terms (in the reduction graph of t) not containing occurrences of a, and let S be the set of all S_{ter}-normalizing reductions. Then S is stable but not regular since the Sunneeded step f(a) → g(a, a) duplicates the S-needed redex a ∈ t, and we have for P : f(a) → g(a, a) → g(b, a) that [P]_{S} : f(a) → f(b), and [P]_{S} ⋬_{S}P.

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

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

(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(P u) ↪ F am((P + u)v).

[FFD] Any reduction that contracts redexes of a finite number of families is terminating.

9 Appendix C: Proofs

Proof of Lemma 31: (⇒) By Definition 22, P ⊴_{S} Q implies that P/Q is S-unneeded. But P ⊴_{L} Q + P/Q, and we can take P/Q for Q′. (⇐) By Definition 22, we need to show that P/Q is S-unneeded. Suppose on the contrary that P/Q = N′+v+N′′ where N′ is S-unneeded and v is S-needed. By Lemma 82.(1), Q′/N′ is S-unneeded, thus by Lemma 82.(3) v must have at least one (S-needed) residual under Q′/N′, contradicting (P/Q)/Q′ = P/(Q + Q′) = ∅.

Proof of Lemma 32: First assume that P, Q and N are finite. By Lemma 31, P ⊴_{S} Q ⊴_{S} N implies P ⊴_{L} Q + Q′ and Q ⊴_{L} N + N′ for some S-unneeded Q′ and N′. But Q ⊴_{L} N + N′ implies Q + Q′ ⊴_{L} N + N′ + Q^{∗} (see the figure), where Q^{∗} = Q′/((N + N′)/Q) is S-unneeded. Thus P ⊴_{L} N + N′ + Q^{∗} where N′ + Q^{∗} is S-unneeded, and P ⊴_{S} N by Lemma 31. Thus the lemma is proved when P, Q and N are finite. Now let us consider the general case. By Definition 22 and P ⊴_{S} Q, for any finite P′ ≤ P there is a finite Q′ ≤ Q such that P′ ⊴_{S} Q′.

Similarly, there is a finite N′ ≤ N such that Q′ ⊴_{S} N′, thus P′ ⊴_{S} N′, implying again by Definition 22 that P ⊴_{S} N.

[figure: N; N′]

[figure: Q; ∅]

[figure: Q′; Q^{∗}]

Proof of Lemma 35: Suppose on the contrary P = P′ + v + P′′, where v is S-needed. Then By Lemma 82.(1) and Lemma 82.(3), Q/P′ is S-unneeded and v/(Q/P′) contains at least one (S-needed) redex, contradicting P ⊴_{L} Q.

Proof of Lemma 36: It is enough to prove the lemma for finite P, Q. By Lemma 31, P ⊴_{L}Q+Q′ for some S-unneeded Q′, implying that P/N⊴_{L}Q/N+Q^{∗}, where Q^{∗} = Q′/(N/Q) is S-unneeded by Lemma 82.(1). Hence P/N ⊴_{S} Q/N again by Lemma 31.

Proof of Lemma 311: Suppose in contradiction that w is the first step in N that is not a residual of a redex in U, say N = N′ + w + N′′. Since w is S-needed and w/(U/N′) is S-unneeded, U/N′ must contract a residual w′ of w, say U/N′ = P′ + w′ + Q′. Thus U = P + u′ + Q where P′ = P/N′ and w′ ∈ u′/(N′/P) ⊆ u/(P ⊔ N′) for some redex u ∈ U (see the figure). But by the Cube Lemma, w′ ∈ u/(N′ ⊔ P), thus w′ is a P′-residual of a redex in the final term of N′, and that latter redex must coincide with w (since w′ ∈ w/P′ and a redex can be a residual of at most one redex along a reduction in an SDRS) – a contradiction.

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

[figure: ·; N′; P′; ·; N′/P; w′]

[figure: w; w′]

Proof of Lemma 312: By Lemma 82.(4), we can assume that both P and Q are S-needed, and that Q is finite, and we want to prove that P is finite too. Suppose not. Since P/Q is S-unneeded, there is a step u of Q, say Q = Q′ + u + Q′′, such that P/Q′ contracts infinitely many S-needed redexes while P/(Q′+u) contracts only a finite number of them. Let P = P′ + P′′, where P′′/((Q′ + u)/P′) is Sunneeded, let N = P′′/(Q′/P′) and U = u/(P′/Q′) (see the figure). Thus we have N ⊴_{S} U. Hence N′ = [N]_{S} ⊴_{S} U′, where U′ is the set of S-needed redexes in U, and N′ is an infinite S-needed reduction by Lemma 82.(4), contradicting Lemma 311.

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

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

[figure: P′′; N]

Proof of Lemma 313: (⇒) Let ⟨P ⟩_{S} be finite. We can assume by Lemma 312 that P is S-needed and finite. Now let ⟨Φ⟩_{S} be directed and ⟨P ⟩_{S} ⊴_{S} ⟨⊔_{S}Φ⟩_{S}. Then P ⊴_{S} ⊔_{S}Φ, and by Lemma 37, P ⊴_{S} ⊔_{S}Φ[k] for some k, where Φ[k] ⊆ Φ is finite. Since ⟨Φ⟩_{S} is directed, ∃N ∈ Φ.⊔_{S} Φ[k]⊴_{S} N. Thus ⟨P ⟩_{S} ⊴_{S} ⟨N⟩_{S} ∈ ⟨Φ⟩_{S}, which means that ⟨P ⟩_{S} is finite in L^{⊴_{S}} (R). (⇐) Let ⟨P ⟩_{S} be finite in L^{⊴_{S}} (R), and let P be infinite (otherwise ⟨P ⟩_{S} is trivially finite). It is immediate from Definition 34 that P = ⊔_{S}{⌈P ⌉^{k}|k ∈ N }, thus P ⊴_{S} ⊔_{S}{⌈P ⌉^{k}|k ∈ N }, and clearly {⌈P ⌉^{k}|k ∈ N } is directed. Hence by finiteness of ⟨P ⟩_{S} in L^{⊴_{S}} (R), P ⊴_{S} ⌈P ⌉^{n} for some n, which by definition of ⊴_{S} means that ⌈P ⌉_{n} is S-unneeded. Hence ⟨P ⟩_{S} is finite.

Proof of Lemma 43: It is immediate from Definition 41 that for any redex t→^{u}_{S}s in R_{S}, and redexes v ∈ t and w ∈ s, v/_{S}u is a set of redexes in s, and that w can be the u-residual of at most one redex in t. Further, R_{S} is non-erasing by Lemma 82.(3), which immediately implies [weak acyclicity]. And [stability] for R_{S} follows immediately from [stability] for R. Thus it remains to check [FD] and [AF].

[FD]: Let U ⊆ t in R_{S}. Then t = ⟨P ⟩_{S} for some finite initial reduction P in R (P can be taken S-needed), and let U′ be the set of corresponding (to U) Rredexes in the final term of P. By [FD] for R, all complete U′-developments Q end at the same term and generate the same residual relation −/U′. Hence any complete development of U in R_{S} ends at ⟨P + [Q]_{S}⟩_{S}. Further, since Q ≈_{L} [Q]_{S}+Q′ for some S-unneeded Q′ in R, we have by the regularity of S and Lemma 82 that any S-needed redex in the final term of Q is the unique Q′-residual of exactly one S-needed redex in the final term of [Q]_{S} (the correspondence between the redexes in the final terms of Q and [Q]_{S} is 1 − 1). Hence any complete development of U in R_{S} generates the same residual relation −/_{S}U, and [FD] for R_{S} follows.

[AF]: Let P′, Q′ be initial reductions in R_{S} ending at the same term. Then (by Definition 41) there are S-needed reductions P = h′(P′), Q = h′(Q′) in R such that h(P) = P′ and h(Q) = Q′, and ⟨P ⟩_{S} = ⟨Q⟩_{S} (since P and Q end at the same term). Thus it is enough to prove that for any reductions P, Q in R, P ≈_{S} Q implies h(P) ≈_{L} h(Q) in R_{S}. To this end, we first prove that:

(a) Let P, Q be finite initial reductions in R. Then h(P/Q) = h(P)/h(Q). Proof of (a): By induction on the number of multisteps in P and Q (it does

not matter how do we group steps in P and Q into multi-steps). The case P = ∅ is trivial, so let P = P_{1} + P_{2} be non-empty. Then

h(P/Q) = h((P_{1} + P_{2})/Q)
= h(P_{1}/Q + P_{2}/(Q/P_{1}))
= h(P_{1}/Q) + h(P_{2}/(Q/P_{1}))
= h(P_{1})/_{S}h(Q) + h(P_{2})/_{S}(h(Q)/_{S}h(P_{1}))
= (h(P_{1}) + h(P_{2}))/_{S}h(Q)
= h(P_{1} + P_{2})/_{S}h(Q)
= h(P)/_{S}h(Q).

Now, by (a), P ⊴_{S} Q iff P/Q is S-unneeded iff h(P/Q) = ∅ iff h(P)/_{S}h(Q) = ∅ iff h(P) ⊴_{L} h(Q) (in R_{S}), and the lemma follows.

Proof of Lemma 48: By induction on the length n of a longest covering (t, ⊔s_{i})- chain P (n is finite by [FB],[FC] and König’s Lemma). The case n = 1 is trivial by [NT]. Assume (without loss of generality) that P starts with t −< s_{1}, let [s_{1}, e_{j}] (1 ≤ j ≤ k) be all residuals of [t, s_{i}] in s_{1}, and let [s_{1}, o_{r}] (1 ≤ r ≤ l) be all residuals of [t, s]. Clearly, ⊔s_{i} = ⊔e_{j}. (Indeed, e_{j} ≤ s_{1} ⊔ s_{i_{j}} for any j and some i_{j}, by definition of residuals, thus ⊔e_{j} ≤ ⊔s_{i}; conversely, s_{i} ≤ e_{j_{i}} for any i and some j_{i}, thus ⊔s_{i} ≤ ⊔e_{j}.) By [SD], e_{j} and o_{r} are pairwise different. By the induction assumption, for any r, ⊔e_{j} < o_{r} ⊔ (⊔e_{j}), thus ⊔e_{j} < (⊔o_{r}) ⊔ (⊔e_{j}). Hence, by [FC], ⊔s_{i} < (s ⊔ s_{1}) ⊔ (⊔s_{i}) = s ⊔ (⊔s_{i}). Finally, s < s ⊔ (⊔s_{i}) follows immediately from s < s ⊔ s_{1} (which holds by [NT]).

Proof of Lemma 49: By induction on n.

(⇒) Let [e_{m}, e_{m}^{∗}] be a residual of [e_{0}, e_{0}^{∗}]. Then [e_{m}, e_{m}^{∗}] is a residual of a residual [e_{m−1}, e_{m−1}^{∗}] of [e_{0}, e_{0}^{∗}] in e_{m−1}. By definition of /_{D} and the induction assumption, e_{m}^{∗} ≤_{D} e_{m} ⊔_{D} e_{m−1}^{∗} ≤_{D} e_{m} ⊔_{D} (e_{0}^{∗} ⊔_{D} e_{m−1}) = e_{m} ⊔_{D} e_{0}^{∗}.

(⇐) Let e_{m}^{∗} ≤_{D} e_{0}^{∗} ⊔_{D} e_{m}. Further, let [e_{m−1}, e_{m−1}^{i}] (0 ≤ i ≤ p) be all prime intervals such that e_{m−1}^{i} ≤_{D} e_{0}^{∗} ⊔_{D} e_{m−1}. By (⇒) and the induction assumption, [e_{m−1}, e_{m−1}^{i}] are all residuals of [e_{0}, e_{0}^{∗}]. If on the contrary [e_{m}, e_{m}^{∗}] is not a residual of any of [e_{m−1}, e_{m−1}^{i}], then e_{m}^{∗} ≰_{D} e_{m} ⊔_{D} e_{m−1}^{i}, for all 0 ≤ i ≤ p. Hence, by Lemma 48, e_{m}^{∗} ≰_{D} e_{m} ⊔_{D} (⊔_{D}e_{m−1}^{i}) = (by the induction assumption) = e_{m} ⊔_{D} (⊔_{D}(e_{0}^{∗} ⊔_{D} e_{m−1})) = e_{0}^{∗} ⊔_{D} e_{m}.

Proof of Theorem 51: To prove that ≃_{S} is a family relation on R_{S}, let us first show that ≃_{z}⊆≃_{S}. So let v′ ≃_{z} w′ in F_{S}, where v′ = (⟨P ⟩_{S}, ⟨P + v⟩_{S}) and w′ = (⟨Q⟩_{S}, ⟨Q + w⟩_{S}). Since ≃_{S} is clearly an equivalence relation, it is enough to consider the case when say w′ is a copy of v′, i.e. Q ≈_{L} P + N and w ∈ v/N for some N. Then P v ≃_{z} Qw in F, thus P v ≃ Qw, implying v′ ≃_{S} w′ (by the definition of ≃_{S}). Now we need to check the family axioms for ≃_{S}.

[initial]: This is immediate by [initial] in F: any initial redexes ∅u and ∅v in F_{S} are also initial redexes in F and therefore ∅u ≄ ∅v, implying ∅u ≄_{S} ∅v.

[contribution]: since we assume that the contribution relation ↪_{S} of F_{S} is defined from ≃_{S} via [contribution], there is nothing to prove.

[creation]: Let e → →^{P} _{S}t→^{u}_{S}s in F_{S}, let u create v ∈ s, and let P′v′ ≃_{S} (P + u)v. We need to show that P′ contracts a redex in the ≃_{S}-family of P u. By the definition of ≃_{S}, h′(P′v′) ≃ h′((P + u)v). By [creation] for F, h′(P′) contracts a redex P′′u′′ in the ≃-family of h′(P u), implying (by the definition of ≃_{S}) that h(P′′u′′) ≃_{S} P u (where h(P′′u′′) is a redex contracted in P′), and we are done.

[FFD]: Easy, by the construction.