Strongly sequential and inductively sequential term rewriting systems

Michael Hanus^{∗}  Salvador Lucas^{†}  Aart Middeldorp^{‡}

Abstract

The concept of definitional tree by Antoy serves to introduce control information into the bare set of rules of a constructor-based term rewriting system (TRS). TRSs whose rules can be arranged into a definitional tree are called inductively sequential. By relying on the existence of such a definitional tree, an optimal rewriting strategy, the outermost-needed strategy is defined. Optimality was proved w.r.t. the Huet and Lévy’s theory of neededness. In this paper, we prove that strongly sequential and inductively sequential constructor-based TRSs coincide. We also show that outermost-needed rewriting only reduces strongly needed redexes.

Keywords: definitional trees, neededness, strong sequentiality, term rewriting, declarative programming.

1 Introduction

For orthogonal TRSs, the best normalizing strategy which avoid unnecessary reductions is needed rewriting [7]. Needed rewriting only considers needed redexes, i.e., redexes which are contracted (themselves or some residual) in every normalizing derivation. Unfortunately, it is undecidable whether a redex is needed. Strongly sequential redexes approximate needed redexes. However, reduction of strong redexes is costly to implement [10], and some efforts have been done to simplify the (strongly) needed reduction process.

Definitional trees [1] allow us to define optimal strategies both in rewriting [1] and narrowing [3]. A definitional tree consists of branches on the values of particular arguments and the rules of the TRS.

Example 1.1 Consider the following rules:

    first(0,x)→ []
    first(s(x),y::z) → y::first(x,z)

We give a graphic representation of the definitional tree for the function first (Figure 1). The first branch is done on the first argument (\underline{x1}) with alternative patterns 0 and s(x), where a further branch on \underline{x2} (with only one alternative) is necessary for the latter pattern.

           [figure: first(\underline{x1}, x2); first(0, x2); first(s(x), \underline{x2}); []; first(s(x), y :: z); y :: first(x, z)]

Figure 1: Definitional tree for the function first A function f, defined by rules of a TRS R is inductively sequential if there exists a definitional tree P containing all rules defining f. R is inductively sequential if all defined symbols are inductively sequential.

Recently, definitional trees and inductively sequential TRS became important for declarative programming languages since they model lazy functional languages with pattern matching and are an adequate basis to implement optimal evaluation strategies for functional logic languages [2]. Moreover, they can be easily extended to more general classes of TRSs [4].

The relevance of inductively sequential TRSs for declarative programming languages raised the question about their relationship to the classical concept of strong sequentiality. In [3], the question was raised whether the classes of strongly sequential and inductively sequential constructor-based TRSs are the same. In this paper we formally show that the two classes coincide. Furthermore, we generalize the notion of a definitional tree to deal also with non-constructor-based TRSs. This allows us to compare definitional trees to other structures used to implement strong sequentiality, like index trees and forward-branching index trees [6, 11], and the matching dags of Huet and Lévy [7].

A definitional tree determines a rewriting strategy, namely the outermost-needed strategy. We prove that this strategy is an index reduction strategy, i.e., it only selects strong indices for reduction. Since we can use the properties of strong indices in constructor-based TRSs, our proof is easier than the one in [1].

∗Informatik II, RWTH Aachen, D-52056 Aachen, Germany, hanus@informatik.rwth-aachen.de. Work partially supported by DFG (under grant Ha 2457/1-1) and Acción Integrada.

†DSIC, U.P. de Valencia, Camino de la Vera s/n, Apdo.

22012, E-46071 Valencia, Spain, slucas@dsic.upv.es. Work partially supported by EEC-HCM grant ERBCHRXCT940624, Bancaixa (Bancaja-Europa grant), Acción Integrada (HA1997-0073) and CICYT (under grant TIC 95-0433-C03-03).

‡Institute of Information Sciences and Electronics, University of Tsukuba, Tsukuba 305-8573, Japan, ami@score.is.tsukuba.ac.jp.

In Section 2, we review the technical concepts used in the remainder of the paper. In Section 3, we introduce definitional trees. Section 4 explores the relation between strongly sequential and inductively sequential TRSs. Section 5 compares to other approaches.

2 Preliminaries

