An Abstract Böhm-normalization

John Glauert^{1}

School of Information Systems, UEA Norwich NR4 7TJ, UK

Zurab Khasidashvili^{2}

Department of CS, Bar-Ilan University Ramat-Gan 52900, Israel

1 Introduction

A normalizable term in a rewriting system may have an infinite reduction, so it is important to have a normalizing strategy which enables one to construct reductions to normal form. For example, it is well known that the leftmostoutermost strategy is normalizing in the λ-calculus [12]. For Orthogonal TRSs, a general normalizing strategy, called the needed strategy, was found by Huet and Lévy [19]. The strategy always contracts a needed redex – one whose residual has to be contracted in any reduction to normal form. Huet and Lévy showed that any term not in normal form has a needed redex, and that repeated contraction of needed redexes leads to its normal form whenever there is one. (They also defined strongly sequential orthogonal TRSs where a needed redex can be computed effectively in every reducible term. We will not discuss this topic here.)

This fundamental work on neededness has been extended in several directions. Barendregt et al. [6], Maranget [34], Nöcker [38] and Middeldorp [37] studied neededness w.r.t. head-normal forms, weak head-normal forms, constructor head-normal forms, and root-stable forms, respectively. Sekar and Ramakrishnan [42] studied normalization via necessary sets of redexes. Kennaway et al. [22] studied a needed strategy for infinitary orthogonal TRSs. A different approach to normalization is developed in Kennaway [20] and Antoy and Middeldorp [3]. Antoy et al. [2] designed a needed narrowing strategy. Gardner [13] described a complete way of encoding neededness information using a type assignment system. Khasidashvili [23,24] introduced a refinement of the needed strategy which is based on a concept of descendant which refines

1 Email: jrwg@sys.uea.ac.uk
2 Email: khasidz@cs.biu.ac.il

that of residual. Melliès [36] and van Oostrom [40] extended the needed and essential strategies, respectively, to some non-orthogonal systems.

In [15], the present authors addressed the question of normalization relative to a desired set of final terms, considering the properties that a set S of terms must possess in order for the neededness theory of Huet and Lévy still to make sense. This work is done in the context of orthogonal Expression Reduction Systems (ERSs), a formalism for rewriting which subsumes Term Rewriting and the λ-calculus. Natural conditions were imposed on S, called stability, that are sufficient for the following Relative Normalization (RN) theorem to hold: each S-normalizable term not in S (that is, not in S-normal form) has at least one S-needed redex, and repeated contraction of such redexes always leads to an S-normal form. It is shown also that if a stable S is regular, i.e., if S-unneeded redexes cannot duplicate S-needed ones, then the S-needed strategy is hypernormalizing as well, and minimal (w.r.t. the Lévy-embedding relation) S-normalizing reductions exist.

In [14], we further generalized the theory by abstracting from the structure of terms. We studied relative normalization in Deterministic Residual Structures (DRSs), which are abstract reduction systems with an axiomatized residual relation. Despite their highly abstract nature, a counterpart of the stability property of Berry [8] and Winskel [44] enabled us to prove the RN theorem for all regular stable sets S. (We actually prove the Relative Hypernormalization theorem.) We show that without this stability axiom the theorem fails. The proof method employed is similar to that in [23,24], and is based on the fact that S-needed steps in a reduction can be pushed before S-unneeded steps without affecting the number of S-needed steps. In [26], we studied discrete normalization in SDRSs, which is normalization relative to particular (finite or infinite) reductions.

Here we extend the concepts of stability and regularity from sets of terms (which represent ‘finite’ results, or values, such as head normal forms) to sets of reductions, to represent the concepts of ‘infinite’ values, such as Böhm trees. Throughout the paper, we restrict ourselves to finite terms – terms can contain only a finite number of redexes. For regular stable sets S of finite or infinite results and an S-normalizable term t, in an SDRS, we show that all S-needed fair reductions starting from t are S-normalizing, and if t has a finite S-normalizing reduction, then any S-needed reduction starting from t eventually normalizes t in a finite number of steps. This result unifies the Relative Hypernormalization theorem with the Discrete Normalization theory. We also show that for S-minimal reductions to exist, for regular stable sets of finite results S, every S-normalizing term must possess an S-needed Serased redex (where a redex is S-erased if it does not have a residual under S-normalizing reductions).

The paper is organized as follows. In the next section, we recall SDRSs and present some fundamental lemmas concerning (mutually) external reductions. In section 3, we give a construction of the meet operation with respect to Lev́y’s ordering on reductions. In Section 4, we introduce the concept of stability for sets of reductions, and give examples. In Section 5, we prove the RN theorem for regular stable sets of reductions in SDRSs, and present the minimality results. Conclusions appear in Section 6.

2 Deterministic Residual Structures

In this section we recall Deterministic Residual Structures (DRSs) which are Abstract Reduction Systems (ARSs) satisfying certain properties concerning residuals. Residuals of redexes were first introduced and studied by Church and Rosser in the λI-calculus [11]. The study of abstract systems with residuals started from Hindley [17].

The definition and some results about ARSs can be found e.g., in [29,18]. Our definition is slightly different.

