Fitting Semantics for Conditional Term Rewriting

1 Introduction

Conditional term rewriting systems (CTRS) have at­ tracted much attention in the recent past as a useful generalization of the simpler formalism of term rewriting systems (TRS). But CTRS have not been uncondition­ ally accepted, due to the absence of well defined seman­ tics for conditional rewriting mechanisms. This paper suggests one remedy, following the approach of Melvin Fitting, who suggested similar semantics for Prolog-style logic programs [5].

Past work on the semantics of conditional term rewrit­ ing has followed three directions:

1. Impose restrictions on the syntax of the CTRS for­ malism to ensure termination and the existence of a unique precongruence which is considered to de­ scribe the meaning of the rewrite relation [8]. This approach does not define the meaning of rewriting when the CTRS does not satisfy the relevant ter­ mination criterion. Also, the termination criterion itself is undecidable, and is not a necessary condi­ tion for each rewrite step and all rewrite sequences to terminate finitely.
2. Give logical semantics for a CTRS R as a set of conditional equations t(R) together with a set of "default" negative equality literals [13]. This ap­ proach is useful if all rewrite sequences terminate or if the CTRS is intended to describe a specification based on a set of free constructor functions.
3. Transform CTRS into "equivalent" TRS, and iden­ tify the semantics of the CTRS with that of the

transformed systems [1]. Assign an "initial algebra" semantics for TRS. The drawback of this approach is that it does not adequately describe the oper­ ational use of CTRS with negative literals in the antecedents of rules.

This paper attempts to fill the lacuna using an elegant approach of Fitting, following Kripke[10] who brought together Kleene's multivalued logics [9], and Tarski's lattice-theoretical fixpoint theorem [16]. Fitting [5] uses this approach to present an alternative to the semantics of logic programming given by Apt and Van Emden [2]. The main contribution of this paper is to show that this approach can also successfully explain the meaning of conditional rewriting systems with negation, including the problematic CTRS whose semantics have eluded the grasp of previous approaches

(e.g., p =/: q => p-+ q,p = q => p-+ q).

In the next section, we introduce CTRS and point out the deficiencies of a two-valued fixpoint semantics. In section 3, following some mathematical preliminaries, we describe the new semantics for conditional rewriting. Several examples are then given in section 4 to illustrate the semantics. References follow concluding remarks.

2 Preliminaries

2.1 Conditional Rewriting

We define the formalism and operational use of a lan­ guage for expressing data type and function specifica­ tions [13, 8].

Definition 1 Equational-lnequationai-Conditional Term Rewriting Systems (EI-CTRS) are finite sets of rules of the general form

[s1 = t1/\ .. . 1\sn = tn/\P1=/:q1/\ ... 1\pm=/:qm] => lhs-+rhs ,

where lhs and rhs are two terms, and the antecedent is a conjunction of zero or more equations s; = t; and negated equality literals Pi =/: qi. Every variable occur­ ring in each s;, t; , Pi, qi and rhs must also occur in l hs.

Following the notation of [4], 'p/j' refers to the subterm of p at position j, and 'p[q]j' refers to the result of replacing pf j by q in p. For in­ stance, when positions are described in Dewey dec­ imal notation, f(g(a, h(b, c)), d)/1.2 is h(b, c), and f(g(a, h(b, c)), d)[m]1.2 is f(g(a, m), d) .

Besides matching and replacement, conditional rewrit­ ing requires checking that the antecedent of a rule holds. The basic idea underlying the definition of EI-rewriting is to conclude that two terms are equal if they have converging reduction sequences, and not equal otherwise (for ground terms) . Not surprisingly, the attempt to find a valley-proof for an equality does not always terminate. But if reduction sequences from two ground terms p, q do terminate without converging, then we can assert that p = q has no 'valley-proof' using the given rewriting system.

Variables in different rules are first renamed to be dis­ tinct from each other and from those in the term to be EI-reduced.

Definition 2 : A term m EI-Reduces (or EI-Rewrites) to n using an EI-CTRS R (written m-+Rn) if R con­ tains a rule cond=::}/hs-+rhs and there is a substitution u matching lhs with a sub term m/ j of m, such that each of the following conditions hold:

1. Match and Replace: (lhs)u==.m/j and n==.m[(rhs)u]j.
2. Demonstrable Convergence: For each equality s; = t; E cond, there is a common term to which s;u and t;u can be EI-reduced in a finite number of steps.
3. Demonstrable Non-Convergence: For every negated equality literal s;#t; E cond, it can be demonstrated by finite EI-rewriting sequences that s;u and t;u are ground terms with no common reduct. More pre­ cisely, the following conditions must hold:

(i) s;u and t;u are ground terms;

(ii) all EI-rewriting sequences from s;u and t;u ter­ minate; and

(iii) the set of all reducts of s;u is disjoint from that of t;u.

For a more detailed description of El-rewriting with examples, see [14].

2.2 Fixpoint Semantics

Definition 3 Iff is a function (of one argument) whose domain and range are the same, then S is a fixpoint (or fixed point) off whenever f(S) = S. If the domain el­ ements are partially ordered, f may have zero or more partially ordered fixpoints:

- a fixpoint S is minimal if there is no other fixpoint T such T < S in the ordering;

- a minimal fixpoint S is the least fixpoint if S ~ T for every fixpoint;

- a fixpoint S is maximal if there is no other fixpoint T such that T > S in the ordering;

- two fixpoints S, T are compatible if they have a com­ mon upper bound which is a fixpoint,

i .e., 3S' .(S ~ S') 1\ (T ~ S') 1\ (f(S') = S');

- a fixpoint is intrinsic [10] (or optimal (12]) iff it is com­ patible with every fixpoint of f.

In the fixpoint semantics approach, the 'meaning' of a program is considered to be the least fixpoint of a func­ tion/relation which represents the behavior of the pro­ gram on some input. The following fixpoint semantics can be suggested for conditional rewriting, as in [8] . A function 'IF R is associated with each CTRS R such that if Sis a binary relation, and S* is its reflexive transitive closure, then WR(S) is a binary relation which is the set of all two-tuples (p, q) such that for some rule [s1 = t11\ ... 1\sn = tn]l\[pl#qll\ .. . 1\pm#qm] =::} l-+r in R, we have 3k, 3u. pfk =: /u, q =: p[ru]k, Vi, 3r;.(s;u, r;) E S* and (t;u, r;) E s·, and Vj, there is no Tj such that {PjU,rj} E S*, {qju,rj} E S*. In this approach, the 'meaning' of rewriting with R is identified with the least fixed point of 'IF R, if it exists.

But such a least fixed point exists only when the CTRS satisfies certain stringent (and undecidable) conditions that ensure the decidability and finite termination of all rewrite sequences. The following is an example of a CTRS R such that 'IF R has no fixpoint according to the above definition: {a # b =::} a --+ b}. Note that {(a, b)} is not a fixpoint because the antecedent a =F b of the conditional rule is such that 3x.(a, x) and (b, x) are members of {(a, a), (a, b), (b, b)}, the reflexive symmetric closure of {(a, b)}.

The problems with the above approach can be pin­ pointed to the following reasons:

1. The use of a two-valued logic precludes distinguish­ ing between cases when we know that a rewrite doesn't occur, and cases when we do not know whether a rewrite can occur, particularly cases involving non-terminating reductions arising from terms in the antecedent of an invoked rewrite rule.
2. The relation WR is not 'monotone'.

Definition 4 A mapping<) is monotone iff for all the el­ ements in the (partially ordered) domain, S ~ T implies <)(S) ~ <)(T).

2.3 Kleene's 3-valued logic

Kleene [9] presented a three-valued logic, partly mo­ tivated by the desire to give truth-value meanings to partial recursive functions. The logic lends itself easily to explain non-deterministic and infinite computations. Kleene's third truth value represents the indeterminate or unknown nature of statements. The truth, falsehood, or indeterminacy of statements may be captured by us­ ing Smullyan's notation of 'signed statements':

Definition 5 If 1/J is a statement, T'I/J is a signed state­ ment which is to be understood as asserting "1/J is true". Similarly, F'ljJ is a signed statement which is to be un­ derstood as asserting "1/J is false", which is contradictory to T'I/J. A set of signed statements is consistent if it does not contain the pair T1/J, F'ljJ for any statement 1/J.

