Termination of order-sorted rewriting

Peter C. Ølveczky Department of Informatics University of Oslo E-mail: peterol@ifi.uio.no

Abstract

We present a method for proving termination of order-sorted rewrite systems by transforming an order-sorted rewrite system into an unsorted one such that termination of the latter implies termination of the ordersorted system. The method is inspired by ideas of Gnaedig and Ganzinger and contains as special cases the method presented in [Gn92a] and the method that simply ignores sort information.

1 Introduction

Order-sorted specifications, i. e. many-sorted specifications where the set of sorts is partially ordered, has been introduced to provide for a more powerful type concept, allowing us to express partiality of functions, error handling and subtype inheritance [GM88]. In languages like OBJ3 [GW88], order-sorted specifications have an operational semantics based on rewriting.

One of the most important properties a rewrite system may have is termination, which means that no infinite computation can take place. Termination is especially important in completion procedures, and last but not least, proving termination of order-sorted rewrite systems ensures termination of programs written in languages like OBJ3.

In general it is undecidable whether a rewrite system terminates, but numerous techniques (e. g. based on the lexicographic path ordering [KL80, Der87]), have been developed that with varying degrees of success may be used to prove termination of unsorted rewrite systems. These techniques have been used to prove termination of order-sorted systems by simply ignoring sort information [CH93, Gan91, GKK90, Gn92b, Wal92]. However, this approach is not good enough since many order-sorted systems terminate where the corresponding unsorted system would not terminate. This is illustrated by the following example, taken from [Gn92a] where the problem of order-sorted termination was first addressed.

Example 1 This system defines a predicate is even over the integers. The idea is to define it over the positive numbers first and to extend it to the negative numbers by using the operation opp.

sorts: Zero, NzNeg, Neg, NzP os, P os, Int, Bool Zero ≤ Neg ≤ Int Zero ≤ P os ≤ Int NzNeg ≤ Neg NzP os ≤ P os

funcs: 0 : Zero s : P os→NzP os p : Neg→NzNeg true : Bool false : Bool is even : Int→Bool opp : NzNeg→NzP os

rules: is even(0)⟶true is even(s(0))⟶false (∀x:P os) is even(s(s(x)))⟶is even(x) (∀y:NzNeg) is even(y)⟶is even(opp(y)) opp(p(0))⟶s(0) (∀y : NzNeg) opp(p(y))⟶s(opp(y))

The system is terminating, the normal form of any ground term is even(t) being either true or false. But if sorts were ignored, the system would not terminate since the fourth rule would generate the infinite rewrite sequence

is even(y)⟶is even(opp(y))is even(opp(opp(y)))⟶ ⋯

However, the system does terminate because opp(y : NzNeg) is of sort NzP os, so y cannot be instantiated with opp(t) for any term t.

In Ganzinger [Gan91], where an order-sorted rewrite system is transformed into a many-sorted equational rewrite system, each function declaration f : w→s induces a (many-sorted) function symbol f_{w→s}. This idea was adopted by Gnaedig [Gn92a] where these labelled function symbols are used to prove termination of order-sorted rewrite systems where the signature is minimal, i. e. if f : w→s and f : w′→s′ are two function declarations then w and w′ must be incomparable with respect to ≤. Termination can then be proven if l′ ≻_{lpo} r′ for every rule l⟶r, t′ being t where each function symbol f is replaced with the “corresponding” symbol f_{w→s}. Unfortunately, not many signatures are minimal, and even for those that are minimal, this approach is not very strong (e. g. this method cannot show termination of the above system even though the signature is minimal).

We will also pursue the idea of labelling each function symbol in a term, but for our purpose the best result is obtained when a function symbol is labelled with the smallest sorts of its arguments. In the previous example the fourth rule would be labelled

is even_{NzNeg}(y)⟶is even_{NzP os}(opp_{NzNeg}(y))

The symbols is even_{NzNeg} and is even_{NzP os} may then be treated as distinct symbols in e. g. the lexicographic path ordering making the inequality

is even_{NzNeg}(y) ≻_{lpo} is even_{NzP os}(opp_{NzNeg}(y))

valid with precedence is even_{NzNeg} ≻_{F} is even_{NzP os} and is even_{NzNeg} ≻_{F} opp_{NzNeg}.