Definition 2.1 An ARS is a triple A = (Ter,Red,→) where Ter is a set of terms, ranged over by t, s, o, e; Red is a set of redexes (or redex occurrences), ranged over by u, v, w; and →: Red → (T er × T er) is a function such that for any t ∈ T er there is only a finite set of u ∈ Red such that → (u) = (t, s), written t→^{u}s. This set will be known as the redexes of term t, where u ∈ t denotes that u is a member of the redexes of t and U ⊆ t denotes that U is a subset of the redexes. Note that → is a total function, so one can identify u with the triple t→^{u}s. (Klop’s ARSs [29] are pairs (T er, →), and do not allow one to distinguish transitions with the same source and target terms.) A reduction is a sequence t→^{u_{1}}t_{2}→^{u_{2}} . . ..

Notation 2.2 Reductions are denoted by P, Q, N. We write P : t → → s or t → →^{P} s if P denotes a reduction (sequence) from t to s. 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.

Definition 2.3 (Deterministic Residual Structure) 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, 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 v/P of residuals of v 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. The residual relation satisfies the following two axioms:

[FD] (Finite Developments [16]) 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. Below U will also denote a complete development of U ⊆ t.

[weak acyclicity] ([43]) Let u, v ∈ t, u ≠ v, and u/v = ∅. Then v/u ≠ ∅.^{3}

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

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

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

DRSs are closely related to Determinate Concurrent Transition Systems (DCTS) of Stark [43], and to Abstract Reduction Systems (ARSs) of Gonthier et al. [16]. The main difference from DCTSs is that Stark requires a nonduplicating residual relation. Unlike ARSs of [16], we do not have a nesting relation on redexes and the corresponding axioms, and the stability axiom is modified accordingly. Instead, we study properties of conflict-free transition and reduction systems based on the duplication and erasure effect of executed transitions on the others, and develop a theory that is applicable to systems with nested transitions too. Other related abstract reduction systems are studied in [35,39,41].

One can verify that all orthogonal (first or fully extended higher-order, see e.g., [41]) term rewriting systems, such as the λ-calculus, form DRSs. These systems are stable, and can be shown so just using an appropriate notion of descendant which assigns the contractum to the contracted redex – labelling is not necessary. Further, orthogonal Term Graph Rewriting Systems [21] are DRSs but they do not satisfy all the nesting axioms of [16].

The properties of the residual relation in orthogonal systems are all standard [19,31,9,32,10,43,35], and we only review quickly the main constructions used in this paper. In a DRS R, Lévy-equivalence or permutation-equivalence is defined as the smallest relation on co-initial finite 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 sets of redexes in the same term. The residual relation on redexes is extended to all co-initial reductions as follows: (P_{1}+P_{2})/Q = P_{1}/Q+P_{2}/(Q/P_{1}) and Q/(P_{1} + P_{2}) = (Q/P_{1})/P_{2}. The Lévy-embedding relation on co-initial finite reductions, ⊴_{L}, is defined by: P ⊴_{L} Q iff P/Q = ∅. One can show that P ≈_{L} Q iff P ⊴_{L} Q and Q ⊴_{L} P and that P ⊴_{L} Q iff Q ≈_{L} P + N for some N. Intuitively, P ⊴_{L} Q expresses that Q does more work than P, and Q/P is the part of Q that remains after P has been done. Further, one can prove

3 This axiom is called [acyclicity] in [14], and is axiom (4) in [43].

the following strong Church-Rosser theorem for DRSs: For all co-initial finite reductions P and Q in a DRS, P ⊔ Q ≈_{L} Q ⊔ P, where P ⊔ Q abbreviates P + Q/P. And finally, we will also need the following Cube Lemma: for any finite co-initial reductions P, Q and N, N/(P ⊔ Q) = N/(Q ⊔ P).

Lévy-equivalence extends to infinite reductions as follows. First, for any u ∈ t → →^{P} , define u/P = ∅ if u/P′ = ∅ for some finite P′ ≤ P (we say u is erased in P). Now, for any co-initial P, Q, define P/Q = ∅, or equivalently, P ⊴_{L} Q, if for any redex v contracted in P, say P = P′ +v +P′′, v/(Q/P′) = ∅ (see the diagram); and define P ≈_{L} Q iff P ⊴_{L} Q and Q ⊴_{L} P.

[figure: P′; v; P′′; P; Q; Q/P′]

Finally, P/Q is only defined for finite Q, as the reduction whose initial parts are residuals of the initial parts of P under Q.

The [stability] axiom is not used in the above constructions. Intuitively, stability means that a redex cannot arise from two unrelated sources. This property has a natural extension to many-step reductions, where ‘unrelated’ is formalized by the notion of external which captures the concept that two external reductions do not contract redexes that have common residuals (although the contracted redexes may have ‘inessential’ common ancestors).

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

• Let P : t_{0} → →^{P_{i}} t_{i}→^{u_{i}}t_{i+1} → → t_{n} and Q : t_{0} = s_{0} → →^{Q_{j}} s_{j}→^{v_{j}}s_{j+1} → → s_{m}. 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}; ·]

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