Implicitly, if a set of signed statements contains nei­ ther T'ljJ nor F'ljJ for some formula 1/J, it is understood that 1/J is indeterminate or has Kleene's third truth value.

'Saturated' consistent sets of signed statements are in­ tended to serve as models for logic programs. To sum­ marize a lengthy definition in [5], a set S of signed statements is saturated iff it contains the intuitive con­ sequences of the members of S; e.g.,

- T(X 1\ Y) E S implies T(X) E S and T(Y) E S,

- F(Vx.P(x)) E S implies F(P(t)) E S for some closed term t,

- FX E S implies T(·X) E S,

- FX E Sand FY E Simply F(X VY) E S, et cetera.

3 New Semantics

Unlike Prolog-style logic programs, the operational use of CTRS involves iterated rewrites ensuing from the antecedents of conditional rules. So the definition of conditional rewriting recursively involves that of iter­ ated rewriting. A careful definition of what it means for "p -:R q" to be "false" is needed, since this is needed when evaluating negated equality literals in the antecedents of rules.

Let S be a consistent set of signed two-tuples; intu­ itively, S is a potential description of a rewrite relation. T(p, q} E S is an abbreviation for T(Rewrites(p, q)), intended to mean that p rewrites to q; and similarly F(p, q} E S means p is known not to rewrite to q. If neither of these is present in S, that means the reduc­ tion from p to q is not known to be true or false, i.e., "p- q" has the third truth value.

A new set of signed statements S*, describing the it­ eration of rewrites in S, is defined as follows. For con­ venience, let S* = S-T l:tJ S'}, distinguishing sets of state­ ments with prefixes T and F, respectively. S-T is just the reflexive transitive closure of the true statements in S, which is the least set satisfying the following three conditions.

1. Va. T{a, a} ES-T,
2. Va, b, if T(a, b} E S, then T(a, b} ES-T, and
3. \::Ia, b, c, if T(a, b} E S-T and T(b, c} E S-T, then T(a, c) ES-T.

The construction of S'} is slightly more compli­ cated; note that F(a, b) E S does not necessarily im­ ply that F(a,b) E S*: a rewrite sequence from a to b might exist through some other terms, e.g., if {F(a, b), T(a, c), T(c, b)}~ S, then T(a, b} E S*.

To conclude the absence of rewrite sequences, there should be no intermediate term from which a reduction sequence can occur. It is safe to assert that (p -:R q) is false iff it can be determined that there is no rewrite sequence of finite length from p to q. This aspect can be described by an iterative construction as follows, where s}.. represents 2 tuples among which there is no reduction sequence of length ~ i.

Note: Vi, S/ 1 ~ S}.., thus S'} is the greatest lower bound of a chain of sets in the subset ordering.

Example 1 Let the language contain only the constants a,b,c,d.

So­

F-

S l­

F-

{F(a, b), F(a, c}, F(a, d) ,

F(b, a), F(b, c}, F(b, d),

F(c, a), F(c, b), F(c, d),

F(d, a), F(d, b}, F(d, c)}

{F(a, c), F(a, d),

F(b, a), F(b, d),

F(c, a}, F(c, b},

F(d, a}, F(d, b}, F(d, c}}

S'}=S}={F(b, a), F(c, a}, F(c, b}, F(d, a), F(d, b), F(d, c)} Example 2 Let the language contain only the constants a,b,c, d.

S'}=S}={F(b, a), F(c, a}, F(c, b), F(d, a), F(d, b), F(d, c)} In this case, S* = S-T US'} contains neither T(c, d) nor F(c, d}.

Lemma 1 If S is consistent, then s· is also consistent.

Lemma 2 The '*'operator is monotone, i.e., if S1 ~ S2. then Si ~ S2.

Definition 6 When R is an EI-CTRS, a mapping <PR from sets of signed two-tuples to sets of signed two-tuples is defined as follows:

<PR(S) is the smallest relation such that

• T(a, b) E <PR(S) if R contains a rule