We will use such labelling to transform an order-sorted rewrite system R into an unsorted rewrite system R′ such that R terminates whenever R′ does. We can thus use unsorted termination orderings to prove that R′, and hence R terminates. However, special features of termination orderings imply that the best result after applying such an ordering is not guaranteed when the transformation R′ is the most accurate. We will keep this in mind and will therefore exemplify our method with the lexicographic path ordering.

This paper is an extended abstract of [Ølv94] where a more thorough investigation on the subject of order-sorted termination as well as the correctness proofs for claims in this paper can be found.

2 Basic notions

2.1 Order-sorted rewriting

We will only introduce the syntactic aspects of order-sorted algebra and refer to [GM88] and [Wal92] for semantics of order-sorted specifications. In this paper, notions and notations mainly follow [GM88] and [GKK90].

Order-sorted algebra is based on a subsort relation, a partial order ≤ on a set S of sorts. We write s′ < s when s′ ≤ s and s′ ≠ s and ≥ for the symmetric relation of ≤. The subsort relation ≤ can be extended to n-tuples of sorts (often denoted w) where w = ⟨s_{1}, …, s_{n}⟩ ≤ ⟨s′_{1}, …, s′_{1}⟩ = w′ iff s_{i} ≤ s′_{i} for i = 1..n and w < w′ iff w ≤ w′ and w ≠ w′. We write w ⋖ w′ when w < w′ and w and w′ only differs in ith position, i. e. w = ⟨s_{1}, …, s_{i−1}, s_{i}, s_{i+1}, …, s_{n}⟩, w′ = ⟨s_{1}, …, s_{i−1}, s′_{i}, s_{i+1}, …, s_{n}⟩ and s_{i} < s′_{i}.

A function declaration has the form f : s_{1}, …, s_{n}→s where each s_{i} is a sort symbol. If n = 0 then f is called a constant and the declaration is written f : s.

An order-sorted signature ⟨S, ≤, Σ⟩, usually denoted just Σ, consists of a partially ordered sort set ⟨S, ≤ ⟩ and a set Σ of function declarations. In this paper, all signatures are assumed to be finite, i. e. to contain a finite number of sorts and declarations.

In the rest of this paper we assume that ⟨S, ≤, Σ⟩ is an order-sorted signature. Given a set X = {X_{s} | s ∈ S} of disjoint sets, the set of terms of sort s, denoted T (Σ, X)_{s}, is the least set such that X_{s′} ⊆ T (Σ, X)_{s} if s′ ≤ s, and f(s_{1}, …, s_{n}) ∈ T (Σ, X)_{s} if there exists a declaration f : s_{1}, …, s_{n}→s′ such that t_{i} is a term of sort s_{i} for i = 1..n and s′ ≤ s. The set T (Σ, X) is defined as T (Σ, X) = {T (Σ, X)_{s} | s ∈ S} and an element of any set T (Σ, X)_{s} is called a (well-formed) term. Given a set X of variables that contains an infinite number of variables of each sort, we will assume that every term t in T (Σ, X) has a unique (and computable) least sort, denoted LS(t). A ground term is a term that does not contain any variables, and we will assume that there exists a ground term of every sort s in the signature.

A term may be viewed as an ordered tree in the obvious way. A position in a term can be seen as a finite sequence of natural numbers, identifying a path from the root of the term. The node in the term where the path ends is the actual position. The subterm of t at position p, written t|_{p}, is the subterm of t which has its root symbol at position p. The result of replacing the subterm of t at position p by the term u is written t[u]_{p}. If p and q are positions we write p.q to denote the concatenation of p and q.

A substitution σ = {σ_{s} : X_{s}→T (Σ, Y)_{s} | s ∈ S} is a mapping from variables to terms. We shall use lowercase Greek letters to denote substitutions. The application of a substitution σ to a term t consists of simultaneously replacing the variables occurring in t by a term according to the mapping. The result of this application is written tσ.

A specialization, often written μ, is a substitution μ : X→Y that maps a variable x of sort s to a variable x of sort s′ less than or equal to s, i. e. (x:s)μ = x: s′ where s′ ≤ s. In a finite signature, a finite set of variables has a finite set of specializations.