Recall from [19] that in concrete orthogonal rewrite systems, a redex is said to be external if its residuals never appear inside arguments of other redexes. It should be clear from the context to which concept of external we are referring.

Lemma 2.5 Let P : t_{0}→^{v_{0}}t_{1}→^{v_{1}} … → t_{n} be external to U = {u_{1}, …, u_{n}} ⊆ t_{0},

and let Q_{0} : t_{0} → → o_{0}. Then P′ = P/Q_{0} is external to the set U′ = U/Q_{0}.

We conclude this section by presenting two fundamental lemmas, which generalize the [weak acyclicity] and [stability] axioms to many-step reductions [14].

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

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

[figure: t; P; s ⊇ W; e; Q; P/Q; o ⊇ W/(Q/P); Q/P]

3 Construction of the ⊴_{L}-meet operation

In this section we give a construction of the ⊴_{L}-meet operation (to be used in the subsequent sections) and prove its correctness. This implies that ⊴_{L} is a complete lattice on Lévy-equivalence classes of reductions. This lattice was first constructed by Berry and Lévy [9], for the case of Recursive Program Schemes (RPSs), as the ideal completion of the upper semi-lattice on Lévyequivalence classes of finite reductions.

Below, in our construction of ⊴_{L}-meets, Φ denotes a set of co-initial reductions in a DRS. Further, for example, we write P ⊴_{L} Φ iff ∀Q ∈ Φ. Q ⊴_{L} P; ⌈Φ⌉^{k} denotes the set of initial parts, of length k, of reductions in Φ; etc.

Definition 3.1 (⊴_{L}-meet) 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 U-development (or the multi-step contracting U). Then ⊓_{L}Φ = U + ⊓_{L}(Φ/U).

Theorem 3.2 Let Φ be a set of co-initial reductions in a DRS. Then ⊓_{L}Φ is a (unique up to ≈_{L}) ⊴_{L}-meet of Φ. Proof Let ⊓_{L}Φ = Q : t_{0} → →^{U_{0}} t_{1} → →^{U_{1}} t_{2} → → . . .. It is immediate from the construction that ⊓_{L}Φ ⊴_{L} Φ. Thus we need to show that for any P : t_{0} → → such that P ⊴_{L} Φ, P ⊴_{L} Q, that is, for any n < |P |, ⌈P ⌉^{n} ⊴_{L} 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} ⊴_{L} Q. Then ⌈P ⌉^{k} ⊴_{L} ⌈Q⌉^{l_{k}} for some l_{k}. We can assume that ⌈Q⌉^{l_{k}} ends at t_{m} for some m. Thus ⌈Q⌉^{l_{k}} ≈_{L} ⌈P ⌉^{k} + Q′_{k} for some finite Q′_{k}, and Φ/⌈Q⌉^{l_{k}} consists of Q′_{k}-residuals of reductions in Φ/⌈P ⌉^{k}, up to ≈_{L}. Let v be the (k + 1)th step of P. Since P ⊴_{L} Φ, v ⊴_{L} Φ/⌈P ⌉^{k}, thus by the Cube Lemma, (v/Q′_{k}) ⊴_{L} Φ/⌈Q⌉^{l_{k}}, and therefore v/Q′_{k} ⊆ U_{m} by Definition 3.1. This means that ⌈P ⌉^{n} ⊴_{L} Q. Thus P ⊴_{L} Q, and ⊓_{L}Φ is a ⊴_{L}-meet of Φ.

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

[figure: N ∈ Φ; N/⌈P ⌉^{k}; N/⌈Q⌉^{l_{k}}]

4 Stable sets of finite or infinite results

In this section, we will introduce the concepts of stability, regularity and superstability of sets of reductions, to cover usual concepts of infinite results, such as Böhm-trees. From this definition, our earlier concepts of stability and regularity for sets of finite results [14,15] can be obtained as a special case. Moreover, to any reduction P we will associate a stable set S_{P} of reductions, which will allow us to infer Discrete Normalization and Standardization results [26] from our normalization results in the next section.

We start by recalling the concepts of relative neededness, and of stability and regularity of sets of terms [14,15], and introduce superstability. The latter will allow us to extend our results concerning minimal relative normalization [15] to the abstract framework of SDRSs.

Definition 4.1 Let S be a set of terms in a DRS 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 u S-unneeded otherwise.

(2) We call S stable iff:

[RC] S is closed under reduction: if t ∈ S and t → s, then s ∈ S, and [CUE] S is closed under unneeded expansion: for any e→^{u}o such that e ∉ S

and o ∈ S, u is S-needed.

(3) Further, we call a stable set S regular iff:

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

(4) Finally, we call a regular stable set S superstable iff:

[Min] For any S-normalizable term t, the set of all S-normalizing reductions starting from t contains a unique, up to ≈_{L}, ⊴_{L}-minimal element. Such a reduction will be called S-minimal.

Examples of stable sets are normal forms [19], head normal forms in the λ-calculus [6], weak head normal forms in the λ-calculus [1], constructor head normal forms for constructor TRSs [38], and root stable forms in orthogonal TRSs [37]. All the above sets are regular. Other examples include weak-head-normal forms (up to garbage-collection, modulo a congruence) in Yoshida’s λf-calculus (an environment calculus) [46], the set of answers in the call-by-need λ-calculus of Ariola et al. [4], and flexible generalized head normal forms in the λ_{hd}^{v}-calculus of Xi [45]; all are conditional rewrite systems.