such that for some position k and some substitution (T 1 we have

Lemma 3 If Sis consistent, then <PR(S) is consistent. Theorem 1 <PR is monotone, i.e.,

Proof: Assume S1 ~ S2. If T(a, b) E <PR(S1) , then R contains a rule

Since Si ~ S2 (by lemma 2), we have

Therefore, T(a, b) E <PR(S2), if T(a, b) E <PR(St). Similarly, it can be shown that if F(a, b) E <PR(St), then F(a, b) E <PR(S2)·

Key Observation: The fixpoints of <PR describe these­ mantics of conditional rewriting with an EI-CTRS R; par­ ticularly important are the least fixpoint and the largest intrinsic fixpoint.

We now investigate the fixpoints of the monotone re­ lation <P R corresponding to each rewrite system R.

Theorem 2 Let R be any EI-CTRS, and <PR be as defined above. Then:

1. <PR has maximal fixpoints.
2. <P R has a smallest fixpoint.
3. <P R has a largest intrinsic fixpoint, which is a subset of n{maximal fixpoints of <PR}.
4. The smallest fixpoint of <PR above the empty set is intrinsic.

Proof: Let D be the collection of all consistent sets of signed statements, ordered by the subset relation. D has a smallest member { } , since the empty set is consistent. Every chain S1 ~ S2 ~ · · · of elements of D has an upper bound UlimS;. Also, every nonempty set having

i an upper bound has a least upper bound. Since <P R is monotone on D, all the premises of theorem 2.2 in [6] are satisfied, and the conclusions stated in this theorem directly follow. 0

A smallest fixpoint can be constructed using the fol­ lowing transfinite sequence of consistent sets of signed statements.

Definition 7 Let <PR be as defined earlier, for any EI­ CTRS R.

By transfinite induction, it can be shown that this is a weakly increasing sequence, i.e., Aa ~ Aa+l for all a. But the sequence cannot be strongly increasing, i.e., it is not possible that 'v'a · Aa < Aa+l, since a sequence of consistent sets cannot have as many members as there are ordinals. Hence, for some a, we must have Aa = <PR(Aa), i.e., some member of the sequence is a fixpoint of <PR.

4 Examples

The following are some examples which illustrate the application of the new fixpoint semantics. Some of the CTRS's considered here cannot be handled ade­ quately by previously given semantics, because they do not satisfy the conditions for termination, and are not constructor-based specifications. In each case, we as­ sume that the only symbols in the language are those that appear in the rules of the rewriting system being considered. For each CTRS R, we begin with candidates for fixpoints which are sup~rsets of 'Z', defined as

The rationale is that for any S, <PR(S) will always con­ tain F(p, q), for those pairs of terms p, q such that no rule in R can possibly reduce p to q.

Example 3 Let R1 be {a= b ~a--+ b}.

Let Z = {F(a, a), F(b, a), F(b, b)}. Candidates for the fixpointsof<PR 1 are: Z, ZU{T(a,b)}, and ZU{F(a,b)}. Each of these is a fixpoint; Z itself is the least fixpoint, whereas the other two are maximal fixpoints, with each of which Z is compatible. Hence Z is also the greatest intrinsic fixpoint of <P R 1 ·

Example 4 Let R2 be {a :f:. b =>a~ b}.

Again, let Z = {F(a, a), F(b, a), F(b, b)}. Candidates for the fixpoints of ~R2 are also again Z, Z U {T(a, b)}, and Z U {F{a, b)}. Of these, only Z is a fixpoint: note that ~R2 (Z U {T{a, b)}) will contain F(a, b), and ~R2 (ZU{F(a, b)}) will contain T(a, b). Hence the others are not fixpoints of ~ R 2 ·

Example 5 Let R3 be {a :f:. c =>a~ b}.

Let Z = {F(a, a), F(a, c), F(b, a), F(b, b), F(b, c), F(c, a), F{c, b), F(c, c)}. Candidates for the fixpoints of ~Rs are Z, Z U {T{a, b)}, and Z U {F{a, b)}. Of these, Z is a fixpoint, because the absence of T(a, b) and F(a, b) from Z implies that ~R3 (Z) will contain neither T(a, b) nor F(a, b). Also, Z U {T(a, b)} is a fix­ point since ~R2 (Z U {T{a, b)}) will contain T(a, b). But ~R2 (Z U {F(a, b)}) will contain T(a, b), hence the third candidate is not a fixpoint. Hence Z is the least fixpoint, whereas ZU{T{a, b)} is the only maximal fixpoint, which is hence the greatest intrinsic fixpoint.

Example 6 Let~ be {a= c =>a~ b}.

Let Z = {F(a, a), F(a, c), F(b, a), F(b, b), F(b, c), F(c, a), F{c, b), F(c, c)} again. Candidates for the fix­ points of ~R4 are Z, Z U {T(a, b)}, and Z U {F(a, b)}. Of these, Z is again a (least) fixpoint. Z U { F (a, b)} is also a fixpoint, but not ZU{T(a, b)}. Thus ZU{F(a, b)} is the greatest intrinsic fixpoint.

Example 7 Let Rs be {c :f:. d =>a~ b}.

Let Z = {F(a, a), F(a, c), F{a, d), F(b, a), F(b, b), F(b, c), F(b, d), F(c, a), F{c, b), F(c, c), F(c, d), F(d, a), F(d, b), F(d, c), F(d, d)}. Candidates for the fixpoints of ~Rs are Z, Z U {T{a, b)}, and Z U {F(a, b)}. This time, Z is not a fixpoint because ~R.(Z) contains T(a, b). For the same reason, ZU{F(a, b)} is also not a fixpoint. The only fixpoint is Z U {T(a, b)}.

Example 8

Let R6 be { c :f:. d => a ~ b, a :f:. b => c ~ d}. Let Z = {F(a, a), F(a, c), F{a, d), F(b, a), F(b, b), F(b, c), F(b, d), F(c, a), F{c, b), F(c, c), F(d, a), F(d, b), F(d, c), F(d, d)}. Candidates for the fixpoints of ~ Re are those supersets of Z which contain at most one of T(a, b), F(a, b), and also at most one of T(c, d), F(c, d). Of these, Z itself is a (least) fixpoint since it does not contain signed tu­ ples which would enable either of the rewrite rules in R6 to be activated. If a fixpoint contains F(a, b), then it must also contain T{c, d) since the second rewrite rule is activated; indeed, Z U {F{a, b), T(c, d)} is a (maximal) fixpoint. Similarly, ZU{F{c, d), T(a, b)} is also a (maxi­ mal) fixpoint. These maximal fixpoints are not mutually compatible, and Z is a fixpoint compatible with each of these maximal fixpoints. Hence Z is the least as well as the largest intrinsic fixpoint.

It can be shown that the other candidates are not fix­ points. For instance, ~R. (ZU{T(a, b)}) does not contain T(a, b), since the antecedent of the first rewrite rule is not enabled: F(c, d) tf. Z U {T(a, b)}

Example 9

Let R1 be {a = b => a ~ b, a :f:. b => a ~ b} .

Let Z = {F{a, a), F(b, a), F(b, b)}. Candidates for the fixpoints of ~R7 are Z, Z U {T(a, b)}, and ZU {F(a, b)} . Of these, Z is a (least) fixpoint. Also Z U {T(a, b)} is a fixpoint, but not Z U {F(a, b)}. Hence Z U {T(a, b)} is the greatest intrinsic fixpoint. Note that a 'disjunctive' conditional rewriting mechanism which examines the an­ tecedents of multiple rules achieves computation of the greatest intrinsic fixpoint in this case.

Example 10 Let Rs be {c :f:. d =>a~ b, a:f:.b=>a~b} .

Let Z = {F(a, a), F(a, c), F(a, d), F(b, a), F(b, b), F(b, c), F(b, d), F(c, a), F(c, b), F(c, c), F(c, d), F(d, a), F(d, b), F(d, c), F(d, d)}. Candidates for the fixpoints of ~ R· are Z, Z U { T (a, b)} , and Z U {F(a, b)}. Since Z contains F(c, x) and F(d, x) for every x, every superset of Z which is a fixpoint must contain T(a, b) since the first rewrite rule is enabled. Hence Z U {T(a, b)} is the only fixpoint.

Example 11 Let R9 be {c :f:. d =>a~ b, a :f:. b => c ~ d, a = b => c ~ d}. Let Z = {F{a, a), F(a, c), F(a, d), F(b, a), F(b, b), F(b, c), F(b, d), F(c, a), F(c, b), F(c, c), F(d, a), F(d, b), F(d, c), F(d, d)} . Candidates for the fixpoints of ~ Ro are those supersets of Z which contain at most one ofT(a,b), F(a,b), and also at most one ofT(c, d), F(c, d) . Of these, Z itself is a (least) fixpoint since it does not contain signed tuples which would enable either of the rewrite rules in R9 . If a fixpoint contains F(a, b), then it must also contain T(c, d) since the second rewrite rule is activated; indeed, Z U {F{a, b), T(c, d)} is a (maximal) fixpoint .

There are no other fixpoints: every superset of Z which contains F(a, b) or T(a, b) must also contain T(c, d) if it is a fixpoint, since the second or third rewrite rule is enabled. But every superset of Z which contains T(c, d) must also contain F(a, b) if it is a fixpoint, since the antecedent of the first rewrite rule is falsified . And every superset of Z which contains F{c, d) must also con­ tain T(a, b) if it is a fixpoint, since the first rewrite rule is enabled.

Example 12

Let R10 be { c :f:. d => a ~ b, a :f:. b => c ~ d, a= b => c ~ d, c = d =>a~ b}. Again, let Z = {F(a, a), F(a, c), F(a, d), F(b, a), F(b, b), F(b, c), F(b, d), F(c, a), F(c, b), F(c, c), F(d, a), F(d, b), F(d, c), F(d, d)}. We again examine various consistent supersets of Z which are potential candidates for the fixpoints of <I> R,o . Z itself is a (least) fixpoint, as in the previous exam­ ple. If one of the other candidates contains T(a, b), then the third rewrite rule dictates that it must also con­ tain T(c, d) if it is a fixpoint (and conversely). Indeed, Z U {T(a, b), T(c, d)} is a (maximal) fixpoint . Candi­ dates which contain F(a, b) (or F{c, d)) are not fixpoints, because the second (or first) rewrite rule is then en­ abled, generating T(c, d) (or T(a, b), respectively), which in turn implies that the candidate must contain T(a , b) (or T(c, d), respectively) making it inconsistent. Hence there are no other fixpoints.

5 Conclusions

We have investigated the fixpoint semantics of condi­ tional term rewriting systems with negation. Two­ valued semantics does not ascribe a meaning to CTRS's that do not satisfy useful properties such as termination. We have shown that a three-valued approach used by Fitting [5] for Prolog-style logic programs is applicable in this context. A monotone operator is developed, whose fixpoints describe the semantics of conditional rewriting. Several examples illustrate this semantics for 'trouble­ some' rewrite systems which could not be handled easily by previous approaches. This work supports the con­ tention that results achieved in research on Prolog-style logic programming can be useful in the context of con­ ditional term rewriting.

We have hesitated to say whether it is the least fix­ point or the greatest intrinsic fixpoint which better de­ scribes the semantics of the EI-CTRS. The examples may motivate a preference for one or the other. The op­ erational mechanism described in [13] and [8] computed members of the least fixpoint. To compute the greatest intrinsic fixpoint, we need a different operational mech­ anism which uses "disjunctive rewriting" [15] ( cf. ex­ ample 9) as well as a mechanism which returns failure in some cases when naive evaluation of the antecedent leads to non-termination ( cf. example 5). The formu­ lation of such a rewriting mechanism, which computes precisely the greatest intrinsic fixpoint, is an issue for future work. In non-controversial cases, when termina­ tion requirements are satisfied, the least fixpoint and the greatest intrinsic fixpoint coincide ( cf. examples 3, 4, 7) . and are essentially equivalent to the semantics given in previous work for such well-behaved rewrite systems.

Acknowledgements

The author thanks Melvin Fitting and anonymous refer­ ees for their comments on the paper.