Documentation

| -> Formats
| -> Structure and Functionality
| -> Termination of CSR
| -> Innermost Termination and Innermost CSR Termination
| -> AvC-Termination
| -> Termination and Operational Termination of Conditional Term Rewriting
| -> Termination of rewriting
| -> Termination of Order-Sorted Rewriting
| -> References

MU-TERM [GL20] is a tool which can be used to verify a number of termination properties of variants
of rewrite systems. MU-TERM follows a logic-based approach to modeling rewriting computations. This makes the treatment of termination problems for existing variants of rewriting easier to deal with. This is combined with the development of specific extensions and
generalizations of the dependency pair framework for treating each variant of rewriting.

For example, 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 [Luc01aLuc01bLuc03]. 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
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.

Formats

We provide different formats to specify the rules and the associated replacement map μ.

Extended TPDB Format

The termination problem data base (TPDB) format is used to specify variants of term rewriting system and strategies. You can add context-sensitive replacement restrictions, equations, conditional rules, etc. by using the TPDB format. We extended the original TPDB format with some extra keywords in order to deal with all MU-TERM capabilities (marked in blue):

spec ::= (decl) spec | e
decl ::= VAR idlist | THEORY listofthdecl | RULES listofrules
| STRATEGY strategydecl | id anylist | CHECK-TERMINATION
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 non-empty sequences of characters except space, '(', ')', '"' and ',', and excluding special sequences '->', '==', '->=', '-><-', '|' and keywords;
  • string are sequences of any characters between double quotes; and
  • int are non-empty 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

Although we cannot prove OBJ/Maude termination with all its features, we allow to describe TPDB problems using OBJ/Maude syntax, providing a more compact description. Furthermore, we can prove order-sorted termination (without conditional rules).

Structure and Functionality

MU-TERM 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 MU-TERM you can:

  • Load a TRSs, extract the corresponding signature, and associate features.
  • Modify the TRS and features of the loaded TRS.
  • Prove termination/innermost termination/context-sensitive termination/innermost context-senstive termination/operational termination for the corresponding rewriting system R using variants of the DP framework.
Example 2. The TRS R and replacement map μ in Example 1 can be specified by the following TPDB module:

(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))) .


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

We refer to [AGIL07Luc04a] for further details.

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 [BLR02Bor03, GL02bLuc04bZan97]. MU-TERM implements the techniques described in [BLR02] (CS-RPO) and [Luc04bLuc05] (polynomial orderings).
  • Context-sensitive dependency pairs: We have also adapted Arts and Giesl’s dependency pairs method [AG00] to CSR leading to a context-sensitive dependency pairs approach [AGL06]. MU-TERM 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 [FR99GM04Luc96Zan97]. Our tool, MU-TERM, implements these transformations using a common environment that eases their combination and comparison.

Examples of CS-TRSs and the corresponding termination proofs by using these techniques can be found here.

Innermost Termination and Innermost CSR Termination with MU-TERM

If you want to prove innermost termination instead of termination you can add the corresponding strategy tag (STRATEGY INNERMOST) in the TPDB input. Termination of OBJ/Maude is innermost by default.

AvC-Termination with MU-TERM

In [ALM10], termination of rewriting using A, C and/or AC axioms is proved using the AvC-DP Framework:

Example 3. The following AvC-TRS:

(VAR x y)
(THEORY
(AC plus))
(RULES
plus(x,0) -> x
plus(x,s(y)) -> s(plus(x,y))
)
can be proved terminating using MU-TERM.

Termination and Operational Termination of Conditional Term Rewriting with MU-TERM

In [LMG18,LMG20], termination and operational termination is proved by using the 2D DP Framework:

Example 3. The following CTRS:

(VAR x)
(RULES
c -> b
d -> b
f(a,x) -> c | x -> a
f(x,x) -> d | x -> a
g(x) -> d | g(x) -> b
g(a) -> f(a,a)
)

can be proved operational non-terminating, but also terminating using MU-TERM. If the CTRS in TPDB format is uploaded, the “Prove automatically” button can be used to prove or disprove operational termination. If the extended TPDB tag (CHECK-TERMINATION) is added (e.g., just before the TPDB encoding of the CTRS), then a termination proof is attempted instead.

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.

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 4. 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 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
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: [Luc05].

Termination of Order-Sorted Rewriting with MU-TERM

Order-sorted TRSs (OS-TRSs) 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 so-called subtype polymorphism. Since Maude provides an appropriate (self-explanatory) notation for OS-TRSs, the OS-TRSs that MU-TERM accepts are presented as Maude modules.

Example 6. The following example computes the factorial of a number. It is order-sorted terminating, but if you remove the sorts then the system is non-terminating.

fmod Factorial is
sorts Nat NzNat .
subsorts NzNat < Nat .

op 0 : -> Nat .
op s : Nat -> NzNat .
op p : NzNat -> Nat .
op _+_ : Nat Nat -> Nat .
op _+_ : NzNat Nat -> NzNat .
op _+_ : NzNat NzNat -> NzNat .
op _*_ : Nat Nat -> Nat .
op _*_ : NzNat NzNat -> NzNat .
op fact : Nat -> NzNat .

vars x y : Nat .
vars x' : NzNat .