Although all normalizing reductions are minimal w.r.t. the set of normal forms, this is not so for other concepts of results. For example, for the set of head-normal form, only the reductions Lévy-equivalent to the leftmostoutermost head-normalizing reductions are minimal. Head-minimal reductions compute the principal head-normal forms [5], from which all other headnormal forms are accessible.

An example of an irregular stable set is given in [14]. The next example exhibits a regular stable set which is not superstable:

Example 4.2 Consider the SDRS given by the following diagram

t  \overline{u  ^{}}t_{2}
[figure: v_{1}; v_{2}]
o_{1}  o_{2}
[figure: v′_{2}; v′_{1}]
s_{1}
[figure: u_{1}; u′_{2}]
t_{1} v_{}t′
[figure: u_{2}; u′_{1}]
s_{2}

where u/v = {u_{1}, u_{2}}, v/u = {v_{1}, v_{2}}, v_{1}/v_{2} = {v′_{1}}, v_{2}/v_{1} = {v′_{2}}, u_{1}/u_{2} = {u′_{1}}, u_{2}/u_{1} = {u′_{2}}, and let S = {o_{2}, s_{2}, t′}. Then S is regular stable but not superstable, as one can easily verify that there is no S-minimal reduction starting from t.

Definition 4.3 Given a set S of reductions in a DRS R and a term t in R, we call t S-normalizable if S contains a reduction P starting from t; P is then called S-normalizing.

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

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

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

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

Lemma 4.5 Let P, Q be co-initial reductions in a DRS. Then P ⊴_{L} Q implies P ⊴_{S} Q and P ≈_{L} Q implies P ≈_{S} Q.

Definition 4.6 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 will be called Sminimal.

Note that, for a set of terms S_{ter} in a DRS, stability of S_{ter} follows easily from stability of the corresponding set S_{red} of S_{ter}-normalizing reductions – (possibly infinite) reductions starting outside S_{ter} and entering it. Indeed,

[CE] (for S_{red}) implies [RC] (for S_{ter}). And [CN] implies [CUE] (since any step entering S_{ter} is an S_{red}-normalizing reduction, thus is S_{red}-needed and therefore S_{ter}-needed too).

Conversely, if S_{ter} is stable, then S_{red} is stable as well: [CS] is immediate,

[CN] follows from [CUE], and [CE] follows from [CUE] and [RC]. (Indeed, to prove [CE], let P ∈ S_{red} and P ⊴_{S_{red}} Q. Further, let P′ ≤ P be finite and P′ ∈ S_{red}. Then there is a finite Q′ ≤ Q such that P′ ⊴_{S_{red}} Q′. i.e., P′/Q′ is S_{red}-unneeded, hence S_{ter}-unneeded. By [RC], P′/Q′ ends in S_{ter}. And by [CUE], Q′ too ends in S_{ter}. Hence Q ∈ S_{red}, and [CE] is proved.)

Now it is immediate that S_{ter} is regular, resp. superstable, iff so is S_{red}. Furthermore, S-neededness and related concepts are not affected if we view S_{ter} as the corresponding set S_{red} of reductions. Therefore, in the following, we will often tacitly identify S_{ter} with S_{red}.

Given a reduction P in an SDRS R, we can also construct its corresponding stable set S_{P} as follows. Let R_{P} be an SDRS whose terms are Lévy-equivalence classes ⟨Q⟩_{L} of finite initial parts of reductions in ⟨P ⟩_{L}, whose redexes are pairs ⟨Q⟩_{L} → ⟨Q + u⟩_{L}, where u is a redex in the final term of Q, and the residual relation is the induced one: If ⟨Q⟩_{L}→^{u^{∗}}⟨Q + u⟩_{L} and ⟨Q⟩_{L}→^{v^{∗}}⟨Q + v⟩_{L} in R_{P}, then for any v′ ∈ v/u, ⟨Q + u⟩_{L}→^{v^{′∗}}⟨Q + u + v′⟩_{L} is a u^{∗}-residual of v. (This definition is sound since Q + u + v′ ⊴_{L} P.) R_{P} is an SDRS since its reduction graph is isomorphic to ⟨P ⟩_{L}, and in addition, R_{P} is acyclic. Now S_{P} is defined as the set of all suffixes of reductions in R_{P} corresponding to reductions in ⟨P ⟩_{L} (hence reductions in S_{P} are ‘maximal’ in some sense). Hence S_{P} is suffix-closed, and it satisfies [CE] since all co-initial reductions in R_{P} are Lévy-equivalent (because of the above ‘maximality’ property). When P is finite, the last step of any (non-empty) reduction in S_{P} is S_{P} -needed by Lemma 2.6, implying [CN] and thus stability of S_{P}.