This section introduces our main notations (see [5, 8] for full definitions). Given a partial order ≤ on a set A and a ∈ A, a↑= {b ∈ A | a ≤ b} is the upward set associated with a. a ∥ b means a ≰ b and b ≰ a.

V denotes a set of variables and Σ denotes a set of function symbols {f, g, …}, each with a fixed arity given by a function ar : Σ → IN. We denote the set of terms by T (Σ, V). A k-tuple t_{1}, …, t_{k} of terms is denoted by t̃, where k will be clarified by the context. The set of variables appearing in a term t is denoted by Var(t).

Terms are viewed as labeled trees in the usual way. Occurrences u, v, … are represented by chains of positive natural numbers used to address subterms of t. Occurrences are ordered by the standard prefix ordering: u ≤ v iff ∃v′ such that v = u.v′. The empty occurrence is denoted by ϵ. O(t) denotes the set of occurrences of t. The subterm at occurrence u of t is denoted by t|_{u}. The term t with the subterm at the occurrence u replaced with s is denoted by t[s]_{u}. The symbol labeling the root of t is denoted by root(t).

A rewrite rule is an ordered pair (l, r), written l → r, with l, r ∈ T (Σ, V), l ∉ V and Var(r) ⊆ Var(l). Given a rule l → r, l is called the left-hand side (lhs) of the rule and r the right-hand side (rhs). A TRS is a pair R = (Σ, R) where R is a set of rewrite rules. A left-linear TRS is a TRS where every lhs is a linear term. An orthogonal TRS is a left-linear TRS without overlapping rules, i.e., given a rule l → r, there is no non-variable occurrence u ∈ O(l) such that l|_{u} unifies with a lhs l′ of a rule l′ → r′ in the TRS (where l → r and l′ → r′ are different in case of u = ϵ).

A term t rewrites to a term s, written t →_{R} s, if t|_{u} = σ(l) and s = t[σ(r)]_{u}, for some rule l → r, u ∈ O(t) and substitution σ. O_{R}(t) = {u ∈ O(t) | ∃l → r ∈ R and σ with t|_{u} = σ(l)} is the set of redex occurrences in t.

Given a TRS, we split the signature into the disjoint union Σ = C ⊎ F of symbols c ∈ C, called constructors, having no associated rule and symbols f ∈ F, called defined functions or operations, which are defined by some rule f(l̃) → r ∈ R. Each rule f(δ̃) → r in a constructor-based TRS or constructor system (CS) must satisfy f ∈ F and δ̃ ∈ T (C, V)^{ar(f)}.

3 Definitional trees

We generalize the notion of (partial) definitional tree (pdt) by using its “declarative” definition (see [2]). To represent unknown parts of a term t we use the symbol Ω. Terms in T (Σ ∪ {Ω}, V) are called Ω-terms. To discuss about unknown portions of expressions, we use the ordering ≤ on Ω-terms given by: Ω ≤ t for all t ∈ T (Σ∪{Ω}, V), x ≤ x for all x ∈ V, and f(t̃) ≤ f(s̃) if t_{i} ≤ s_{i} for 1 ≤ i ≤ ar(f). In this way, t ≤ s means “t is less or equally defined than s”. O_{Ω}(t) = {u ∈ O(t) | t|_{u} = Ω} is the set of occurrences of Ω in t.

A definitional tree of a finite set of (incomparable) Ω-terms S ⊆ T (Σ ∪ {Ω}) with pattern π ∈ T (Σ ∪ {Ω}) is a non-empty, ordered set P of Ω-terms having the following properties:

• There is a minimum element which is the pattern of the pdt: min(P) = π (minimum property).

• The maximal elements are the elements of S: maximal(P) = S (leaves property).

• If π′ ∈ P, π′ ≠ π, there is a unique π′′ ∈ P, π′′ < π′, such that there is no π′′′ ∈ T (Σ ∪ {Ω}) with π′′ < π′′′ < π′ (parent property).

• Given π′ ∈ P\S, there is an occurrence u ∈ O_{Ω}(π′) (called the inductive occurrence), and symbols^{1} f_{1}, …, f_{n} ∈ Σ with f_{i} ≠ f_{j} for i ≠ j, such that, for all π_{1}, …, π_{n} which are immediately below π′, π_{i} = π′[f_{i}(Ω̃)]_{u} for all 1 ≤ i ≤ n (induction property).

