Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
MU-TERM 4.0
[go: Go Back, main page]

MU-TERM

A Tool for Proving Termination of Rewriting with Replacement Restrictions

Version 4.0   ---   March 2004

Contents:
   Introduction
Structure and functionality
Use of MU-TERM
Termination of CSR with MU-TERM
Termination of Lazy Rewriting with MU-TERM
Termination of rewriting with MU-TERM
Available
References
Contact

Introduction

Restrictions of rewriting can eventually achieve termination by pruning all infinite rewrite sequences issued from every term. However, proving that such an improvement is actually achieved is challenging. Context-sensitive rewriting (CSR) is a restriction of rewriting which is useful for describing semantic aspects of programming languages (e.g., Maude, OBJ2, OBJ3, or CafeOBJ) and analyzing the computational properties (e.g., termination or completeness) of the corresponding programs [Luc01a, Luc01b, Luc03].

In CSR, a replacement map, i.e., a mapping µ from symbols into subsets of their argument positions, is used to discriminate the argument positions on which replacements are allowed; in this way, a restriction of rewriting is obtained.

Example 1: Consider the TRS [Luc98, Example 6]:
  first(0,X) -> nil
  first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
  from(X) -> cons(X,from(s(X)))
In order to avoid infinite rewritings with expressions involving calls to from, it is natural to forbid rewritings on the second argument of the list constructor cons (i.e., we let µ(cons)={1}). It is possible to prove that such context-sensitive computations are terminating.

In Lazy Rewriting, a replacement map is also used to distinguish between arguments which can be freely eveluated from those which are evaluated only on-demand. Thus, in contrast to CSR, reductions are eventually allowed on non-replacing arguments of symbols f, i.e., arguments i which do not belong to µ(f). See [Luc02] for further details about the connections between CSR and Lazy Rewriting.

Structure and functionality

MU-TERM provides a simple way to deal with Term Rewriting Systems and replacement maps. The application is written in Haskell. MU-TERM consists of around 30 modules containing more than 4000 lines of Haskell code and has been developed with GHC, a popular Haskell compiler. The tool has a graphical user interface which has been developed by using the wxHaskell graphics library.

With MU-TERM you can:

  • Load TRSs, extract the corresponding signature, and associate a replacement map to the symbols of the signature.
  • Modify a replacement map previously associated to the symbols of the signature.
  • Prove termination of Context-Sensitive Rewriting for a given TRS R and replacement map µ. Most available techniques for proving termination of CSR (direct proofs via polynomial oderings, modular decompositions, transformations, etc.) have been implemented.
  • Prove termination of Innermost Context-Sensitive Rewriting for a given TRS R and replacement map µ.
  • Prove termination of Lazy Rewriting for a given TRS R and replacement map µ.
  • Prove termination of Rewriting by using the techniques which have been developed for proving termination of CSR (polynomials over the rational numbers, weakly monotonic orderings together with the Dependency Pairs approach, etc.).

Use of MU-TERM

We provide two different ways to associate a replacement map µ to a given TRS:

  • first load the rules in simple format, i.e., as a sequence 
    	   l1 -> r1
	   l2 -> r2
	   ...
	   ln -> rn
    of rewrite rules li -> ri as in Example 1 above (option 1 of menu File), and then specify the replacement map by using menu Replacement map.... Or else,
  • directly specify the rules and replacement map by using the (simple) Maude/OBJ format (option 2 of menu File)). This provides a more compact description: the replacement map is described by means of strategy annotations (i1 ··· in 0) associated to each symbol; this means that µ(f)={i1,...,in}, if the arity of f is k (zeros are dropped, see [Luc03]). Symbols f without any explicit strategy annotation have no replacement restriction, i.e., µ(f)={1,...,k}.
Example 2: The TRS R and replacement map µ in Example 1 can be specified by the following module: 
  obj Ex6_Luc98 is
    sort S .
    op first : S S -> S .
    op 0 : -> S .
    op nil : -> S .
    op s : S -> S .
    op cons : S S -> S [strat (1 0)] .
    op from : S -> S .
    vars X Y Z : S .
    eq first(0,X) = nil .
    eq first(s(X),cons(Y,Z)) = cons(Y,first(X,Z)) .
    eq from(X) = cons(X,from(s(X))) .
  endo