An order-sorted rewrite rule is a directed equation (∀X) l⟶r where l and r are terms in T (Σ, X). A major difference between unsorted and order-sorted rewriting lies in the fact that a term t cannot always be rewritten if the lefthand-side of a rule matches a subterm of t. The reason for this is either that rewriting could result in a non-well-formed term or because of the definition of congruence in order-sorted algebras where f(a) ≈ f(b) may not be valid even though a ≈ b and both f(a) and f(b) are well-formed terms. Therefore, given a rewrite system, i. e. a set of rewrite rules, R, a term t ∈ T (Σ, X) rewrites to t′ with a rule (∀Y) l⟶r in R at position p, denoted t⟶_{R} t′ if 1. there is a substitution σ : Y →T (Σ, X) such that lσ = t|_{p} and t′ = t[rσ]_{p}

and

2. there is a sort s such that, for x a variable of sort s, t[x]_{p} is a well-formed term and lσ, rσ ∈ T (Σ, X)_{s}.

We write t ⟶ \begin{matrix}+ \\ R \end{matrix} t′ when t rewrites to t′ in one or more steps. We will assume that every rule l⟶r is sort-decreasing, i. e. LS(lσ) ≥ LS(rσ) for every substitution σ. Sort-decreasingness ensures 1) that condition 2 in the above definition of rewriting is satisfied when the first condition is fulfilled, 2) that the critical pair lemma is valid and 3) that Birkhoff’s theorem is valid for confluent systems [GKK90]. Sort-decreasingness may however be too restrictive for many purposes; we will therefore indicate how the method presented can be extended to handle non-sort-decreasing systems as well.

A rewrite system R is terminating if there does not exist any infinite rewrite sequence

t_{1}⟶_{R} t_{2}⟶_{R} t_{3}⟶_{R} ⋯

2.2 Termination of unsorted rewriting

Unsorted rewriting is the special case of order-sorted rewriting where the signature has only one sort. Since an (unsorted) rewrite system can model a Turing machine, termination of rewriting is in general undecidable (see for instance [Der87]). Many techniques, mostly so-called reduction or termination orderings, have been developed that sometimes may be used to prove termination of unsorted rewrite systems.

A quasi-ordering ≿ on a set S is a reflexive and transitive relation on S. The symmetric relation to ≿ is denoted ≾. The strict part ≻ of ≿ and the induced equivalence relation ≈ are defined ≻ = (≿ \ ≾) and ≈ = (≿ ∩ ≾) respectively.

We will use the lexicographic path ordering to exemplify our method. Assume that F is a set of function symbols and X is a set of variables. Let ≿_{F} be a quasi-ordering on F ∪ X such that a variable (seen as a constant in the ordering) is incomparable in ≻_{F} with any other symbol. The lexicographic ordering ≻_{lpo} on the set of T (F, X) of terms is then defined as follows:

t = f(t_{1}, …, t_{m}) ≻_{lpo} g(t′_{1}, …, t′_{n}) = t′

iff

either  t_{i} ≻_{lpo} t′ or t_{i} ≈_{lpo} t′
or  f ≻_{F} g and t ≻_{lpo} t′_{i} for all i ∈ 1..n
or  f ≈_{F} g and ⟨t_{1}, …, t_{m}⟩≻_{lpo}^{lex}⟨t′_{1}, …, t′_{n}⟩

and t ≻_{lpo} t′_{i} for i ≥ 2 where t≈_{lpo}t′ if t and t′ are equal up to replacement of ≈_{F} -equal symbols.

A finite rewrite system R is terminating if l ≻_{lpo} r for each rule l⟶r in R.

The reader is referred to [Der87] for an introduction to unsorted termination.

3 Termination of order-sorted rewriting

In this section we propose a technique for proving termination of an order-sorted rewrite system R by transforming it into an unsorted system R′.

Definition 1 Let Σ be an order-sorted signature. Its translation into a corresponding unsorted signature (i. e. a set of function symbols) F is defined

F = {f_{w} | f : w′→s declaration in Σ for any s and w ≤ w′}

A term t in T (Σ, X) is represented in T (F, X) by the term ⌊t⌋ where each function symbol in t is labelled with the least sorts of its arguments:

Definition 2 The mapping ⌊ ⌋ : T (Σ, X)→T (F, X) where F is the translation of Σ is defined inductively as follows:

• ⌊x : s⌋ = x for a variable x ∈ X_{s}.

• ⌊f(t_{1}, …, t_{n})⌋ = f_{LS(t_{1}),...,LS(t_{n})}(⌊t_{1}⌋, …, ⌊t_{n}⌋)

We will use ⌊ ⌋ to make a reflection of an order-sorted rewrite system R:

Definition 3 An unsorted rewrite system R′ reflects an order-sorted rewrite system R iff

t⟶_{R} t′ ⟹ ⌊t⌋⟶ \begin{matrix}+ \\ R′ \end{matrix} ⌊t′⌋

for all terms t, t′ ∈ T (Σ, X).

Clearly, R terminates whenever its reflection does.

Let us now define R′. Letting R′ = {⌊l⌋⟶⌊r⌋ | l⟶r ∈ R} is not sufficient, R′ must at least contain a rule ⌊lμ⌋⟶⌊rμ⌋ for every specialization μ of each rule l⟶r in R. Unfortunately, the following example shows that not even this definition is sufficient to make R′ a reflection of an order-sorted system R.

Example 2 Let a rewrite system R be given

sorts: s, s_{1}, s_{2}
s_{1} ≤ s
s_{2} ≤ s
funcs: f : s→s
g : s→s
g : s_{1}→s_{2}
a : s
b : s_{1}
rule: a⟶b

The term f(g(a)) rewrites to f(g(b)) in R but ⌊f(g(a))⌋ = f_{s}(g_{s}(a)) and

⌊f(g(b))⌋ = f_{s_{2}}(g_{s_{1}}(b)) so we need

f_{s}(g_{s}(a))⟶ \begin{matrix}+ \\ R′ \end{matrix} f_{s_{2}}(g_{s_{1}}(b))

which is not true if R′ only contains the rule a⟶b.

In the above example all the (unsorted) function symbols have changed even though the order-sorted rewriting occurred at position 1.1. We call such a “side effect” of a rewrite step a function symbol jump or just a F-jump:

Definition 4 Assume that a term t is rewritten to t′ in an order-sorted rewrite system and that the rule is applied at position p in t. There is a function symbol jump, often just called an F -jump, from f_{w} to f_{w′} if there is a position q in t such that ⌊t⌋|_{q} = f_{w}(…) and ⌊t′⌋|_{q} = f_{w′}(…) and there is no position r such that q = p.r

In the previous example we had two F -jumps, from f_{s} to f_{s_{2}} and from g_{s} to g_{s_{1}} respectively. Sort-decreasingness and monotonicity properties of order-sorted signatures imply that w′ ⋖ w when an F -jump from f_{w} to f_{w′} occurs. To handle this, a so-called extra rule

f_{w}(x_{1}, …, x_{n})⟶f_{w′}(x_{1}, …, x_{n})

is added to R′ for all symbols f_{w}, f_{w′} in F when w′ ⋖ w. In example 2, R′ would have contained the extra rules f_{s}(x)⟶f_{s_{1}}(x), f_{s}(x)⟶f_{s_{2}}(x) , g_{s}(x)⟶g_{s_{1}}(x) and g_{s}(x)⟶g_{s_{2}}(x). Together with a rule a⟶b, R′ is a reflection of R where the rewrite sequence f_{s}(g_{s}(a))⟶_{R′} f_{s}(g_{s}(b))⟶_{R′} f_{s}(g_{s_{1}}(b))⟶_{R′} f_{s_{2}}(g_{s_{1}}(b)) is the desired

⌊f(g(a))⌋⟶ \begin{matrix}+ \\ R′ \end{matrix} ⌊f(g(b))⌋.

A reflection R′ can then be defined

R′ = {⌊lμ⌋⟶⌊rμ⌋ | l⟶r ∈ R, μ specialization } ⋃
{f_{w}(x_{1}, …, x_{n})⟶f_{w′}(x_{1}, …, x_{n}) | f_{w} ∈ F, w′ ⋖ w}

