Contents:
Introduction Structure and functionality
Termination of CSR with MUTERM
Termination of
Lazy Rewriting with MUTERM
Termination of rewriting with MUTERM
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. Contextsensitive 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.
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 contextsensitive 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 ondemand. Thus, in contrast to CSR, reductions are eventually allowed on nonreplacing 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 
MUTERM provides a simple way to deal with Term Rewriting Systems and replacement maps. The application is written in Haskell 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 MUTERM you can:
We provide two different ways to associate a replacement map µ to a given TRS:
l1 > r1 l2 > r2 ... ln > rnof rewrite rules l_{i} > r_{i} as in Example 1 above (option 1 of menu File), and then specify the replacement map by using menu Replacement map.... Or else,
(VAR X Y Z) (STRATEGY CONTEXTSENSITIVE (first 1 2) (0) (nil) (s 1) (cons 1) (from 1) ) (RULES first(0,X) > nil first(s(X),cons(Y,Z)) > cons(Y,first(X,Z)) from(X) > cons(X,from(s(X))) )You can also do it as an OBJ 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))) . endoThe 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
We refer to [AGIL07,Luc04a] for further details.
Termination of CSR with MUTERM 
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:
Examples of CSTRSs and the corresponding termination proofs by using these techniques can be found here.
Termination of Lazy Rewriting with MUTERM 
In [Luc02], termination of Lazy Rewriting is proved by using a transformation which permits to use any available technique for proving termination of CSR:
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))) . endocan 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))) . endowhich is obtained by applying the transformation in [Luc02] (implemented in MUTERM).
Termination of rewriting with MUTERM 
Since termination of rewriting is a particular case of termination of CSR (where µ(f)={1,...,k} for each kary symbol f), we can also use MUTERM to prove termination of rewriting.
Nowadays, MUTERM 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.
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 > dcan be automatically proved terminating by using the following polynomial interpretation computed by MUTERM:
[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.
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) > Xcan be proved terminating by using the following polynomial interpretation computed by MUTERM:
[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.Xwhere 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: Luc05.
Available 

References 
[AGIL07]
Proving Termination of ContextSensitive Rewriting With
MUTERM
B. Alarcón,
R. Gutiérrez,
J. Iborra, and
S. Lucas
© Elsevier
Proc. of the
Sixth Spanish Conference on Programming and Computer Languages,
PROLE 2006
 Selected papers
Electronic Notes in Theoretical Computer Science, to appear, 2006.
Available:
Abstract
[AGL06]
ContextSensitive Dependency Pairs
B. Alarcón,
R. Gutiérrez, and
S. Lucas
© SpringerVerlag
Proc. of the
26th Conference on Foundations of Software Technology and Theoretical Computer Science,
FSTTCS'06
LNCS 4337:298309, SpringerVerlag, Berlin, 2006.
Available:
Abstract
PDF
[BLR02]
Recursive Path Orderings can be ContextSensitive
C. Borralleras,
S. Lucas, and
A. Rubio
© SpringerVerlag
Proc. of 18th International Conference on Automated Deduction, CADE'02,
LNAI 2392:314331, SpringerVerlag, Berlin, 2002.
Available:
Abstract
PDF
PostScript
BibTeX
entry.
[Bor03]
Orderingbased methods for proving termination
automatically
C. Borralleras,
PhD Thesis, Departament de Llenguagtes i Sistemes Informàtics de
la Universitat Politècnica de Catalunya, May 2003.
[FR99]
ContextSensitive ACRewriting
M.C.F. Ferreira and A.L. Ribeiro
© SpringerVerlag
Proc. of 10th International Conference on Rewriting Techniques and
Applications, RTA'99,
LNCS 1631:173181, SpringerVerlag, Berlin, 1999.
[GL02a]
Modular Termination of ContextSensitive Rewriting
B. Gramlich and
S. Lucas
© ACM Press
Proc. of 4th International Conference on Principles
and Practice of Declarative Programming, PPDP'02,
pages 5061, ACM Press 2002.
Available:
Abstract
PDF
PostScript
Slides
BibTeX
entry.
[GL02b]
Simple Termination of ContextSensitive Rewriting
B. Gramlich and
S. Lucas
© ACM Press
Proc. of 3rd ACM Sigplan Workshop on Rulebased Programming, RULE'02,
pages 2941, ACM Press, 2002.
Available:
Abstract
PDF
PostScript
Slides
BibTeX
entry.
[GM99]
Transforming ContextSensitive Rewrite Systems
J. Giesl and
A. Middeldorp
© SpringerVerlag
Proc. of 10th International Conference on Rewriting Techniques and
Applications, RTA'99,
LNCS 1631:271287, SpringerVerlag, Berlin, 1999.
Available:
Abstract
PostScript
BibTeX
entry
[GM02]
Innermost Termination of ContextSensitive Rewriting
J. Giesl and
A. Middeldorp
Technical Report AIB 200204, RWTH Aachen, 2002.
[GM03]
Innermost Termination of ContextSensitive Rewriting
J. Giesl and
A. Middeldorp
© SpringerVerlag
Proc. of 6th International Conference on Developments of Language Theory,
DLT'02,
LNCS 2450:231244, 2003.
[GM04]
Transformation Techniques for ContextSensitive Rewrite Systems
J. Giesl and
A. Middeldorp
Journal of Functional Programming, 14(4):379427, 2004.
Available:
Abstract
PDF
(preprint)
BibTeX
entry
[Luc96b]
Termination of ContextSensitive Rewriting by
Rewriting
S. Lucas
© SpringerVerlag
23rd International Colloquium on Automata, Languages and Programming,
ICALP'96,
LNCS 1099:122133, SpringerVerlag, Berlin, 1996.
Available:
Abstract
PostScript
BibTeX
entry.
[Luc98]
Contextsensitive computations in functional and functional logic
programs
S.
Lucas
Journal of Functional and Logic Programming, 1998(1):161, January
1998.
Available:
Abstract
Paper
BibTeX
entry
[Luc01a]
Termination of ondemand rewriting and termination of
OBJ programs
S. Lucas
© ACM Press
Proc. of 3rd International Conference on Principles
and Practice of Declarative Programming, PPDP'01,
pages 8293, ACM Press, 2001.
Available:
Abstract
PostScript
BibTeX
entry.
[Luc01b]
Termination of Rewriting With Strategy Annotations
S. Lucas
© SpringerVerlag
Proc. of 8th International Conference on Logic for Programming,
Artificial Intelligence and Reasoning, LPAR'01
LNAI 2250:666680, SpringerVerlag, Berlin, 2001.
Available:
Abstract
PostScript
BibTeX
entry.
Extended and revised version in [Luc03]
[Luc02]
Lazy Rewriting and ContextSensitive Rewriting
S. Lucas
© Elsevier
International Workshop on Functional and (Constraint) Logic Programming,
WFLP 2001 (selected papers)
Electronic
Notes in Theoretical Computer Science, volume 64, 2002.
Available:
Abstract
PDF
PostScript
BibTeX
entry.
[Luc03]
Termination of programs with strategy annotations
S. Lucas
Technical Report DSIC II/20/03, 47 pages.
Departamento de Sistemas Informáticos y Computación, UPV,
September 2003.
Available:
Abstract
PDF
PostScript
BibTeX
entry.
[Luc04a]
MUTERM: A Tool for Proving Termination of ContextSensitive Rewriting
S. Lucas
© SpringerVerlag
Proc. of 15th International Conference on Rewriting Techniques and
Applications, RTA'04,
LNCS 3091:200209, SpringerVerlag, Berlin, 2004.
Available:
Abstract
PDF
PostScript
[Luc04b]
Polynomials for Proving Termination of ContextSensitive
Rewriting
S. Lucas
© SpringerVerlag
Proc. of 7th International Conference on
Foundations of Software Science and Computation Structures,
FOSSACS'04,
LNCS 2987:318332, 2004.
Available:
Abstract
PDF
PostScript
BibTeX entry
[Luc05]
Polynomials over the reals in proofs of termination: from
theory to practice
S. Lucas
©
EDP Sciences
RAIRO Theoretical Informatics and Applications,
39(3):547586, July 2005.
Available:
Abstract
PDF
[Zan97]
Termination of ContextSensitive Rewriting
H. Zantema
© SpringerVerlag
Proc. of 8th International Conference on Rewriting Techniques and
Applications, RTA'97,
LNCS 1232:172186, SpringerVerlag, Berlin, 1997.
Contact 
Please, report any bug, comment, or suggestion to: slucas@dsic.upv.es