These properties entail S ⊆ P ⊆ π ↑. Given a TRS R = (F ⊎ C, R), a redex scheme of R is a lhs of a rule l → r where all variables are replaced by Ω. Let L_{Ω}(R) be the set of redex schemes of R. Since we deal with orthogonal TRSs, we assume that a bijective function ρ : L_{Ω}(R) → R associates the rule which corresponds to each redex scheme. A preredex of a redex scheme l is an Ω-term π such that π ≤ l. Let L_{Ω}^{<}(R) = {π | ∃l ∈ L_{Ω}(R) with π < l}. For f ∈ F, let L_{Ω}^{f}(R) = {l ∈ L_{Ω}(R) | root(l) = f}. f is called inductively sequential if there exists a definitional tree P_{f} which is a pdt of L_{Ω}^{f}(R) with pattern f(Ω̃). R is called inductively sequential if all defined symbols f ∈ F are inductively sequential. An inductively sequential TRS can be viewed as a set of definitional trees, each defining a function symbol. By using a representation function pdt, we can represent a pdt P of a set S ⊆ L_{Ω}(R) with pattern π as a term pdt(P) as follows:

1In the original definition of definitional trees, only constructor symbols are allowed.

pdt(P) = rule(ρ(π)) if P = {π} = S.

pdt(P) = branch(π, u, pdt(P_{1}), …, pdt(P_{n})) if P is not a singleton, where π = min(P), u is the inductive occurrence of π, f_{1}, …, f_{n} ∈ Σ, f_{i} ≠ f_{j} if i ≠ j, and, for all i, 1 ≤ i ≤ n, P_{i} is a pdt with pattern π_{i} = π[f_{i}(Ω̃)]_{u} of the set S_{i} = S ∩ π_{i}↑.

Example 3.1 Consider the program of Example 1.1. Then (we use Ω’s instead of variables),

branch(first(Ω, Ω), 1,

     rule(first(0,y) → []),

branch(first(s(Ω),Ω), 2,

      rule(first(s(x),y::z) → y::first(x,z))))

is a definitional tree for the function first (Figure 1).

4 Strong sequentiality and inductively sequential TRSs

Regarding normalization strategies, the main result of Huet and Lévy [7, 9] is the following: reduction of needed redexes is normalizing for orthogonal TRSs. In general, the occurrences of such needed redexes are undecidable, but Huet and Lévy define a computable approximation, the (strong) indices. To obtain such an approximation, they use Ω-terms.

To calculate indices a function ω is used. It is defined by means of a reduction relation →_{Ω} [9]: C[t] →_{Ω} C[Ω] if t ≠ Ω and there exists l ∈ L_{Ω}(R) such that t ↑ l, i.e., there exists an Ω-term s such that t ≤ s and l ≤ s. The relation →_{Ω} is confluent and terminating (see [7, 9]). Let ω(t) be the →_{Ω}-normal form of t. Instead of the usual definition of index, based on the notion of sequential predicate, we use an equivalent, simpler characterization (see [7, 9]).

Definition 4.1 Let t ∈ T (Σ ∪ {Ω}, V) and u ∈ O_{Ω}(t). Let • be a fresh constant symbol, and t′ = t[•]_{u}. Then u is an index of t iff ω(t′)|_{u} = • (sometimes we write • ∈ ω(t′) for short). The set of indices of t is denoted by I(t).

Proposition 4.2 ([9]) If u.v ∈ I(t[s]_{u}), then u ∈ I(t[Ω]_{u}) and v ∈ I(s).

Proposition 4.3 ([9]) If u ∈ I(t) and t ≤ t′, then u ∈ I(t′[Ω]_{u}).

An Ω-normal form is an Ω-term t such that O_{R}(t) = ∅ and O_{Ω}(t) ≠ ∅. Strongly sequential TRSs are defined as follows.

Definition 4.4 ([8]) An orthogonal TRS is strongly sequential if every Ω-normal form has an index.

When considering CSs, things are simpler.

Proposition 4.5 ([9]) An orthogonal CS R is strongly sequential iff ∀π ∈ L_{Ω}^{<}(R)\{Ω}, I(π) ≠ ∅.

