Single Rewrite Systems

A single TRS is inputted by typing the rules into the upper left text area or by uploading a file via the browse button. The size of the TRS may not exceed 10K. In the latter case, the file name must match the pattern [a-zA-Z0-9][.a-zA-Z0-9_]*.trs.

A TRS is presented as a sequence of rewrite rules, separated by semi-colons. Rewrite rules are pairs of terms, separated by "->".

Terms are built from variables and function symbols, using commas and parentheses (and spaces). Variables and function symbols must start with a lowercase letter and may contain uppercase letters, digits, underscores, and the sharp "#" and single quote "'" characters. To distinguish variables from constants, the latter must be followed by "()". Alternatively, a list of variables (like [m,n,x,y]) may be given before the sequence of rewrite rules. In addition, numbers as well as the string "[]" (both without "()") are treated as constants. We also allow binary infix operators that consist of one or more of the characters "+", "-", "*", ":", ".", "/", "\", "=", "|", "@", "<" and ">".

TRSs may also be inputted in the official format of the Termination Problems Data Base.

Examples

The following rules for computing disjunctive normal forms adhere to the above syntax:

  not(not(x)) -> x;
  not(x \/ y) -> not(x) /\ not(y);
  not(x /\ y) -> not(x) \/ not(y);
x /\ (y \/ z) -> (x /\ y) \/ (x /\ z);
(y \/ z) /\ x -> (x /\ y) \/ (x /\ z)
Here is another example:
      [] @ y -> y                    ;
   (n:x) @ y -> n:(x @ y)            ;
   0 <= y    -> true()               ;
s(x) <= 0    -> false()              ;
s(x) <= s(y) -> x <= y               ;
  low(n,[])  -> []                   ;
  low(n,m:x) -> ifLow(m<=n,n,m:x)    ;
 high(n,[])  -> []                   ;
 high(n,m:x) -> ifHigh(m<=n,n,m:x)   ;
ifLow(true(),n,m:x)   -> m:low(n,x)  ;
ifLow(false(),n,m:x)  -> low(n,x)    ;
ifHigh(true(),n,m:x)  -> high(n,x)   ;
ifHigh(false(),n,m:x) -> m:high(n,x) ;
quicksort([])  -> []                 ;
quicksort(n:x) -> quicksort(low(n,x)) @ (n:quicksort(high(n,x)))

Multiple Rewrite Systems

A collection of TRSs can be given as input to TTT by uploading a zip archive. The name of the archive must match [a-zA-Z0-9][a-zA-Z0-9_]*.zip and its size may not exceed 100K. All files matching [a-zA-Z0-9][.a-zA-Z0-9_]*.trs are extracted from the archive and the termination prover runs on each of these files in turn.

Simply-Typed Applicative Rewrite Systems

In addition to ordinary first-order rewrite systems as described above, TTT can handle simply-typed applicative rewrite systems introduced by Aoto and Yamada. A typical example is
TYPES
0    : N                  ;
s    : N => N             ;
id   : N => N             ;
add  : N => N => N        ;
map  : (N => N) => L => L ;
nil  : L                  ;
cons : N => L => L        
 
RULES
id x              -> x           ;
add 0             -> id          ;
add (s x) y       -> s (add x y) ;
map f nil         -> nil         ;
map f (cons x xs) -> cons (f x) (map f xs)