Using the lexicographic path ordering, the extra rules are decreasing iff f_{w} ≻_{F} f_{w′} in the precedence when w′ ⋖ w. The relation ≻_{F} being transitive, this means that f_{w} ≻_{F} f_{w′} for all w, w′ where w′ < w. However, we can allow a precedence f_{w} ≈_{F} f_{w′} by replacing each function symbol f_{w} in R′ with a canonical element of the class [f_{w}]_{≈_{F}} with respect to f and omitting the obvious extra rules.

The first version of our method is thus described by the following theorem:

Theorem 5 A finite, sort-decreasing order-sorted rewrite system R terminates if

⌊lμ⌋ ≻_{lpo} ⌊rμ⌋

for each rule l⟶r in R and each specialization μ of the variables in the rule, provided that the precedence ≿_{F} satisfies

f_{w} ≿_{F} f_{w′}

for all symbols f_{w}, f_{w′} ∈ F where w′ < w.

This method, which can be applied to other termination orderings in the same way, can be totally automated and contains as special cases the method published in [Gn92a] and the method that ignores sort information (by letting f_{w} ≈_{F} f_{w′} in the precedence for all function symbols f in Σ and labels w and w′). The main disadvantages of the method are:

1. Loss in efficiency, even though investigating each specialization seems inherent to most problems in order-sorted rewriting.

2. R′ contains a rule f_{w}(x_{1}, …, x_{n})⟶f_{w′}(x_{1}, …, x_{n}) whenever w′ ⋖ w even in systems where an F -jump from f_{w} to f_{w′} cannot occur. If, for instance, all specializations of all rules are sort-preserving, no F -jump can take place, and therefore all restrictions on the precedence ≿_{F} are superfluous. This problem is addressed in section 4.2.

3. A possible F -jump form f_{w} to f_{w′} can be handled in more elaborate ways than just adding a rule f_{w}(x_{1}, …, x_{n})⟶f_{w′}(x_{1}, …, x_{n}). This opportunity is dealt with in the next section.

4. The method requires sort-decreasing rules. In section 4.2 we will indicate how it can be extended to non-sort-decreasing systems as well.

An example

Let us see how the method can be applied to the following system, which cannot be shown to terminate by ignoring sort information:

Example 3 Let a rewrite system R be

sorts: s′, s

s′ ≤ s funcs: f : s→s

g : s→s a : s b : s′

rules: (∀x:s′) f(x)→g(x)

g(a)→f(a)

Since s′ < s the precedence ≿_{F} must satisfy g_{s} ≿_{F} g_{s′} and f_{s} ≿_{F} f_{s′} and

\begin{aligned}⌊f(x:s′)⌋ = f_{s′}(x) & ≻_{lpo} & g_{s′}(x) = ⌊g(x)⌋ \\ ⌊g(a)⌋ = g_{s}(a) & ≻_{lpo} & f_{s}(a) = ⌊f(a)⌋ \end{aligned}

which are all satisfied with the precedence

g_{s} ≻_{F} f_{s} ≻_{F} f_{s′} ≻_{F} g_{s′}

4 Extensions of the method

4.1 A more elaborate treatment of possible F -jumps

A possible F -jump from f_{w} to f_{w′} is handled with an extra rule f_{w}(x_{1}, …, x_{n})⟶ f_{w′}(x_{1}, …, x_{n}) in R′ (or by having f_{w} ≈_{F} f_{w′}), forcing the precedence to satisfy f_{w} ≿_{F} f_{w′}. The following example shows a weakness of this approach:

Example 4 Let the signature Σ and the terminating rewrite system R be given

sorts: s′, s

s′ ≤ s funcs: f : s→s

g : s′→s h : s→s h : s′→s′ a : s b : s′

rules: (∀x:s′) f(x)⟶f(g(x))

a⟶b To have the desired inequality

⌊f(x:s′)⌋ = f_{s′}(x) ≻_{lpo} f_{s}(g_{s′}(x)) = ⌊f(g(x))⌋

we need f_{s′} ≻_{F} f_{s}, but our method requires f_{s} ≿_{F} f_{s′} since s′ ≤ s. Note also that an F -jump from f_{s} to f_{s′} may occur because of the second rule.