We use the following property of indices in CSs.

Proposition 4.6 ([9]) Let R be an orthogonal CS. Let u ∈ I(t) and s such that root(s) ∈ F and v ∈ I(s). Then u.v ∈ I(t[s]_{u}).

A strategy which always reduces redexes pointed by indices is called index reduction.

Theorem 4.7 ([7]) Index reduction is normalizing for orthogonal, strongly sequential TRSs.

4.1 Inductive sequentiality of strongly sequential TRSs

Let t ∈ T (Σ ∪ {Ω}). t↑^{<} is the set of terms which are greater than t: t↑^{<}= {s ∈ T (Σ ∪ {Ω}) | t < s}. Given u ∈ O(t), t ↓_{<}^{u} is the set of terms which are smaller than t and whose subterm at occurrence u is not Ω: t↓_{<}^{u}= {s ∈ T (Σ ∪ {Ω}) | s < t ∧ u ∈ O(s) ∧ s|_{u} ≠ Ω}. Given a set of terms S ⊆ L_{Ω}(R) and an occurrence u ∈ O(s) for all s ∈ S, we define the equivalence relation ≡_{u} by s ≡_{u} s′ iff root(s|_{u}) = root(s′|_{u}), i.e., the terms have the same symbol rooting the subterm at the occurrence u.

In the remainder of the paper, given Ω-terms π and l ∈ π ↑ and an occurrence u ∈ O(π), we define Π(l, π, u) = π↑^{<} ∩ l↓_{<}^{u}. The function nodes builds a pdt for a given function definition:

nodes(S, π, u) =

if S = {l} and Π(l, π, u) = ∅ then
rule(ρ(l))
else let π′ = min(∪_{l∈S}Π(l, π, u))
u′ ∈ I(π′)
{S_{1}, …, S_{n}} = S/≡_{u′}
in branch(π′, u′, nodes(S_{1}, π′, u′), …,
nodes(S_{n}, π′, u′))

Lemma 4.8 Let π ∈ T (Σ ∪ {Ω}), u ∈ O_{Ω}(π) and S ⊆ π↑, such that, ∃f ∈ Σ.∀l ∈ S, root(l|_{u}) = f and there exists l ∈ S with l↓_{<}^{u}≠ ∅. Let Π_{S} = ∪_{l∈S}Π(l, π, u). Then, min(Π_{S}) = π[f(Ω̃)]_{u}.

Proof. Let π′ = π[f(Ω̃)]_{u}. Clearly, π′ ∈ π ↑^{<} and it is minimal in π ↑^{<}. Let l ∈ S be such that l↓_{<}^{u}≠ ∅. Clearly, Π(l, π, u) ≠ ∅ because, since l ∈ π↑, l↓_{<}^{u}≠ ∅, and l|_{u} ≠ Ω, we have that π′ ∈ l↓_{<}^{u}. Therefore, π′ is minimal in Π(l, π, u). Let π′′ ∈ Π(l, π, u). Since root(l|_{u}) = f and root(π′′|_{u}) ≠ Ω, it must be that root(π′′|_{u}) = f. Thus π′ ≤ π′′. Since π′′ is arbitrary, it follows that Π(l, π, u) has a minimum element min(Π(l, π, u)) = π′. Since this holds for every l ∈ S with l↓_{<}^{u}≠ ∅ and the elements l ∈ S with l↓_{<}^{u}= ∅ do not introduce new elements in Π_{S}, we obtain min(Π_{S}) = π′. □

The height h of a finite ordered set is the number of elements n of the largest strict chain a = a_{1} < a_{2} < ⋯ < a_{n} = b going from a minimal element a to a maximal element b. We define h = 0 if the set is empty. Then, we can prove the following result.

Theorem 4.9 Let R be an orthogonal, strongly sequential TRS. Then, for all defined symbols f, nodes(L_{Ω}^{f}(R), Ω, ϵ) is a definitional tree for f.