When P is infinite, [CN] does not hold in general (in SDRSs), as can be seen from the diagram below (only a finite part of the infinite reduction graph is shown). Each non-empty horizontal step creates its next horizontal step, and similarly for vertical steps; every redex has at most one residual on the opposite side of each elementary diagram, and erasure is indicated by empty steps ∅. The SDRS axioms are not violated. Further, the infinite reductions u_{0} + u_{1} + … and v_{0} + v_{1} + … are Lévy-equivalent but they contract different, hence unneeded, redexes. Clearly, no normalization-by-neededness theory can be developed for such reductions.

[figure: ·; u_{0}; ·; u_{1}; ·]

[figure: ·; v_{0}; ·; u′_{1}; ·; ∅; u_{2}; ·]

[figure: ·; v_{1}; ∅; ·; v′_{1}; ·; u′_{2}; ·; ∅]

[figure: ·; v_{2}; ∅; ·; v′_{2}]

Let us recall concepts related to neededness w.r.t. particular reductions P, or discrete neededness, from [26].

Definition 4.7 ^{•} Let P : t → → and u ∈ t, in a DRS. 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, in a DRS. We say that u is Qneeded, or more precisely, P′u is Q-needed, if u is Q/P′-needed. We call P Q-needed if every redex contracted in P is Q-needed. We call P self-needed or standard if it is P -needed.

It is easy to verify that P -neededness of redexes occurring in terms of reductions in ⟨P ⟩_{L} coincides with S_{P} -neededness, and in particular standard reductions P are simply S_{P} -needed reductions. Hence the stability concept for sets of reductions allows to unify the existing relative and discrete normalization theories (as far as normalization-by-neededness is concerned).

It is easy to check that for example the sets of reductions ‘computing’ Böhm-trees [5] or Lévy-Longo-trees [30,33] or Berarducci-trees [7] are stable and regular. To make this precise, let us consider the Böhm-tree semantics of the λ-calculus. Recall that the immediate syntactic value ω(t) of a λterm t is defined by: ω(t) = ⊥_{B} if t is not a head normal form, and ω(t) = λx_{1} … x_{m}.yω(t_{1}) … ω(t_{n}) if t = λx_{1} … x_{m}.yt_{1} … t_{n}, where ⊥_{B} is a special constant which denotes the ‘undefined’. Then the Böhm-tree or Böhm-normal-form BT (t) of t, which is the value of t according to Böhm-semantics, is defined by BT (t) = ⊴_{Ω}−lub{ω(t) | t → → _{β}s}, where ⊴_{Ω} is the minimal contextclosed ordering on λ-⊥_{B}-terms (i.e., λ-terms possibly containing occurrences of ⊥_{B}) generated by ⊥_{B} ⊴_{Ω} t for any λ-⊥_{B}-term t.

Now let us define the Böhm-approximant computed by P : t_{0} → t_{1} → …, written ω(P), by ω(P) = ⊴_{Ω}− lub{ω(t_{i}) |, i = 0, 1….}. It is well known that t → → s implies ω(t) ⊴_{Ω} ω(s), thus in particular for a finite P : t_{0} → → t_{k}, ω(P) = ω(t_{k}). Now we can define that P : t_{0} → → computes BT (t_{0}) iff ω(P) = BT (t_{0}). Let us call a subterm of t an ⊥_{B}-subterm if its corresponding occurrence in ω(t) is ⊥_{B}. Recall that the standard way to approximate BT (t_{0}) sequentially is to construct ‘iterated head-reductions’ P : t_{0} → →^{P_{0}} t_{1} → →^{P_{1}} …, where P_{i} is the head-reduction computing the principal head normal form of one of the ⊥_{B}-subterms of t_{i} having a head normal form. In order to compute BT (t_{0}), P must be ‘fair’, i.e., every ⊥_{B} subterm of every t_{i} having a head normal form must eventually be dealt with in P; we call such reductions P canonical Böhm-reductions.

Regularity and stability of the set S_{B} of reductions computing Böhm-trees follow easily from the top-down manner of construction of Böhm-trees: [CS] is immediate; [CN] follows from the fact that head redexes of ⊥_{B}-subterms of any λ-term t are S_{B}-needed; and [CE] follows from a simple observation that Q ∈ S_{B} iff P ⊴_{S_{B}} Q for some canonical Böhm-reduction P. The axiom [Reg] follows from the fact that if a β-redex u ∈ t is nested in an S_{B}-unneeded β-redex v, then for any canonical Böhm-reduction P : t → → , P does not contract residuals of v, and therefore it does not contract residuals of u as any residual of u is nested inside a residual of v. Finally, [Min] follows from the fact that P ⊴_{L}⊓_{L}S_{B}^{∗} for any canonical Böhm-reduction P, where S_{B}^{∗} is the subset of reductions in S_{B} that are co-initial with P (note that, since P ∈ S_{B}, P ⊴_{L}⊓_{L}S_{B}^{∗}

implies P ≈_{L} ⊓_{L}S_{B}^{∗}). To prove P ⊴_{L} ⊓_{L}S_{B}^{∗}, assume P : t = t_{0}→^{u_{0}}t_{1}→^{u_{1}} … and