eq x + 0 = x .
eq x + s(y) = s(x + y) .
eq x * 0 = 0 .
eq x * s(y) = x + (x * y) .
eq fact(0) = s(0) .
eq fact(x') = x' * fact(p(x')) .
eq p(s(x)) = x .


endfm

References

[AEF+08] B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, R. Gutiérrez, S. Lucas, P. Schneider-Kamp, and R. Thiemann. Improving Context-Sensitive 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. Springer-Verlag, Berlin.
Available: here.
[AG00] T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Compututer Science, 236(1-2):133–178, 2000.
Available: here.
[AGIL07] B. Alarcón, R. Gutiérrez, J. Iborra, and S. Lucas. Proving Termination of Context-Sensitive Rewriting with MU-TERM. Electronic Notes in Theoretical Computer Science, 188:105–115, 2007.
Available: here.
[AGL06] B. Alarcón, R. Gutiérrez, and S. Lucas. Context-sensitive dependency pairs. In S. Arun-Kumar 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. Springer-Verlag.
Available: here.
[AGL10] B. Alarcón, R. Gutiérrez, and S. Lucas. Context-sensitive dependency pairs. Information and Computation, 208:922-968, 2010. Elsevier.
Available: here.
[AGLNM10] B. Alarcón, R. Gutiérrez, S. Lucas, and R. Navarro Marset. Proving Termination Properties with MU-TERM. 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. Springer-Verlag.
Available: here.
[AL07] B. Alarcón, and S. Lucas. Termination of Innermost Context-Sensitive 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. Springer-Verlag.
Available: here.
[AL08] B. Alarcón, and S. Lucas. Using Context-Sensitive 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 AvC-Termination. 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. Springer-Verlag.
Available: here.
[BLNM+09] C. Borralleras, S. Lucas, E. Rodríguez Carbonell, and A. Rubio. Solving non-linear 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. Springer-Verlag.
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 context-sensitive. 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. Springer-Verlag, Berlin.
Available: here.
[Bor03] C. Borralleras. Ordering-based 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. Context-Sensitive AC-rewriting. In Proc. of the 10th International Conference on Rewriting Techniques and Applications, RTA’99, pages 286–300, London, UK,
1999. Springer-Verlag.
Available here
[FNMO+08] C. Fuhs, R. Navarro Marset, C. Otto, J. Giesl, S. Lucas, and P. Schneider-Kamp. 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. Springer-Verlag, Berlin.
Available: here.
[GL02a] B. Gramlich and S. Lucas. Modular Termination of Context-Sensitive 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 Context-Sensitive Rewriting. In B. Fischer and E. Visser, editors, Proc. of 3rd ACM Sigplan Workshop on Rule-Based 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 2002-04, RWTH Aachen, 2002.
[GM03] J. Giesl and A. Middeldorp. Innermost Termination of Context-Sensitive Rewriting. In Proc. of 6th International Conference on Developments of Language Theory, DLT’02. Springer-Verlag, 2003.
Available: here
[GM04] J. Giesl and A. Middeldorp. Transformation Techniques for Context-Sensitive Rewrite Systems. Journal of Functional Programming, 14:329–427, 2004.
Available: here.
[GL10] R. Gutiérrez, and S. Lucas. Proving Termination in the Context-Senstive 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. Springer-Verlag.
Available: here.
[GL20] R. Gutiérrez, and S. Lucas. MU-TERM: Verify Termination Properties Automatically (System Description). In: Peltier N., Sofronie-Stokkermans V. (eds) Automated Reasoning. IJCAR 2020. LNCS, vol 12167.Springer-Verlag.
Available: here.
[GLU08] R. Gutiérrez, S. Lucas, and X. Urbain. Usable Rules for Context-Sensitive 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. Springer-Verlag.
Available: here.
[LMG18] S. Lucas, J. Meseguer and R. Gutiérrez. The 2D Dependency Pair Framework for conditional rewrite systems. Part I: Definition and basic processors. Journal of Computer and System Sciences 96: 74-106 (2018)
Available: here.
[LMG20] S. Lucas, J. Meseguer and R. Gutiérrez. The 2D Dependency Pair Framework for Conditional Rewrite Systems – Part II: Advanced Processors and Implementation Techniques. Journal of Automated Reasoning 64(8): 1611-1662 (2020)
Available: here.
[LM08] S. Lucas, and J. Meseguer. Order-Sorted 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 Context-Sensitive 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. Springer-Verlag, Berlin, 1996.
Available: here.
[Luc98] S. Lucas. Context-Sensitive Computations in Functional and Functional Logic Programs. Journal of Functional and Logic Programming, 1998(1), January 1998.
Available: here.
[Luc01a] S. Lucas. Termination of On-Demand 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. Springer-Verlag, Berlin.
Available: here.
Extended and revised version in [Luc03]
[Luc02] S. Lucas. Lazy Rewriting and Context-Sensitive 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 DSIC-II/20/03, DSIC, Universitat Politècnica de
València, September 2003.
Available: here.
[Luc04a] S. Lucas. MU-TERM: A Tool for Proving Termination of Context-Sensitive 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 Context-Sensitive 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. Springer-Verlag.
Available: here.
[Luc05] S. Lucas. Polynomials over the Reals in Proofs of Termination: from Theory to Practice. RAIRO Theoretical Informatics and Applications, 39(3):547-586, July 2005.
Available: here.
[Luc06] S. Lucas. Proving Termination of Context-Sensitive Rewriting by Transformation. Information and Computation, 204(12):1782-1846, 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 Context-Sensitive Rewriting. In Proc. of 8th International Conference on Rewriting Techniques and Applications, RTA’97. Springer-Verlag, 1997.
Available: here.