Relative Normalization in Deterministic Residual Structures

John Glauert and Zurab Khasidashvili School of Information Systems University of East Anglia Norwich NR4 7TJ England jrwg@sys.uea.ac.uk, zurab@sys.uea.ac.uk ^{∗}

Abstract This paper generalizes the Huet&Lévy theory of normalization by neededness to an abstract setting. We define Stable Deterministic Residual Structures (SDRS) and Family Structures by axiomatizing some properties of the residual relation and the family relation on redexes in an Abstract Rewriting System. We present two proofs of the Relative Normalization Theorem, one for SDRSs for regular stable sets, and another for DRSs for all stable sets of desirable ‘normal forms’. We further prove the Relative Optimality Theorem for Family Structures. {Zurab:We extend this results to deterministic Computation Structures which are deterministic Event Structures with an extra relation expressing self-inessentiality.}

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. It is well known that the leftmost-outermost strategy is normalizing in the λ-calculus [CuFe58].

For Orthogonal Term Rewriting Systems (OTRSs), a general normalizing strategy, called the needed strategy, was found by Huet and Lévy in [HuLé91]. The needed strategy always contracts a needed redex – a redex whose residual is to be contracted in any reduction to normal form. Huet and Lévy showed that any term t not in normal form has a needed redex, and that repeated contraction of needed redexes in t leads to its normal form whenever there is one.

Barendregt et al. [BKKS87] generalized the {Zurab:concept of neededness to the λ-calculus, and studied neededness also w.r.t. head-normal forms, proving correctness of the two needed strategies for computing normal forms and head-normal forms, respectively.} In [Mar92], Maranget studied a strategy that computes a weak head-normal form of a term in an OTRS. Normalization w.r.t. another interesting set of ‘normal forms’, that of constructor head-normal forms in constructor OTRSs, is studied by Nöcker [Nök94].

In [GlKh94], the present authors address the question of normalization relative to a desired set of final terms, considering the properties that a set 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 (OERS) [Kha92], a form of higher-order rewriting which subsumes Term Rewriting and the λ-calculus. They introduce the notion of neededness w.r.t. a set of reductions Π or a set of terms S. Natural conditions are imposed on S, called stability, that are necessary and sufficient for the following Relative Normalization theorem to hold: each S-normalizable term not in S (not in S-normal form) has at least one S-needed redex, and repeated contraction of S-needed redexes in a term t will lead to an S-normal form of t whenever there is one.

∗This work was supported by the Engineering and Physical Sciences Research Council of Great Britain under grant GR/H41300

Each existing notion of neededness can be given by specifying Π or S. For example, Huet&Lévyneededness is neededness w.r.t. the set of normal forms, Maranget-neededness [Mar92] is neededness w.r.t. all fair reductions, head-neededness is neededness w.r.t. the set of head-normal forms, etc. 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.

In this paper, we further generalize the Huet&Lévy theory, by abstracting from the structure of terms. We study relative normalization in Deterministic Residual Structures (DRSs). DRSs are Abstract Reduction Systems (ARSs), which consist of a set of objects t, s, …, often called terms, and labelled transitions t→^{u}s between objects, where u is a label. Each transition is uniquely labelled. If t→^{u}s and t′→^{u}s′, then t = t′ and s = s′. Transitions between the same source and target terms may have different labels. When t→^{u}s, u is said to be a redex of t, reduction of which gives s. A reduction is a sequence of transitions.

A DRS is an ARS which has a residual relation between redexes in the source and target terms of each transition. Redexes of t may be erased by reduction of u, new redexes may be introduced in s, while other redexes of s are considered residuals of redexes in t, as specified by the residual relation. Further, the residual relation is generalized to all reductions, and permutationequivalence on reductions, referred to below as Lévy-equivalence, and the embedding relation, which induces a partial ordering on the reduction space, is introduced, as is done for the λ-calculus in [Lév78, Lév80]. Sufficient conditions needed to define the above concepts in an abstract setting were stated in Stark [Sta89] and Gonthier et al. [GLM92].