⊓_{L}S_{B} : t = s_{0} → →^{U_{0}} s_{1} → →^{U_{1}} . . .. Since u_{0} is external, it must be contracted by any reduction in S_{B}, hence u_{0} ∈ U_{0} and hence u_{0}/U_{0} = ∅. Further, P/U_{0} remains external, and we can prove similarly that the first contracted redex in P/U_{0} must belong to U_{1}, and so on. This means that, P/ ⊓_{L} S_{B} = ∅, that is, P ⊴_{L} S_{B}.

Note that N ⊴_{S_{B}} Q implies ω(N) ⊴_{Ω} ω(Q), but N ⊲_{S_{B}} Q need not imply ω(N) ⊲_{Ω} ω(Q). This is because the ordering ⊴_{S_{B}} is more subtle than ⊴_{Ω} and can take into account (or observe) parts of computations that occur in the ⊥_{B}- subterms, while ω(t) = ⊥_{B} for any t not in head normal form, irrespectively of ‘how far’ is t from being a head normal form. For example, let t = Ix(Ix) and N : t→^{I}(Ix)x; then ∅ ⊲_{S_{B}} N but ω(∅) = ω(N) = ⊥_{B}. Thus ⊴_{S_{B}}, defined on reductions rather than on terms, can be seen as a refinement of the classical Böhm topology on trees [5].

Thus stability of sets of reductions is a natural generalization of stability for sets of finite results. It is also consistent with the definition of stability of sets of configurations in prime event structures with erasure in [27,28].

5 Relative Normalization in SDRSs

In this section, we will generalize the Relative Hypernormalization theorem to regular stable sets of finite or infinite reductions, in stable DRSs R. We then show how S-minimal reductions can be constructed in R.

We begin by showing that, for finite or infinite results S, S-unneeded redexes cannot create S-needed ones, and that residuals of S-unneeded redexes remain unneeded. When S is regular, this enables us to construct an S-needed variant of any S-normalizing reduction, in any SDRS.

Lemma 5.1 Let S be a set of reductions satisfying [CE] and [CS], in an SDRS (in particular, S may be regular), 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.

Proof

(1) Since v is S-unneeded, there is Q : t → → ∈ S that is external to v. Then Q/u is external to v′ by Lemma 2.5, and Q/u ∈ S by [CE], Lemma 4.5 and [CS] (indeed, Q ∈ S ∧Q⊴_{L} u+Q/u implies u+Q/u ∈ S implies Q/u ∈ S). Hence v′ is S-unneeded.

(2) Since u is S-unneeded, there is Q : t → → ∈ S that is external to u. By Lemma 2.7, Q/u is external to v, and Q/u ∈ S by [CE] and [CS] (see the proof of (1)). Thus v is S-unneeded.

Definition 5.2 Let S be a set of reductions in an SDRS R.

(1) We call P S-(un)needed if it contracts only S-(un)needed redexes. We call P S-quasi-needed if it contracts infinitely many S-needed redexes.

(2) The S-needed part of P : t → → , written [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.

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

It follows immediately from Lemma 5.1 that [P]_{S} is S-needed. Note that [P]_{S} is not defined uniquely as its (k + 1)th step depends on the particular sequentializations of multi-steps (i.e., complete developments of redex sets) in P/⌈[P]_{S}⌉^{k}, but this does not cause any difficulties.

Lemma 5.3 Let P be a finite or infinite reduction in an SDRS R, and let S be a regular stable set of reductions in R. 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}. Proof Immediate from the fact that, in the notation of Definition 5.2, u has at most one residual along P (by the regularity of S), and one of the residuals of u is contracted in P (see the diagram, where all horizontal steps are S-unneeded and all vertical ones are S-needed).

[figure: ·; ·]
[figure: ·; ·; ·]
[figure: ·; ·]
[figure: P]
[figure: [P]_{S}]

Next we show that, unless it is contracted, an S-needed redexes has at least one S-needed residual. Therefore, residuals of S-quasi-needed reductions remain so. It follows that an S-normalizable term t cannot possess an Squasi-needed reduction if at least one S-normalizing reduction starting from t is finite.

Lemma 5.4 Let S be a regular stable set of reductions in an SDRS R, and let P : t→^{u}s → →^{P′} ∈ S. Further, let u ≠ v ∈ t, and let v be S-needed. Then v has at least one S-needed residual in s. Proof Since P ∈ S and v is S-needed, v/u = V ≠ ∅. Suppose on the contrary that none of the redexes in V is S-needed. By [CS] and Lemma 5.3, [P′]_{S} ∈ S, and since [P′]_{S} is S-needed, it is external to V by Lemma 5.1.(1). Hence u + [P′]_{S} is external to v, and u + [P′]_{S} ∈ S by [CE], contradicting S-neededness of v.

Lemma 5.5 Let S be a regular stable set of reductions in an SDRS, let t_{0} have an S-quasi-needed reduction, and let t_{0}→^{u}s_{0}. Then s_{0} also has an Squasi-needed reduction. Proof By Lemma 5.3, t_{0} has an infinite S-needed reduction P : t_{0}→^{u_{0}}t_{1}→^{u_{1}} . . .. Let U_{i} = u/(u_{0} + … + u_{i−1}), i = 0, 1, … (see the diagram below). It follows from finiteness of developments that there are infinitely many numbers k such that u_{k} ∉ U_{k} (otherwise there should be a number m such that t_{m}→^{u_{m}}t_{m+1} →^{u_{m+1}} … is an infinite U_{m}-development). By Lemma 5.4, u_{k} has at least one S-needed U_{k}-residual in s_{k}, i.e. u_{k}/U_{k} contains at least one S-needed step. Hence P/u is S-quasi-needed.