We may have an F -jump from f_{s_{1},..,s_{i},..,s_{n}} to f_{s_{1},..,s′_{i},..,s_{n}} if f is “applied” to an instance lσ⟶rσ of a rule where LS(lσ) = s_{i} and LS(rσ) = s′_{i} or if there is a function symbol g in Σ such that LS(g(… lσ …)) = s_{i} and LS(g(… rσ …)) = s′_{i}. In example 4, we have F -jumps from f_{s} to f_{s′} because f is “applied” to the second rule (f(a)⟶_{R} f(b)) and because h “changes” value sort (e. g. f(h(a))⟶_{R} f(h(b)) , f(h(h(a)))⟶_{R} f(h(h(b))), …).

An extra rule

f_{s_{1},..,s_{i},..,s_{n}}(x_{1}, …, x_{i}, …, x_{n})⟶f_{s_{1},..,s′_{i},..,s_{n}}(x_{1}, …, x_{i}, …, x_{n})

may therefore be replaced by a rule

f_{s_{1},..,s_{i},..,s_{n}}(x_{1}, …, ⌊lμ⌋, …, x_{n})⟶f_{s_{1},..,s′_{i},..,s_{n}}(x_{1}, …, ⌊rμ⌋, …, x_{n})

for every rule specialization lμ⟶rμ where LS(lμ) = s_{i} and LS(rμ) = s′_{i} and with a rule

f_{s_{1},..,s_{i},..,s_{n}}(x_{1}, …, g_{w}(y_{1}, …, y_{m}), …, x_{n})⟶f_{s_{1},..,s′_{i},..,s_{n}}(x_{1}, …, g_{w′}(y_{1}, …, y_{m}), …, x_{n})

for each pair g_{w}, g_{w′} of function symbols in F where w′ ⋖ w, LS(g(\overline{x}: w)) = s_{i} and LS(g(\overline{y}:w′)) = s′_{i}.

Unfortunately, we do not have

f_{s_{1},..,s_{i},..,s_{n}}(x_{1}, …, ⌊lμ⌋, …, x_{n}) ≻_{lpo} f_{s_{1},..,s′_{i},..,s_{n}}(x_{1}, …, ⌊rμ⌋, …, x_{n})

or

f_{s_{1},..,s_{i},..,s_{n}}(x_{1}, …, g_{w}(y_{1}, …, y_{m}), …, x_{n}) ≻_{lpo} f_{s_{1},..,s′_{i},..,s_{n}}(x_{1}, …, g_{w′}(y_{1}, …, y_{m}), …, x_{n})

if the arity of f is greater than 1 and f_{s_{1},..,s_{i},..,s_{n}} ≿̸_{F} f_{s_{1},..,s′_{i},..,s_{n}}. Using any path ordering, all function symbols that violate the restriction w′ < w ⟹ f_{w} ≿_{F} f_{w′} must be unary. Other orderings, such as the Knuth-Bendix-ordering [KB70], do not have this restriction. For the lexicographic path ordering, this method can be described by the following theorem:

Theorem 6 Assume that Σ is a finite order-sorted signature and R a finite set of sort-decreasing rewrite rules. R terminates if the following conditions are satisfied:

1. For any non-unary function symbol g in Σ

g_{w} ∈ F ∧ w′ < w ⟹ g_{w} ≿_{F} g_{w′}

2. For every rule l⟶r in R and every specialization μ

⌊lμ⌋ ≻_{lpo} ⌊rμ⌋

3. For any pair f_{s}, f_{s′} in F where s′ < s and f_{s} ≿̸_{F} f_{s′} we have

• f_{s}(⌊lμ⌋) ≻_{lpo} f_{s′}(⌊rμ⌋), that is ⌊lμ⌋ ≻_{lpo} f_{s′}(⌊rμ⌋), for every rule specialization lμ⟶rμ where LS(lμ) = s and LS(rμ) = s′.

• f_{s}(g_{w}(x_{1}, …, x_{n})) ≻_{lpo} f_{s′}(g_{w′}(x_{1}, …, x_{n})), that is g_{w} ≻_{F} f_{s′} and g_{w} ≻_{F} g_{w′}, for each pair g_{w}, g_{w′} in F where w′ ⋖ w, LS(g(\overline{x} : w)) = s and LS(g(\overline{y}:w′)) = s′.

Although the method becomes quite complicated with this version it can be fully automated and can be used to prove termination of the system in example 4.

