Restrictions of rewriting can eventually achieve termination by pruning all infinite rewrite sequences issued from every term. However, proving that 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.
Example 1. Consider the TRS from Example 6 in [Luc98]:first(0,X) > nil 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.
Formats
We provide differents formats to specify the rules and the associated replacement map μ.
TPDB Format
Termination of CSR is one of the subcategories of termination of rewriting which is included in the termination problem data base (TPDB). It is possible to specify a term rewriting system with contextsensitive replacement restrictions (given by a replacement map) by using the TPDB format:
spec ::= (decl) spec  e
decl ::= VAR idlist  THEORY listofthdecl  RULES listofrules
 STRATEGY strategydecl  id anylist
anylist ::= e  id anylist  string anylist
 (anylist) anylist  , anylist
idlist ::= e  id idlist
listofthdecl ::= e  (thdecl) listofthdecl
thdecl ::= id idlist  EQUATIONS eqlist
eqlist ::= e  equation eqlist
equation ::= term == term
listofrules ::= e  rule listofrules
rule ::= term > term  term > term  condlist
 term >= term  term >= term  condlist
condlist ::= cond  cond, condlist
cond ::= term > term  term >< term
term ::= id  id ( )  id (termlist)
termlist ::= term  term, termlist
strategydecl ::= INNERMOST  OUTERMOST  CONTEXTSENSITIVE csstratlist
csstratlist ::= e  (id intlist) csstratlist
intlist ::= e  int intlist
where
id
are nonempty sequences of characters except space,'('
,')'
,'"'
and','
, and excluding special sequences'>'
,'=='
,'>='
,'><'
,''
and keywordsCONTEXTSENSITIVE
,EQUATIONS
,INNERMOST
,OUTERMOST
,RULES
,STRATEGY
,THEORY
andVAR
;string
are sequences of any characters between double quotes; andint
are nonempty sequences of digits.
Moreover, at least one VAR
and one RULES
sections are mandatory. If they are several, the union is taken and:
 a symbol declared in a
VAR
section must not have been used in previous declarations, and is assumed to denote a variable in remaining declarations (in particular must not be applied to arguments),  a symbol occuring in a
RULES
section which has not been used before is assumed to denote a function symbol, and must be used afterwards always with the same arity.
OBJ/Maude Format
It provides a more compact description as an OBJ module (which is also compatible with the Maude syntax). Here, the replacement map is described by means of strategy annotations (i_{1}…i_{n} 0) associated to each symbol; this means that μ(f) = {i_{1},…,i_{n}}, if the arity of f is k. (see [Luc03]). Symbols f without any strategy OBJ module have no replacement restriction, i.e., μ(f) = {1,…,k}.
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. With MUTERM 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 ContextSensitive 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 ContextSensitive 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 pair framework, etc.).
Example 2. The TRS R and replacement map μ in Example 1 can be specified by the following TPDB module:(VAR X Y Z) You can also do it as an OBJ module: obj Ex6_Luc98 is op first : S S > S . vars X Y Z : S . eq first(0,X) = nil . endo

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:
 Direct methods, i.e., orderings