Proof. We consider a generic call nodes(S, π, u) under the restrictions π ∈ T (Σ ∪ {Ω}), u ∈ O_{Ω}(π), and S ⊆ π↑ ∩ L_{Ω}(R) non-empty and such that ∃f ∈ Σ, ∀l ∈ S, root(l|_{u}) = f. First, we prove that nodes builds a pdt for S with pattern π[f(Ω̃)]_{u}. Given l ∈ S, let h_{l} denote the height of Π(l, π, u). We proceed by induction on the height h_{S} = max_{l∈S}(h_{l}) of Π_{S} = ∪_{l∈S}Π(l, π, u).

h_{S} = 0: Note that h_{S} = 0 implies that, for all l ∈ S, h_{l} = 0, i.e., Π(l, π, u) = ∅ for all l ∈ S. Moreover, orthogonality implies that S = {l}. Otherwise, since for all (distinct) l, l′ ∈ S, we have root(l|_{u}) = root(l′|_{u}) = f, it holds that π[f(Ω̃)]_{u} ≤ l and π[f(Ω̃)]_{u} ≤ l′. Orthogonality implies that π[f(Ω̃)]_{u} < l. This means that Π(l, π, u) ≠ ∅, a contradiction. Therefore, we are in the if part of nodes and the conclusion is immediate.

h_{S} > 0: Since h_{S} > 0 implies that there is l ∈ S with h_{l} > 0, this means that Π(l, π, u) ≠ ∅ for this l. Hence, we are in the else part of nodes. By definition of Π(l, π, u), we have l↓_{<}^{u}≠ ∅. Then, by Lemma 4.8, π′ in the algorithm is correctly defined as π′ = min(Π_{S}) = π[f(Ω̃)]_{u}. Since π′ < l and l ∈ L_{Ω}(R), by orthogonality, π′ is an Ω-normal form. By strong sequentiality, there exists u′ ∈ I(π′). Strong sequentiality ensures that, for each l ∈ S, l|_{u′} ≠ Ω, i.e., root(l|_{u′}) = g_{l} ∈ Σ. Otherwise, u′ is not an index, since π′[•]_{u′} can be refined to a redex of l, and hence • ∉ ω(π′[•]_{u′}) = Ω. Since π < π′, the height h′_{l} of Π(l, π′, u′) is less than h_{l}, for each l ∈ S. Thus, we apply the I.H.: each P_{i} = nodes(S_{i}, π′, u′), 1 ≤ i ≤ n, is a pdt for S_{i} with pattern π′′_{i} = π′[g_{i}(Ω̃)]_{u′}, where g_{i} is the common

                                                          f(\underline{Ω}, Ω)

f(g(\underline{Ω}, Ω), Ω)
f(g(h(Ω), \underline{Ω}), Ω)
f(g(h(Ω), a), Ω)

                                                                                f(\underline{Ω}, Ω)

f(g(Ω, \underline{Ω}), Ω)
f(g(\underline{Ω}, a), Ω)
f(g(h(Ω), a), Ω)

Figure 2: Two pdts for f

symbol at occurrence u′ of each l ∈ S_{i}. Thus, P = branch(π′, u′, nodes(S_{1}, π′, u′), …, nodes(S_{n}, π′, u′)) immediately satisfies the minimum and leaves property. By minimality of each π′′_{i} in P_{i}, and by the definition of P, it satisfies the parent and induction properties too.

Now we apply nodes to the arguments L_{Ω}^{f}(R), Ω, ϵ in the hypothesis and we obtain the desired result. □

The previous definition of nodes was closer to our definition of a pdt as a kind of ordered set which simplified the proofs. However, using the previous results, we can give a more readable version of the algorithm. Remember that ρ(π) associates with π ∈ L_{Ω}(R) the rule l → r such that π is a redex scheme of l.

nodes(S, π, u) =

if S = {π} then rule(ρ(π))

                                                     else let f = root(l|_{u}) for some l ∈ S

π′ = π[f(Ω̃)]_{u}
u′ ∈ I(π′)
{S_{1}, …, S_{n}} = S/≡_{u′}

in branch(π′, u′, nodes(S_{1}, π′, u′), …,

nodes(S_{n}, π′, u′))

4.2 Strong sequentiality of inductively sequential TRSs

Proposition 4.10 Let P_{f} be a pdt for the function f of a CS. Then every inductive occurrence u in a branch node branch(π, u, P̃) of P_{f} satisfies u ∈ I(π).