The following à la Maude version would also be accepted: 
  fmod Ex6_Luc98 is
    sort S .
    op first : S S -> S .
    op 0 : -> S .
    op nil : -> S .
    op s : S -> S .
    op cons : S S -> S [strat (1 0)] .
    op from : S -> S .
    vars X Y Z : S .
    eq first(0,X) = nil .
    eq first(s(X),cons(Y,Z)) = cons(Y,first(X,Z)) .
    eq from(X) = cons(X,from(s(X))) .
  endfm

Termination of CSR with MU-TERM

A number of methods have been developed for proving the µ-termination of a TRS R (i.e., termination of CSR for R and the replacement map µ). Basically, we have:

  • Direct methods, i.e., orderings > on terms which can be used to directly compare the left-hand sides and right-hand sides of the rules in order to conclude the µ-termination of the TRS, see [BLR02, Bor03, GL02b, Luc04, Zan97]. MU-TERM implements the techniques described in [Luc04]: we interpret each symbol of the signature as a polynomial with undefined coefficients; then we generate constraints over the undefined coefficients to make them compatible with the µ-termination of the system. We use CiME 2.0 as an external tool to solve these constraints (see the user's manual for further details).

    Example 3: The µ-termination of R in Example 1 can be directly and automatically proved by using MU-TERM
    Proof of termination for Ex6_Luc98:

[first](X1,X2) = X1 + 2.X2
[0] = 1
[nil] = 0
[s](X) = X
[cons](X1,X2) = X1 + 1
[from](X) = X + 2

    The following example shows an interesting capability of MU-TERM: its ability to compute polynomials which use rational coefficients:

    Example 4: Consider the following module which corresponds to an example in the introduction of [GM04]: 
    obj ExIntrod_GM04 is
  sort S .
  op nats : -> S .
  op adx : S -> S .
  op zeros : -> S .
  op cons : S S -> S [strat (0)] .
  op 0 : -> S .
  op incr : S -> S .
  op s : S -> S [strat (0)] .
  op hd : S -> S .
  op tl : S -> S .
  vars X Y : S .
  eq nats = adx(zeros) .
  eq zeros = cons(0,zeros) .
  eq incr(cons(X,Y)) = cons(s(X),incr(Y)) .
  eq adx(cons(X,Y)) = incr(cons(X,adx(Y))) .
  eq hd(cons(X,Y)) = X .
  eq tl(cons(X,Y)) = Y .
endo
    The µ-termination of the TRS can be automatically proved with MU-TERM: 
    Proof of termination for ExIntrod_GM04:

[nats] = 5
[adx](X) = X + 3
[zeros] = 1
[cons](X1,X2) = X1 + 1/2.X2
[0] = 0
[incr](X) = X + 1
[s](X) = 0
[hd](X) = X + 1
[tl](X) = 2.X + 1
    Note that the polynomial interpretation uses a polynomial (for cons) containing rational coefficients.

    Finally, we exemplify the use of simple-mixed polynomial interpretations with the following

    Example 5: Consider the following module which corresponds to Example 5 of [Zan97]: 
    obj Ex5_Zan97 is
  sort S .
  op f : S -> S .
  op if : S S S -> S [strat (1 2 0)] .
  op c : -> S .
  op true : -> S .
  op false : -> S .
  vars X Y : S .
  eq f(X) = if(X,c,f(true)) .
  eq if(true,X,Y) = X .
  eq if(false,X,Y) = Y .
endo
    The µ-termination of this TRS cannot be proved by using a linear interpretation. However, it can be automatically proved with MU-TERM: 
    Proof of termination for Ex5_Zan97:

[f](X) = 3.X + 2
[if](X1,X2,X3) = X1.X3 + X1 + X2 + 1
[c] = 0
[true] = 0
[false] = 1

  • Transformations from TRSs R and replacement maps µ that obtain a TRS R'. If we are able to prove termination of R' (using the standard methods), then the µ-termination of R is ensured, see [FR99, GM04, Luc96a, Zan97]. Our tool, MU-TERM, implements these transformations using a common environment that eases their combination and comparison.

    Example 6: The µ-termination of R in Example 1 can also be automatically proved by first using the transformation of Luc96a to obtain the following TRS RL: 
    first(0,X) -> nil
first(s(X),cons(Y)) -> cons(Y)
from(X) -> cons(X)
    Since termination of rewriting is a particular case of termination of CSR (where µ(f)={1,...,k} for each k-ary symbol f), we can also use MU-TERM to obtain a direct proof of termination of RL (see below).

    We also provide interfaces for using existing tools for proving termination of rewriting, e.g., AProVE, CiME 2.0, the dependency pairs system, Termptation, Tsukuba Termination Tool, etc.

Termination of Lazy Rewriting with MU-TERM

In [Luc02], termination of Lazy Rewriting is proved by using a transformation which permits to use any available technique for proving termination of CSR:

Example 7: The termination of Lazy Rewriting for the following module: 
obj Ex1_2_Luc02c is
  sort S .
  op 2nd : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op from : S -> S .
  op s : S -> S .
  vars X Y Z : S .
  eq 2nd(cons(X,cons(Y,Z))) = Y .
  eq from(X) = cons(X,from(s(X))) .
endo
can be proved by proving termination of CSR for the following system: 
obj Ex1_2_Luc02c_LR is
  sort S .
  op 2nd : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op from : S -> S .
  op s : S -> S .
  op cons1 : S S -> S .
  vars X Y Z X1 : S .
  eq 2nd(cons1(X,cons(Y,Z))) = Y .
  eq 2nd(cons(X,X1)) = 2nd(cons1(X,X1)) .
  eq from(X) = cons(X,from(s(X))) .
endo
which is obtained by applying the transformation in [Luc02] (implemented in MU-TERM).

Termination of rewriting with MU-TERM

Since termination of rewriting is a particular case of termination of CSR (where µ(f)={1,...,k} for each k-ary symbol f), we can also use MU-TERM to prove termination of rewriting.

Example 8: The termination of RL in Example 6 above can be automatically proved by using the polynomial interpretations computed by MU-TERM: 
Proof of termination for CS-TRS  Ex6_Luc98_L:

[first](X1,X2) = X1 + X2
[0] = 1
[nil] = 0
[s](X) = X + 1
[cons](X) = X
[from](X) = X + 1

Nowadays, MU-TERM is the only tool which implements the automatic generation of polynomial orderings based on polynomial intepretations which use rational coefficients. This can be used for proving termination of rewriting.

Example 9: The following TRS R 
f(X) -> u1(X,X)
u1(h(Y),X) -> u2(i(X),X,Y)
u2(Y,X,Y) -> g(Y)
i(X) -> a
a -> u(c)
u(d) -> b
c -> d
can be automatically proved terminating by using the following polynomial interpretation computed by MU-TERM: 
[f](X) = 3.X + 1
[u1](X1,X2) = X1 + 2.X2
[h](X) = X + 3
[u2](X1,X2,X3) = X1 + X2 + X3 + 1
[i](X) = X + 3/2
[g](X) = X
[a] = 1
[u](X) = X + 1/2
[c] = 1/3
[d] = 0
[b] = 0

On the other hand, µ-reduction orderings based on polynomial interpretations over the rationals are also used together with Arts and Giesl's dependency pairs approach to prove termination of rewriting.

Example 10: The µ-termination of Ex1_2_Luc02c_LR in Example 7 above can be proved by using Ferreira and Ribeiro's transformation. The TRS Ex1_2_Luc02c_LR_FR: 
2nd(cons1(X,cons(Y,Z))) -> Y
2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1)))
from(X) -> cons(X,n__from(n__s(X)))
from(X) -> n__from(X)
s(X) -> n__s(X)
activate(n__from(X)) -> from(activate(X))
activate(n__s(X)) -> s(activate(X))
activate(X) -> X
can be proved terminating by using the following polynomial interpretation computed by MU-TERM: 
[2nd](X) = 3.X
[cons](X1,X2) = X1 + 1/3.X2 + 1
[from](X) = 2.X + 3
[s](X) = X + 1
[cons1](X1,X2) = 1/3.X2
[n__from](X) = 2.X + 3
[n__s](X) = X + 1
[activate](X) = X
[nF_2nd](X) = X
[nF_from](X) = 0
[nF_activate](X) = 1/3.X
where nF_2nd, nF_from, and nF_activate are new symbols which have been automatically introduced to compute the dependency pairs that correspond to Ex1_2_Luc02c_LR_FR.

A more detailed justification of these techniques is given in this note: Luc04b.

Available
Download
Examples (Maude/OBJ format)
Proofs of termination with the previous examples using MU-TERM

Previous versions

References

Contact

Salvador Lucas

Please, report any bug, comment, or suggestion to: slucas@dsic.upv.es