[figure: t_{0}; u_{0}; t_{1}; u_{1}; t_{2}; s_{0}; u = U_{0}; u_{0}/U_{0}; s_{1}; U_{1}; u_{1}/U_{1}; s_{2}; U_{2}]

The following theorem justifies the stability concept for sets of reductions:

Theorem 5.6 Let S be a regular stable set of reductions in an SDRS R, and let t be S-normalizable.

(1) Any S-needed fair reduction starting from t is S-normalizing.

(2) If S contains a finite reduction starting from t, then t does not possess a reduction in which S-needed redexes are contracted infinitely many times.

Proof

(1) By Lemma 5.3, there is an S-needed reduction P : t → → ∈ S. Let Q be S-needed fair. By [CE], it is enough to prove that P ⊴_{S} Q, which requires proving that ⌈P ⌉^{k} ⊴_{S} Q for every finite initial part ⌈P ⌉^{k} of P. Suppose ⌈P ⌉^{k} ⊴_{S} Q, and let us prove ⌈P ⌉^{k+1} ⊴_{S} Q. Then ⌈P ⌉^{k}/⌈Q⌉^{l_{k}} is S-unneeded for some l_{k}. Let v be the (k + 1)th step of P. If v has an S-needed ⌈Q⌉^{l_{k}}/⌈P ⌉^{k}-residual v′, then by Lemma 5.1 v′ must be a residual of some S-needed redex v′′ in the final term t_{l_{k}} of Q_{l_{k}} (see the diagram), and v′′ ⊴_{S} ⌈Q⌉_{k} since Q is S-needed fair. Thus, by the Cube Lemma and Lemma 5.1, v′ ⊴_{S} ⌈Q⌉_{l_{k}}/(⌈P ⌉^{k}/⌈Q⌉^{l_{k}}), and we are done.

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

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

(2) Let P : t → → s and P ∈ S. Suppose on the contrary that there is an Squasi-needed Q starting from t. Then by Lemma 5.5 Q/P is S-quasi-needed as well – a contradiction, since P ∈ S implies that Q/P is S-unneeded.

Based on the result in section 3, we will now give a sufficient and necessary condition for superstability of regular stable sets of finite results.

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

(1) We call u ∈ t S-erased if u does not have a residual under any Snormalizing reduction.

(2) We call a reduction S-erased if it only contracts S-erased redexes.

Clearly, a reduction P is S-erased iff P ⊴_{L} Q for every Q ∈ S. Note that S-erased redexes need not be S-needed (e.g., when S is the set of normal forms and the OTRS has an erasing rule, say f(x) → a). However, any reducible normalizable term t in an orthogonal (first or higher-order) term rewriting system has an external redex [19]. And such redexes are both erased and needed w.r.t. to the regular stable sets considered in the literature.

Theorem 5.8 Let S be a regular stable set of terms, in an SDRS. Then S is superstable (i.s, satisfies [Min]) iff any S-normalizable term t ∉ S contains an S-erased S-needed redex. Proof Let S_{red} be the set of all S-normalizing reductions starting from t, and

let ⊓_{L}S_{red} : t = t_{0} → →^{U_{0}} t_{1} → →^{U_{1}} . . ..

(⇐) By the assumption and the construction of ⊓_{L}S_{red}, every multi-step of ⊓_{L}S_{red} contracts an S-needed redex. Hence ⊓_{L}S_{red} ∈ S_{red} by Theorem 5.6 and ⊓_{L}S_{red} is S-minimal by Theorem 3.2, which imply [Min].

(⇒) Since, by [Min], ⊓_{L}S_{red} is S-normalizing, it contracts a S-needed redex by [CUE]. Let i be the smallest number such that U_{i} contains an S-needed redex, say v_{i}. Suppose on the contrary that i ≠ 0. Then, by Lemma 5.1, t_{i−1} contains a S-needed redex v_{i−1} for which v_{i} is the unique residual (since by the minimality of i, all redexes in U_{i−1} are S-unneeded). But v_{i−1} is erased along ⊓_{L}S_{red} since v_{i} is, and by the S-minimality of ⊓_{L}S_{red}, v_{i−1} is S-erased. Hence we must have v_{i−1} ∈ U_{i−1} – a contradiction.

This theorem gives a more ‘local’ definition of superstability for regular stable sets of finite results. By combining this with the Relative Hypernormalization theorem, we get the following corollary:

Corollary 5.9 (Minimal Relative Normalization) Let S be a superstable set of terms in an SDRS, and let t be an S-normalizable term not in S. Then repeated contraction of S-needed S-erased redexes in t yields an S-minimal S-normalizing reduction, even if a finite number of S-unneeded S-erased, and only such, redexes are also contracted.

6 Concluding remarks