Proof. Let P_{f} = branch(π, u, P̃). Note that u ∈ O_{Ω}(π). By contradiction: Since we consider CSs, if u ∉ I(π), then π[•]_{u} ↑ l for some redex scheme l in maximal(∪_{P∈_{P}}P). Since π < l, this means that the pattern π′ of P, the pdt in P̃ which contains l, verifies root(π′|_{u}) = Ω, contradicting the definition of a pdt, since it must be that root(π′|_{u}) ∈ Σ. □

This result does not hold for arbitrary pdts.

Example 4.11 Consider the orthogonal TRS

f(g(h(x), a), y) → x   c → a

g(x, b) → g(h(x), a) Partial definitional trees for f are drawn in Figure 2.

The inductive occurrence 1.1 is not an index in the pattern f(g(Ω, Ω), Ω) of the first pdt. By using nodes, we obtain the second definitional tree for which every inductive occurrence is an index.

Theorem 4.12 Let R = (Σ, R) be an inductively sequential CS. Then, R is strongly sequential.

Proof. From Proposition 4.5, we prove by contradiction that every proper prefix Ω < p < l of a redex scheme l has an index. Assume I(p) = ∅. Let Ω < π_{1} < ⋯ < π_{n} < l be the chain of patterns in the branch nodes of a pdt for the function f = root(p) which contains l. It is not possible to have a π_{j}, 1 ≤ j ≤ n such that p ≤ π_{j}. Otherwise, by Proposition 4.10 and Proposition 4.2, p also has an index. Thus, π_{i} ∥ p for some i, 1 ≤ i ≤ n. Let us consider the maximal π ∈ {π_{1}, …, π_{n}} such that π ≤ p and π ≤ π_{i}. π exists, because π_{1} = f(Ω̃), and Ω < f(Ω̃) ≤ p < l. Let u be the inductive occurrence for the branch node with pattern π. By Proposition 4.10, u ∈ I(π). We have p|_{u} = Ω. Otherwise, since p < l and root(l|_{u}) = root(p|_{u}), there is π′ > π such that π′ ≤ p and π′ ≤ π_{i}, thus contradicting the maximality of π. By Proposition 4.3, u ∈ I(p). □

This theorem does not hold for general strongly sequential TRSs, as the following example shows.

Example 4.13 Consider the following TRS which is not strongly sequential (from [7]):

f(g(a, x), f(b, y)) → x   g(d, d) → d

f(g(x, a), f(c, y)) → x f and g admit definitional trees, and nodes can build them, because every redex scheme has some index.

Theorems 4.9 and 4.12 entail our main result.

Theorem 4.14 An orthogonal CS is strongly sequential iff it is inductively sequential.

4.3 Outermost-needed reduction

A definitional tree determines a rewriting strategy, namely the outermost-needed rewriting strategy^{2}:

Definition 4.15 ([1]) The (partial) function φ takes arguments t = f(t̃), f ∈ F and a pdt P such that min(P) ≤ t, and yields a redex occurrence u ∈ O_{R}(t): φ(t, P) =

ϵ  if P = rule(α)
φ(t, P_{i})  if P = branch(π, u, P_{1}, …, P_{n})

and min(P_{i}) ≤ t for some i

u.φ(t|_{u}, P_{g}) if P = branch(π, u, P_{1}, …, P_{n}), (∗)

root(t|_{u}) = g ∈ F, and

P_{g} is a definitional tree for g.

Note that, dealing with CSs, the second and third cases are disjoint. This is because if root(t|_{u}) = g ∈ F, then since π ≤ min(P_{i}) for all subpdt P_{i} of P = branch(π, u, P_{1}, …, P_{n}), it is not possible to have min(P_{i}) ≤ t since root(min(P_{i})|_{u}) ∈ C. We show that φ is equivalent to index reduction.

Theorem 4.16 Let R be an inductively sequential CS and u = φ(t, P). Then u is an index of t[Ω]_{u}.