>
on terms which can be used to directly compare the lefthand sides and righthand sides of the rules in order to conclude the μtermination of the TRS, see [BLR02, Bor03, GL02b, Luc04b, Zan97]. MUTERM implements the techniques described in [BLR02] (CSRPO) and [Luc04b, Luc05] (polynomial orderings).  Contextsensitive dependency pairs: We have also adapted Arts and Giesl’s dependency pairs method [AG00] to CSR leading to a contextsensitive dependency pairs approach [AGL06]. MUTERM implements all techniques described in [AGL06].
 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, Luc96, Zan97]. Our tool, MUTERM, implements these transformations using a common environment that eases their combination and comparison.
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:
Example 3. The termination of lazy rewriting for the following module:obj Ex1_2_Luc02c is op 2nd : S > S . vars X Y Z : S . eq 2nd(cons(X,cons(Y,Z))) = Y . endo

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.
Example 4. The following TRS Rf(X) > u1(X,X)

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 5. For example, μtermination of Ex1_2_Luc02c_LR in Example 3 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 can be proved terminating by using the following polynomial interpretation computed by MUTERM: [2nd](X) = 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: [Luc05].
Termination of OrderSorted Rewriting with MUTERM
Ordersorted TRSs (OSTRSs) are TRSs together with a set of sorts S which comes with a subsort ordering, which is interpreted in the models as set inclusion. Furthermore, the arguments of function symbols have sorts and can be subsort overloaded, like
+ : Nat Nat > Nat
+ : Int Int > Int
where Nat < Int
, supporting socalled subtype polymorphism. Since Maude provides an appropriate (selfexplanatory) notation for OSTRSs, the OSTRSs that MUTERM accepts are presented as Maude modules.
Example 6. The following example computes the factorial of a number. It is ordersorted terminating, but if you remove the sorts then the system is nonterminating.fmod Factorial is op 0 : > Nat . vars x y : Nat . eq x + 0 = x . endfm 
References
[AEF+08]  B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, R. Gutiérrez, S. Lucas, P. SchneiderKamp, and R. Thiemann. Improving ContextSensitive Dependency Pairs. In I. Cervesato, H. Veith, and A. Voronkov, editors, Proc. of 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR’08, volume 2250 of Lecture Notes in Artificial Intelligence, pages 636–651, 2008. SpringerVerlag, Berlin. Available: here. 
[AG00]  T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Compututer Science, 236(12):133–178, 2000. Available: here. 
[AGIL07]  B. Alarcón, R. Gutiérrez, J. Iborra, and S. Lucas. Proving Termination of ContextSensitive Rewriting with MUTERM. Electronic Notes in Theoretical Computer Science, 188:105–115, 2007. Available: here. 
[AGL06]  B. Alarcón, R. Gutiérrez, and S. Lucas. Contextsensitive dependency pairs. In S. ArunKumar and N. Garg, editors, Proc. of 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, FST&TCS’06, volume 4337 of Lecture Notes in Computer Science, pages 297–308, Kolkata, India, 2006. SpringerVerlag. Available: here. 
[AGL10]  B. Alarcón, R. Gutiérrez, and S. Lucas. Contextsensitive dependency pairs. Information and Computation, 208:922968, 2010. Elsevier. Available: here. 
[AGLNM10]  B. Alarcón, R. Gutiérrez, S. Lucas, and R. Navarro Marset. Proving Termination Properties with MUTERM. In M. Johnson and D. Pavlovic, editors, Proc. of the 13th International Conference on Algebraic Methodology And Software Technology, AMAST10, volume 6486 of Lecture Notes in Computer Science, pages 201–208, 2011. SpringerVerlag. Available: here. 
[AL07]  B. Alarcón, and S. Lucas. Termination of Innermost ContextSensitive Rewriting Using Dependency Pairs. In Proc. of the 6th International Symposium on Frontiers of Combining Systems, FroCoS’07, volume 4720 of Lecture Notes in Computer Science, pages 73–87, 2007. SpringerVerlag. Available: here. 
[AL08]  B. Alarcón, and S. Lucas. Using ContextSensitive Rewriting for Proving Innermost Termination of Rewriting. Electronic Notes in Theoretical Computer Science, 248:3–17, 2008. Available: here. 
[ALNM09]  B. Alarcón, S. Lucas, and R. Navarro Marset. Using Matrix Interpretations over the Reals in Proofs of Termination. In Proc. of the 9th Jornadas sobre Programación y Lenguajes, pages 255–264, 2009. Available: PDF. 
[ALM10]  B. Alarcón, S. Lucas, and J. Meseguer. A Dependency Pair Framework for AvCTermination. In P. Ölveczky, editor, Proc. of the 8th International Workshop on Rewriting Logic and its Applications, WRLA’10, volume 6381 of Lecture Notes in Computer Science, pages 36–52, 2010. SpringerVerlag. Available: here. 
[BLNM+09]  C. Borralleras, S. Lucas, E. Rodríguez Carbonell, and A. Rubio. Solving nonlinear polynomial arithmetic via SAT modulo linear arithmetic. In Proc. of 22th International Conference on Automated Deduction, CADE’09, volume 5663 of Lecture Notes in Artificial Intelligence, pages 294–305, 2009. SpringerVerlag. Available: here. 
[BLO+12]  C. Borralleras, S. Lucas, A. Oliveras, E. Rodríguez Carbonell, and A. Rubio. SAT modulo linear arithmetic for Solving Polynomial Constraints. Journal of Functional Programming, 14:329–427, 2004. Available: here. 
[BLR02]  C. Borralleras, S. Lucas, and A. Rubio. Recursive path orderings can be contextsensitive. In A. Voronkov, editor, Proc. of 18th International Conference on Automated Deduction, CADE’02, volume 2392 of Lecture Notes in Artificial Intelligence, pages 314–331, Copenhagen, Denmark, June 2002. SpringerVerlag, Berlin. Available: here. 
[Bor03]  C. Borralleras. Orderingbased methods for proving termination automatically. PhD thesis, Departament de Llenguagtes i Sistemes Informàtics de la Universitat Politècnica de Catalunya, May 2003. 
[FR99]  Maria C. F. Ferreira and A. L. Ribeiro. ContextSensitive ACrewriting. In Proc. of the 10th International Conference on Rewriting Techniques and Applications, RTA’99, pages 286–300, London, UK, 1999. SpringerVerlag. Available here 
[FNMO+08]  C. Fuhs, R. Navarro Marset, C. Otto, J. Giesl, S. Lucas, and P. SchneiderKamp. Search Techniques for Rational Polynomial Orders. In Proc. of 9th International Conference on Artificial Intelligence and Symbolic Computation, AISC’08, volume 5144 of Lecture Notes in Artificial Intelligence, pages 109–124, 2008. SpringerVerlag, Berlin. Available: here. 
[GL02a]  B. Gramlich and S. Lucas. Modular Termination of ContextSensitive Rewriting. In C. Kirchner, editor, Proc. of 4th ACM Sigplan Conference on Principles and Practice of Declarative Programming, PPDP’02, pages 50–61, Pittsburgh, USA, October 2002. ACM Press, New York. Available: here. 
[GL02b]  B. Gramlich and S. Lucas. Simple Termination of ContextSensitive Rewriting. In B. Fischer and E. Visser, editors, Proc. of 3rd ACM Sigplan Workshop on RuleBased Programming, RULE’02, pages 29–41, Pittsburgh, USA, October 2002. ACM Press, New York. Available: here. 
[GM02]  J. Giesl and A. Middeldorp. Innermost Termination of Contextsensitive Rewriting. Technical Report AIB 200204, RWTH Aachen, 2002. 
[GM03]  J. Giesl and A. Middeldorp. Innermost Termination of ContextSensitive Rewriting. In Proc. of 6th International Conference on Developments of Language Theory, DLT’02. SpringerVerlag, 2003. Available: here 
[GM04]  J. Giesl and A. Middeldorp. Transformation Techniques for ContextSensitive Rewrite Systems. Journal of Functional Programming, 14:329–427, 2004. Available: here. 
[GL10]  R. Gutiérrez, and S. Lucas. Proving Termination in the ContextSenstive Dependency Pair Framework. In P. Ölveczky, editor, Proc, of the 8th International Workshop on Rewriting Logic and its Applications, WRLA’10, volume 6381 of Lecture Notes in Computer Science, pages 19–35, 2010. SpringerVerlag. Available: here. 
[GLU08]  R. Gutiérrez, S. Lucas, and X. Urbain. Usable Rules for ContextSensitive Rewrite Systems. In A. Voronkov, editor, Proc. of the 19th International Conference on Rewriting Techniques and Applications, RTA’08, volume 5117 of Lecture Notes in Computer Science, pages 126–141, 2008. SpringerVerlag. Available: here. 
[LM08]  S. Lucas, and J. Meseguer. OrderSorted Dependency Pairs. In S. Antoy and E. Albert, editors, Proc. of the 10th International ACM SIGPLAN conference on Principles and Practice of Declarative Programming, PPDP’08, pages 108–119, 2008. ACM Press. Available: here. 
[Luc96]  S. Lucas. Termination of ContextSensitive Rewriting by Rewriting. In F. Meyer auf der Heide and B. Monien, editors, Proc. ofthe 23rd International Colloquium on Automata, Languages, and Programming, ICALP’96, volume 1099 of Lecture Notes in Computer Science, pages 122–133. SpringerVerlag, Berlin, 1996. Available: here. 
[Luc98]  S. Lucas. ContextSensitive Computations in Functional and Functional Logic Programs. Journal of Functional and Logic Programming, 1998(1), January 1998. Available: here. 
[Luc01a]  S. Lucas. Termination of OnDemand Rewriting and Termination of OBJ Programs. In H. Sondergaard, editor, Proc. of 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP’01, pages 82–93, Firenze, Italy, September 2001. ACM Press, New York. Available: here. 
[Luc01b]  S. Lucas. Termination of Rewriting with Strategy Annotations. In A. Voronkov and R. Nieuwenhuis, editors, Proc. of 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR’01, volume 2250 of Lecture Notes in Artificial Intelligence, pages 669–684, La Habana, Cuba, December 2001. SpringerVerlag, Berlin. Available: here. Extended and revised version in [Luc03] 
[Luc02]  S. Lucas. Lazy Rewriting and ContextSensitive Rewriting. International Workshop on Functional and (Constraint) Logic Programming, WFLP 2001, Selected Papers, volume 64 of Electronic Notes in Theoretical Computer Science, pages 234–254, September 2002. Available: here. 
[Luc03]  S. Lucas. Termination of Programs with Strategy Annotations. Technical Report DSICII/20/03, DSIC, Universitat Politècnica de València, September 2003. Available: here. 
[Luc04a]  S. Lucas. MUTERM: A Tool for Proving Termination of ContextSensitive Rewriting. In Proc. of the 15th International Conference on Rewriting Techniques and Applications, RTA’04, pages 200–209, 2004. Available: here. 
[Luc04b]  S. Lucas. Polynomials for Proving Termination of ContextSensitive Rewriting. In I. Walukiewicz, editor, 7th International Conference on Foundations of Software Science and Computation Structures, FOSSACS’04, volume 2987 of Lecture Notes in Computer Science, pages 318–332, Barcelona, Spain, April 2004. SpringerVerlag. Available: here. 
[Luc05]  S. Lucas. Polynomials over the Reals in Proofs of Termination: from Theory to Practice. RAIRO Theoretical Informatics and Applications, 39(3):547586, July 2005. Available: here. 
[Luc06]  S. Lucas. Proving Termination of ContextSensitive Rewriting by Transformation. Information and Computation, 204(12):17821846, 2008. Elsevier. Available: here. 
[Luc07]  S. Lucas. Practical Use of Polynomials over the Reals in Proofs of Termination. In Proc. of 9th ACM Sigplan Conference on Principles and Practice of Declarative Programming, PPDP’07, pages 39–50, 2007. ACM Press, New York. Available: here. 
[Zan97]  H. Zantema. Termination of ContextSensitive Rewriting. In Proc. of 8th International Conference on Rewriting Techniques and Applications, RTA’97. SpringerVerlag, 1997. Available: here. 