{Zurab: In [Sta89], Stark defines Concurrent Transition Systems (CTSs) and uses them to develop a dataflow-like model of concurrent computation, studying ways of building machine networks with machines as basic objects. On the other hand, Gonthier et al. [GLM92] were interested in studying more syntactic properties, such as standardization, of orthogonal rewrite systems in an abstract setting. The way standardization is understood in that paper requires a nesting relation on redexes in a term, and some axioms giving its important properties. Standard reductions then become some kind of outside-in reductions. However, the [GLM92] axioms are rather restrictive, since say orthogonal DAGs [Mar91, Mar92, KKSV93] do not satisfy them.^{1}

Our DRSs are more refined than CTSs, since in the latter the residual relation is non-duplicating. We do not impose a nesting relation on redexes, but are still able to prove the Relative Normalization theorem for all regular stable sets S. (We actually prove Relative Hypernormalization Theorem.) This theorem is applicable also to determinate CTSs, to ARSs of [GLM92], and to Winskel’s deterministic Event Structures [Win80]. We only use some form of Berry’s stability axiom [Ber79] which is weaker than both the one in [Win80] and one in [GLM92].} We show that without the latter axiom the Relative Normalization theorem fails. The method employed to prove the Relative Normalization theorem is similar to that in [Kha88], and is based on the fact that S-needed steps can be pushed before S-unneeded steps, in any reduction, without affecting the number of S-needed steps. The important difference is that in [Kha88] we made heavy use of the notion of descendant of subterms – a refinement of the residual notion for redexes – both in the proofs and in the definition of an alternative notion of neededness – essentiality.

1Counterexamples to axioms 2 and 3 of [GLM92] were pointed out by R. Kennaway.

Since for irregular stable S, S-unneeded redexes can duplicate S-needed ones, the above proof method does not work; for the same reason, the S-needed strategy is not hypernormalizing any more. Therefore, to prove Relative Normalization for irregular stable S, we define the Family Structure (FS) as a DRS with a very liberal notion of family relation [Lév78, Lév80] and a contribution relation on families, expressing the notion of (at least one member of) a family to be needed to create another family. For FSs, the proof of the Relative Normalization theorem for all stable S from [GlKh94] works perfectly.

We show that FSs are stable DRSs, so the previous Relative Normalization theorem (for stable DRSs w.r.t. regular stable sets) is subsumed by this one; however the previous Relative Normalization theorem is also useful since checking for Berry’s stability is much simpler than constructing a sound family relation. For example, the λ-calculus [Lév78, Lév80], orthogonal TRSs [Mar92], Interaction Systems [AsLa93], and orthogonal CRSs (and ERSs) [Klo80, KeSl89] form FSs, hence stable DRSs. For other higher-order rewriting systems, such as HRSs [Nip93] and HORSs [Oos94, OR94], which do form stable DRSs, to our knowledge, it is not yet known if they form FSs too (though it is very likely that the latter is the case).

For FSs we show that a strategy that only contracts, in an arbitrary order, redexes that belong to S-needed families but which need not be S-needed themselves, is still S-normalizing. As a corollary, any S-needed complete family-reduction, which contracts all members of a family containing an Sneeded redex in a multi-step, is S-normalizing. Similarly to [Lév80], we show that the latter reductions are optimal in the sense that they reach S in the least number of family-reduction steps.

{Zurab:Using the family axioms, we give an Event Structure (ES) semantics to DRSs, by considering redex-families as events. We define Computation Structures as stable deterministic ESs with an extra relation ⊳ to express the fact that an event is inessential for a set of events, a configuration. This enables us to define Lévy-equivalence on the ES. For CSs, the theory of relative normalization can be applied.}

The paper is organized as follows. In the next section, we introduce stable DRSs and give some examples. In Section 3, we prove the Relative Normalization theorem for regular stable sets S in an SDRS R, and demonstrate that if S or R is not stable, then the theorem fails. In Section 4, we introduce Family Structures, show that they are stable DRSs, and prove the Relative Normalization theorem for all stable S. In Section 5, we strengthen the latter result, and prove the Relative Optimality theorem for any FS. {Zurab:Finally, in Section 6, we extend the obtained results to Event Structures.} Conclusions appear in Section 7.

2 Deterministic Residual Structures