Proof. Induction on the number of visited definitional trees. In the case base (n = 1), u is ϵ and the conclusion easily follows. Otherwise (n > 1), the occurrence u can be split up into u = v.w, where v is an occurrence of the pdt P and w has been used to reduce t|_{v} and, because R is a CS, root(t|_{v}) ∈ F, with v the inductive occurrence for some pattern in a branch node of P. By Proposition 4.10, v ∈ I(π). Since π ≤ t, by Proposition 4.3, v ∈ I(t[Ω]_{v}). Then, by I.H., w ∈ I(t|_{v}[Ω]_{w}) and the conclusion follows by Proposition 4.6. □

Theorem 4.9 suggests that definitional trees can be used with general strongly sequential TRSs. The outermost-needed strategy, as given in Definition 4.15 cannot be used to successfully evaluate a term in general (i.e., non-constructor-based) TRSs. For instance, consider the TRS in Example 4.11, t = f(g(x, b), y) and let P_{f} be a pdt for the function f if we try to compute φ(t, P_{f}). Then φ(t, P_{f}) = φ(t, P_{1}) are undefined, i.e., the strategy cannot proceed. This can be solved by changing (∗) in Definition 4.15 as follows: φ(t, P) = u′.v if P = branch(π, u, P_{1}, …, P_{n}), root(π_{j}|_{u}) ≠ root(t|_{u}) = f′ ∈ F, for all j, 1 ≤ j ≤ n; π′ = π[f′(Ω̃)]_{u}, and u′ ∈ O(π′), ϵ < u′ ≤ u is the minimal occurrence such that π′|_{u′} is compatible with some redex scheme, P_{g} is a definitional tree for g = root(π′|_{u′}), and φ(t|_{u′}, P_{g}) = v.

This works well when considering CSs (it is equivalent to Definition 4.15). However, this does not ensure that φ is index reduction when considering general TRSs. This can be clarified by comparing the strategy with the standard Huet and Lévy procedure, as discussed in the following section.

2This is a slightly different definition because we do not allow for exempt nodes as in [1]. However, it is equivalent.

5 Definitional trees and matching dags

To implement normalizing strategies without lookahead, the matching dags (directed acyclic graphs) of Huet and Lévy can be used with any strongly sequential TRS. Simpler structures are the index trees of Strandh [11] which have been proved equivalent to matching dags by Durand [6]. An index tree is a finite state automaton which has, in addition to the usual transfer function, also a failure function. The set of final states is L_{Ω}(R). Non-final states are index points, pairs ⟨π, u⟩, where π ∈ L_{Ω}^{<}(R), and u is an index of π and both satisfy some special conditions (see [6]). The initial state is ⟨Ω, ϵ⟩. The transfer function, written δ(s, f), yields a new state of the automaton, given a state s and a function symbol f: δ(⟨π, u⟩, f) = ⟨π[f(Ω̃)]_{u}, v⟩ (or just δ(⟨π, u⟩, f) = π[f(Ω̃)]_{u} if π[f(Ω̃)]_{u} ∈ L_{Ω}(R)). The failure function, ϕ, is ϕ(s) = s′ iff s′ is an immediate failure point of s. Failure points are states of the automaton which are expected to deal with a failing partial matching, by resuming the matching of a subterm of the currently inspected term. In the most general definition of an index tree, some states may not be reachable from the initial state ⟨Ω, ϵ⟩ via transfer transitions (using δ) only. Thus, only the failure function can provide access to these nodes of the tree. Orthogonal TRSs which can be given such an index tree are called bounded TRSs. Durand proves that the class of bounded TRSs and strongly sequential TRSs coincide. The proof is given by showing that there is an immediate correspondence between the matching dag of Huet and Lévy and the index trees of Strandh.

Strandh defines the forward-branching index trees, for which all states of the index tree can be reached via the transfer function δ from the initial state.

We provide a simple connection between index trees and definitional trees: transitions δ(⟨π, u⟩, f_{1}) = ⟨π[f_{1}(Ω̃)]_{u}, v_{1}⟩, …, δ(⟨π, u⟩, f_{n}) = ⟨π[f_{n}(Ω̃)]_{u}, v_{n}⟩ can be written as branch(π, u, P_{1}, …, P_{n}), where the pattern of each P_{i} is π_{i} = π[f_{i}(Ω̃)]_{u}. Each initial transition δ(⟨Ω, ϵ⟩, f) = ⟨f(Ω̃), u⟩ can be seen as the starting point of the pdt for the function f. When considering forward-branching index trees, the correspondence is even closer. However, pdts are not equivalent to the previous structures. For instance, consider the bounded TRS (from [6])