Example 4 (cont.) We need f_{s′} ≻_{F} f_{s} to obtain the inequality f_{s′}(x) ≻_{lpo} f_{s}(g_{s}(x)). Therefore, the inequalities f_{s}(a) ≻_{lpo} f_{s′}(b) and f_{s}(h_{s}(x)) ≻_{lpo} f_{s′}(h_{s′}(x)) must also hold. The precedence

a ≿_{F} h_{s} ≻_{F} f_{s′} ≻_{F} f_{s} ≿_{F} g_{s} ≿_{F} g_{s′} ≿_{F} b ≿_{F} h_{s′}

satisfies all the requirements of method 2 and hence termination of the system is established.

The process described above can then be repeated such that an extra rule

f_{s}(g_{w}(x))⟶f_{s′}(g_{s′}(x))

in R′ is replaced by a set of rules

f_{s}(g_{w}(⌊lμ⌋))⟶f_{s′}(g_{s′}(⌊rμ⌋))

and a set of rules

f_{s}(g_{w}(h_{s_{1}}(x)))⟶f_{s′}(g_{s′}(h_{s_{2}}(x)))

for all necessary rule specializations and pairs of F -symbols. Then, the rule f_{s}(g_{w}(h_{s_{1}}(x)))⟶ f_{s′}(g_{s′}(h_{s_{2}}(x))) may be substituted in the same way, and this process can continue. However, the process may not terminate. Assume for instance that the system in example 4 is extended and that we need a precedence h_{s′} ≻_{F} h_{s}. Then, a (possible) extra rule h_{s}(x)⟶h_{s′}(x) is replaced by h_{s}(a)⟶h_{s′}(b) and h_{s}(h_{s}(x))⟶h_{s′}(h_{s′}(x)). The latter is not decreasing in the ordering and is therefore replaced by h_{s}(h_{s}(a))⟶h_{s′}(h_{s′}(b)) and h_{s}(h_{s}(h_{s}(x)))⟶ h_{s′}(h_{s′}(h_{s′}(x))) which is replaced by … and so on.

It may happen (at least for the path orderings) that the number of iterations necessary to prove termination is bounded by the depth of the terms in the rules in R.

4.2 Possible F -jumps

Until now, we have assumed (more or less) that an F -jump from f_{s_{1},..,s_{i},..,s_{n}} to f_{s_{1},..,s′_{i},..,s_{n}} can occur whenever s′_{i} < s_{i} and have concentrated on how to handle such a possible jump. However, in some systems an F -jump from f_{s_{1},..,s_{i},..,s_{n}} to f_{s_{1},..,s′_{i},..,s_{n}} may not occur. Our method can be strengthened by computing the set of F -jumps that actually can take place. A more thorough analysis also has the advantage that the proposed method can be used on non-sort-decreasing systems as well, which is exemplified by the following system:

Example 5 Let a terminating rewrite system be given

sorts: s, s_{1}, s_{2}, s_{3}, s_{4}

s_{1} ≤ s
s_{2} ≤ s
s_{3} ≤ s
s_{4} ≤ s

funcs: f : s→s

g : s→s
g : s_{3}→s_{1}
g : s_{4}→s_{2}
h : s_{1}→s_{2}
a : s_{3}
b : s_{4}

rules: a⟶b

(∀x:s_{1}) f(x)⟶f(h(x))

The second rule implies that an unsorted analysis cannot prove termination of the system which is non-sort-decreasing by the first rule. An analysis of the system gives the set of possible F -jumps as follows:

g_{s_{3}} to g_{s_{4}}  (g(a)⟶_{R} g(b))
g_{s_{1}} to g_{s_{2}}  (g(g(a))⟶_{R} g(g(b))
f_{s_{3}} to f_{s_{4}}  (f(a)⟶_{R} f(b))
f_{s_{1}} to f_{s_{2}}  (f(g(a))⟶_{R} f(g(b))

In a first approach, each possible F -jump from f_{w_{1}} to f_{w_{2}} imply a restriction f_{w_{1}} ≿_{F} f_{w_{2}} using the lexicographic path ordering. In this example we would have the restrictions g_{s_{3}} ≿_{F} g_{s_{4}} , g_{s_{1}} ≿_{F} g_{s_{2}} , f_{s_{3}} ≿_{F} f_{s_{4}} , and f_{s_{1}} ≿_{F} f_{s_{2}} which combined with f_{s_{1}} ≻_{F} f_{s_{2}}, f_{s_{1}} ≻_{F} h_{s_{1}} and a ≻_{F} b proves termination of the system.

A complete analysis with respect to possible F -jumps is quite tedious but it is decidable whether a F -jump from f_{w_{1}} to f_{w_{2}} may take place. Any possible F -jump can then be handled in the way described in the previous section.

4.3 Other improvements

The method presented here can be improved in many ways, e. g. in finding more suitable orderings which tackle the specific problems with the method, making the method more efficient. Another improvement, also mentioned in [Gn92a], is to “preprocess” the rewrite system before applying the technique presented here. For instance, a rule (∀x:s) l⟶r can be replaced by two rules (∀x: s_{1}) l⟶r and (∀x: s_{2}) l⟶r provided that there is no ground term of sort s which is not a term of either sort s_{1} or sort s_{2}.

5 Conclusion

The method presented is an extension of the works of Gnaedig [Gn92a] and Ganzinger [Gan91]. The latter is not concerned with termination when transforming an order-sorted system into a many-sorted one for completion purposes, but introduces the idea of labelling function symbols and adding equations/rules to handle F -jumps. Gnaedig [Gn92a] requires, in addition to sort-decreasingness, that the signatures are minimal. That approach has the advantage of being more efficient, but our method has been shown to be significantly stronger.

The technique presented is only one of many approaches to the problem of proving termination of order-sorted rewriting. A totally different idea we have been looking at, is to handle variables in better ways in the termination orderings, always achieving the crucial t ≻ t′ ⟹ tσ ≻ t′σ. In unsorted orderings, a variable is not comparable to any term not containing the same variable. This restriction can sometimes be loosened by letting a variable of sort s be comparable to some terms that are not of sort s. In [Ølv94] we propose an extension to the lexicographic path ordering based on this principle, thereby being able to prove termination of a system which cannot be shown to terminate with the method given in this paper.

Acknowledgements: I would like to thank Olav Lysne for comments on the full version [Ølv94] of this paper.

References

[CH93] H. Chen and J. Hsiang. Order-Sorted Equational Specification and Completion. Unpublished note, Department of Computer Science, State University of New York at Stony Brook, 1993.

[Der82] N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science 17(3):279-301, 1982.

[Der87] N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3:69-116, 1987.

[DJ90] N. Dershowitz and J.P. Jouannaud. Rewrite systems. Handbook of Theoretical Computer Science, chapter 15, North-Holland, 1990.

[Gan91] H. Ganzinger. Order-sorted completion: the many-sorted way. Theoretical Computer Science 89(1991) 3-32.

[GKK90] I. Gnaedig, C. Kirchner and H. Kirchner. Equational Completion in Order-Sorted Algebras. Theoretical Computer Science 72:169-202, 1990.

[GM88] J. A. Goguen and J. Meseguer. Order-Sorted Algebra I. Center for the Study of Language and Information, Stanford University, 1988.

[Gn92a] I. Gnaedig. Termination of order-sorted rewriting. Proc. Algebraic and Logic Programming. Third International Conference, Springer-Verlag, 1992.

[Gn92b] I. Gnaedig. ELIOS-OBJ: theorem proving in a specification language. Proc. ESOP ’92, 4th European Symposion on Programming, Springer-Verlag, 1992.

[GW88] J. A. Goguen and T. Winkler. Introducing OBJ3. Tech. report, SRI International, Computer Science Lab., 1988.

[KB70] D. Knuth and P. Bendix. Simple word problems in universal algebras. J. Leech, editor, Computational Problems in Abstract Algebra, pages 263-297, Pergamon Press, Oxford, 1970.

[KL80] S. Kamin and J.-J. Lévy. Two generalizations of the recursive path ordering. Unpublished note, Dept. of Computer Science, University of Illinois, Urbana, IL.

[Wal92] U. Waldmann. Semantics of order-sorted specifications. Theoretical Computer Science 94(1992) 1-35.

[Ølv94] P. C. Ølveczky. Terminering av typeordnet omskrivning. Masters thesis, Dept. of Informatics, University of Oslo, 1994. In Norwegian.