In this section we define Deterministic Residual Structures (DRSs) which are Abstract Reduction Systems (ARSs) satisfying certain properties concerning residuals. The definition and some results about ARSs can be found e.g., in [Klo92]. Our definition is slightly different. An ARS is a twosorted set of objects: the set Ter of terms (ranged over by t, s, o, e) and the set Red of redexes (ranged over by u, v, w), with a partial function →: T er × Red → T er such that for any t ∈ T er there are only a finite number of u ∈ Red such that → (t, u) = s, (written t→^{u}s). A reduction is a sequence t→^{u_{1}}t_{2}→^{u_{2}} . . .. Reductions are denoted by P, Q, N. We write P : t → → s or t → →^{P} s if P denotes a reduction (sequence) from t to s. ∅_{t} denotes the empty reduction starting from t. P u denotes a redex u in the final term ft(P) of P. |P | denotes the length of P. u also denotes the reduction that contracts u. We use U, V, W to denote sets of redex-occurrences in a term.

DRSs are very similar to Stark’s Determinate Concurrent Transition Systems [Sta89], to Abstract Reduction Systems of [GLM92], and to van Oostrom’s Descendant Rewriting Systems [Oos94]. The main difference from DCTSs is that Stark considers a non-duplicating residual relation. The difference from ARSs of [GLM92] is that we do not have the nesting relation on redexes and the corresponding axioms (but we still have a restricted tool to express the notion of one redex controlling another), and the stability axiom is modified accordingly. The difference from van Oostrom’s DRSs is that in the latter the notion of descendant of any subterm/position of a term is formalized, not only the notion of residual of redexes.

Definition 2.1 (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, such that if t→^{u}s ∈ R and v ⊆ t, then 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. The set of residuals of a redex under any reduction is defined by transitivity. 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.

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

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

{Zurab: We assume that, in a DRS R, the residual relation on redexes is extended to all co-initial reductions as follows: (P_{1} + P_{2})/Q = P_{1}/Q + P_{2}/(Q/P_{1}) and P/(Q_{1} + Q_{2}) = (P/Q_{1})/Q_{2}, and that Lévy-equivalence or permutation-equivalence is defined as the smallest relation on co-initial reductions satisfying: U ⊔ V ≈_{L} V ⊔ U and Q ≈_{L} Q′ ⇒ P + Q + N ≈_{L} P + Q′ + N, where U and V are complete developments of redex sets in the same term. Further, one defines P ⊔ Q = P + Q/P, P ⊴ Q iff P/Q = ∅, and can show that P ≈_{L} Q iff P ⊴ Q and Q ⊴ P; and P ⊴ Q iff Q ≈_{L} P + N for some N. Below we also use the fact that Lévy-equivalent reductions are Hindley-equivalent, i.e., if P ≈_{L} Q, then for any redex u in the initial term of P, u/P = u/Q. This is all standard, and we refer to [HuLé91, Lév78, Lév80, Sta89] for details. The above relations can equivalently be defined also using Klop’s method of commutative diagrams. We will often use Klop’s diagrams in definitions and proofs. The method is well described in [Klo80, Bar84]. }

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

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

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

It is easy to verify that the λ-calculus [Lév78], orthogonal TRSs [HuLé91], orthogonal Higher-Order Rewriting Systems (HORSs) [OR94, Oos94], and hence other orthogonal higher-order rewrite systems as well (such as CRSs [Klo80], ERSs [Kha92], and HRSs [Nip93]), and Orthogonal Term Graph Rewriting Systems (OTGRSs) [KKSV93] form DRSs; OTGRSs are equivalent to Maranget’s orthogonal DAG (Directed Acyclic Graphs) rewriting systems, defined via labelled orthogonal TRSs. {Zurab:All these are stable, and can be shown so without using any notion of labelling.}

3 The Relative Normalization Theorem for regular stable sets

In this section, we recall the notion of stability and regularity for sets of terms in a DRS, and relative notions of neededness as defined in [GlKh94]. We prove that, for any regular stable S in a stable DRS R, an S-normal form of an S-normalizable term can be found by contracting S-needed redexes in it, even if every S-needed step is preceded by a finite number of S-unneeded steps. We show that without the assumption of stability for R, this result breaks down. Further, examples from [GlKh94] show that the stability of S is necessary for the Relative (Hyper)normalization theorem to hold. This shows that the stability of S for a Berry–stable R provides a unique notion of stability for the computation system (R, S). Note that S in our DRSs plays the role of the set of final states for a Transition System.

Definition 3.1 ([GlKh94]) We call a redex u ⊆ t S-needed, written NE_{S}(u, t), if at least one residual of it is contracted in any reduction from t to a term in S, and