f(g(x, a), a) → a   g(b, b) → a

f(g(a, x), b) → a and the pdts in Figure 3.

The patterns and inductive occurrences of these pdts are taken by following the index tree for the TRS, as

[figure: f(Ω, \underline{Ω}); f(\underline{Ω}, a); f(\underline{Ω}, b); f(g(Ω, \underline{Ω}), a); f(g(\underline{Ω}, Ω), b); f(g(Ω, a), a); f(g(a, Ω), b)]

                                                                                g(\underline{Ω}, Ω)
                                                                                g(b, \underline{Ω})
                                                                                g(b, b)

                                                                                g(Ω, \underline{Ω})
                                                                                g(\underline{Ω}, b)
                                                                                g(b, b)

Figure 3: pdts for f and g

given in [6]. Of course, if we do not do this, we cannot ensure that the composition of the occurrences considered for the partial matchings (which are indices of the corresponding preredexes) is an index. This means that, even if we use nodes, that always selects (arbitrary) indices for inductive occurrences, we cannot ensure index reduction. But we have more involved situations. For instance, if we reduce t = f(g(Δ1, Δ2), a), where Δ1, Δ2 are redexes, it is not difficult to see that φ (modified) reduces the redex Δ1 which is not a needed redex. This is because, when we fail in matching f(g(Ω, \underline{a}), a) (we underline the last considered occurrence, 1.2) against our term, we try to reduce g(Δ1, Δ2) and we must jump to a pdt for g, in order to continue the matching. If we have the first pdt (recall that, in our strategy, only one pdt is available), then we choose to reduce Δ1. However, Δ1 is not needed in the whole context, since f(g(•, Ω), a) →Ω Ω. With an index tree, the failure function selects the other pdt for g, which properly continues the matching tasks by looking at the occurrence 2 of g(Δ1, Δ2). This is consistent with the situation before the jump.

The modification of φ would work if we consider forward branching TRSs (because they do not have such additional nodes) and we use pdts having the same pattern and inductive occurrences as the corresponding forward-branching index tree. The previous TRS is not forward-branching. However, even with such modifications, we loose efficiency, because, having a very simple definition of the failure function (we always jump to the root node of a new pdt), we would read more than once some symbols. Therefore, it seems that there is no advantage in using pdts with general TRSs.

References

[1] S. Antoy. Definitional Trees. In Proc. of ALP’92, LNCS 632:143-157, Springer-Verlag, 1992.

[2] S. Antoy. Needed Narrowing in Prolog (Extended Abstract). In Proc. of PLILP’96, LNCS 1140:473-474, Springer-Verlag, 1996.

[3] S. Antoy, R. Echahed and M. Hanus. A needed narrowing strategy. In Proc of POPL’94, pages 268-279. ACM Press, 1994.

[4] S. Antoy, R. Echahed, and M. Hanus. Parallel evaluation strategies for functional logic languages. In Proc. of ICLP’97, pages 138–152. The MIT Press, 1997.

[5] N. Dershowitz and J.P. Jouannaud. Rewrite Systems. In Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 243-320. Elsevier and The MIT Press, 1990.

[6] I. Durand. Bounded, Strongly Sequential and Forward Branching Term Rewriting Systems. Journal of Symbolic Computation, 18:319-352, 1994.

[7] G. Huet and J.J. Lévy. Computations in orthogonal term rewriting systems, I and II. In Computational logic: essays in honour of J. Alan Robinson, pages 396–443. The MIT Press, 1991.

[8] J.W. Klop. Term Rewriting Systems. In Handbook of Logic in Computer Science, volume 2, pages 1-116. Oxford University Press, 1992.

[9] J.W. Klop and A. Middeldorp. Sequentiality in Orthogonal Term Rewriting Systems. Journal of Symbolic Computation 12:161-195, 1991.

[10] M.J. O’Donnell. Equational Logic as a Programming Language. The MIT Press, 1985.

[11] R. Strandh. Classes of Equational Programs that Compile into Efficient Machine Code. In Proc. of RTA’89, LNCS 355:449-461, Springer-Verlag, 1989.