We have formalized a concept of ‘infinite results’, and proved a normalization theorem relative to such results, in an abstract framework of SDRSs. We also studied minimal relative normalization in SDRSs. These results unify and extend several earlier results on relative and discrete normalization. Furthermore, concepts of stable sets of results and corresponding orderings introduced in this paper allow SDRSs to be viewed as semi-distributive domains, or ‘domains with duplication’ [25].

References

[1] S. Abramsky and C.-H. L. Ong, Full abstraction in the lazy lambda calculus, Information and Computation 105 (1993) 159-267.

[2] S. Antoy, R. Echahed and M. Hanus, A needed narrowing strategy, in: Proc. 21st ACM Symp. on Principles of Programming Languages (1994) 268-279.

[3] S. Antoy and A. Middeldorp, A Sequential Reduction Strategy, Theoret. Comput. Sci. 165(1) (1996) 75-95.

[4] Z.M. Ariola, M. Felleisen, J. Maraist, M. Odersky, P.A. Wadler, A call-by-need lambda calculus, in: Proc. 22nd ACM Symp. on Principles of Programming Languages (1995) 233-246.

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

[6] H.P. Barendregt, J.R. Kennaway, J.W. Klop, M.R. Sleep, Needed reduction and spine strategies for the lambda calculus, Information and Computation 75(3) (1987) 191-231.

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

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

[9] G. Berry and J.-J. Lévy, Minimal and optimal computations of recursive programs, J. of the Association for Computing Machinery 26 (1979) 148-175.

[10] G. Boudol, Computational semantics of term rewriting systems. in: M. Nivat and J.C. Reynolds, eds., Algebraic methods in semantics (CUP, 1985) 169-236.

[11] A. Church and J.B. Rosser, Some properties of conversion, Transactions of American Mathematical Society 39 (1936) 472-482.

[12] H.B. Curry and R. Feys, Combinatory Logic, Vol. 1 (North-Holland, Amsterdam, 1958).

[13] P. Gardner, Discovering needed reductions using type theory, in: Proc. TACS’94, Lecture Notes in Computer Science, vol 789 (Springer, Berlin, 1994) 555-574.

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

[15] J.R.W. Glauert, J.R. Kennaway and Z. Khasidashvili, Stable results and relative normalization, Journal of Logic and Computation 10(3), Special Issue: Type Theory and Term Rewriting, F. Kamareddine and J.W. Klop, eds. Oxford University Press (2000) 323-348.

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

[17] R.J. Hindley, An abstract form of the Church-Rosser theorem I, Journal of Symbolic Logic 34(4) (1969) 545-560.

[18] G. Huet, Confluent reductions: Abstract properties and applications to term rewriting systems, J. of the Association for Computing Machinery 27(4) (1980) 797-821

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

[20] J.R. Kennaway, Sequential evaluation strategy for parallel-or and related reduction systems, Annals of Pure and Applied Logic 43 (1989) 31-56.

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

[22] J.R. Kennaway, J.W. Klop, M.R. Sleep and F.-J. de Vries, Transfinite reductions in orthogonal term rewriting systems, Information and Computation 119(1) (1995) 18-38.

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

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

[25] Z. Khasidashvili, Stable computational semantics of conflict-free rewrite systems. (Available on request.)

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

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

[28] Z. Khasidashvili and J.R.W. Glauert, Relating conflict-free stable transition and event models via redex families. Special issue dedicated to MFCS’97 conference, P. Ružička, ed. Theoretical Computer Science (to appear). Available

at http://www.cs.biu.ac.il/~khasidz.

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

[30] Lévy J.-J. An algebraic interpretation of the λβK-calculus; and an application of a labelled λ-calculus. TCS 2(1):97-114, 1976.

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

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

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

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

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

[36] P.-A. Melliès, Axiomatic rewriting theory II: The λσ-calculus enjoys finite normalization cones, Journal of Logic and Computation 10(3), Special Issue: Type Theory and Term Rewriting, F. Kamareddine and J.W. Klop, eds. Oxford University Press (2000) 461-487.

[37] A. Middeldorp, Call by need computations to root-stable form, in: Proc. 24th ACM Symp. on Principles of Programming Languages (1997) 94-105.

[38] E. Nöcker, Efficient functional programming: Compilation and programming techniques, Ph.D. Thesis, Katholic University of Nijmegen, 1994.

[39] V. van Oostrom, Confluence for abstract and higher-order rewriting, Ph.D. Thesis, Free University, Amsterdam, 1994.

[40] V. van Oostrom, Normalisation in weakly orthogonal rewriting, in: proc. RTA’99, Lecture Notes in Computer Science, vol. 1631 (Springer, Berlin, 1999) 60-74.

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

[42] R.C. Sekar and I.V. Ramakrishnan, Programming in equational logic: Beyond strong sequentiality, Information and Computation 104(1) (1993) 78-109.

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

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

[45] H. Xi, Evaluation under lambda abstraction, in: proc. PLILP’97, Lecture Notes in Computer Science, vol. 1292 (Springer, Berlin, 1997) 259-274.

[46] N. Yoshida, Optimal reduction in weak λ-calculus with shared environments, in: Proc. ACM Conference on Functional Programming Languages and Computer Architecture (1993) 243-252.