The CiME Rewrite Tool

CiME is a jemstic scientific project at LRI, supported by the STIC department of the CNRS. Inside this project is developed a computer toolbox called CiME2. CiME2 is not developed anymore, its successor CiME 3 is developed by ANR project A3PAT and available there

The CiME 1.x system
The CiME 2.0 system
The CiME 3 system
Examples of use
Known bugs

The CiME 1.x system

This version is no longer being maintained. Since version 2 does not cover yet all features of the version 1, the old distribution is still available here.

The CiME 2.0 system

CiME 2.0 is an entrant of CASC 18 competition. This version is used by the system TALP for proving termination of logic programs.

You will find the following features:

An interactive toplevel to allow naming of objects and call to various functions.
Solving Diophantine constraints over finite intervals
Solving Presburger constraints
String Rewriting Systems, KB completion.
Term Rewrite Systems, possibly with commutative or associative-commutative symbols.
Termination of TRSs using standard or dependency pairs criteria, automatic generation of termination orderings based on polynomial interpretations, including weak orderings for dependency pairs criteria.
Parameterized String Rewriting Systems confluence checking
TRS confluence checking, KB completion, modulo AC when needed

The CiME 2.02 distribution

Don't hesitate to send a mail to Claude.Marche@lri.fr if you have any questions, remarks or suggestions.

Documentation

Far from complete, see also the examples to know the set of functions available.

On-line in HTML
As a bunch of HTML files, by HTTP or by FTP
In Postscript, by HTTP or by FTP

Binaries

Available for the following architectures:

For pentium PCs running Linux: by HTTP or by FTP (uncompress using bzip2 -d ...)
For pentium PCs running Linux, statically linked binary: by HTTP or by FTP
For pentium PCs running MS Windows: by HTTP or by FTP
For Mac OS X: by HTTP or by FTP

Sources

by HTTP or by FTP.
Also available by read-only anynomous CVS. Proceed as follows :
- Log anonymously on our CVS server by
```
cvs -d :pserver:guest@cvs.lri.fr:/users/demons/demons/master-sources-repository login
```
  and leave the password empty.
- check out the source tree by
```
cvs -d :pserver:guest@cvs.lri.fr:/users/demons/demons/master-sources-repository co cime
```
- the installation procedure is (see file INSTALL for more details)
```
cd cime
autoconf
./configure
make 
```
- Later on, you may update your source tree by
```
cd cime
cvs update -d
```
  and recompile again

Examples

By HTTP or by FTP

More recent versions of the examples may be available in the CVS archive.

Examples of use

Parameterized String rewriting system

This example shows how to prove that a parameterized string rewriting system is locally confluent.

CiME> let N = parameters "N";
N : parameter_set = "N "
CiME> let S = pword_signature N "s | {N>=2}; r | {N>=2}" ;
S : pword_signature = 
CiME> let R = psrs S "s s -> | {N>=2};
                s r -> r^{N-1} s | {N>=2} ;
                r^{N} -> | {N>=2};"
        ;
R : S psrs = { [] s s  -> | { N - 2 >= 0} ;
               [] s r  -> ( r )^{ N - 1} s | { N - 2 >= 0} ;
               [] ( r )^{ N}  -> | { N - 2 >= 0} ; } <3 rules>
CiME> let Rnorm = psrs S "s r^{k} -> r^{N-k} s | {N>=2 /\ 1 <= k <= N-1 };";
Rnorm : S psrs = { [k ] s ( r )^{ k}  -> ( r )^{ N - k} s |
                   { (N - 2 >= 0 and k - 1 >= 0 and N - k - 1 >= 0)} ;
                   } <1 rules>
CiME> pconfluent_ext R Rnorm;
Computing CP.
Found 17 CP.
- : bool = true

String rewriting system

CiME> let S = word_signature "a b c";
S : word_signature = 
CiME> let R = SRS S " a b -> c ; b c -> a";
R : S SRS = { a b -> c,
              b c -> a } (2 rules)
CiME> let prec = word_precedence S " a > b >c ";
prec : S word_precedence = 
CiME> let ord = length_lex prec;
ord : S word_ordering = 
CiME> let R' = word_completion ord R;
R' : S SRS = { a b -> c,
              b c -> a,
              a^2 -> c^2,
              c^2 b -> a c,
              a c^2 -> c^2 a,
              a c b -> b a c } (6 rules)
CiME> word_normalize R' (word S "a b c b c a b");
- : S word = a^3 c

Termination

Here is a first example that uses the standard termination criterion (find a reduction ordering w.r.t which the rules are strictly decreasing)

CiME> let F = signature "0 : constant; s : unary; m,p : binary; ";
F : signature
CiME> let X = vars "x y z";
X : variable set
CiME> let R = TRS F X "
p(x,0) -> x; p(x,s(y)) -> s(p(x,y));
m(x,0) -> 0; m(x,s(y)) -> p(m(x,y),x); ";
R : TRS = { p(x,0) -> x,
            p(x,s(y)) -> s(p(x,y)),
            m(x,0) -> 0,
            m(x,s(y)) -> p(m(x,y),x) } (4 rules)
CiME> #time;
time is now on
CiME> termination R;
Entering the termination expert. Verbose level = 0
[0] = 0;
[s](X0) = 1*X0 + 1;
[m](X0,X1) = 2*X0*X1 + 2*X1 + 1*X0 + 1;
[p](X0,X1) = 2*X1 + 1*X0 + 1;
Execution time: 0.21 sec.
- : unit = ()
CiME>

Here is a second example that uses the dependency pair termination criterion

CiME> let F = signature "
  0 : constant;
  s : unary;
  minus : binary;
  quot : binary;
";
F : signature
CiME> let X =vars "x y";
X : variable set
CiME> let quotient = TRS F X "
  minus(x,0) -> x ;
  minus(s(x),s(y)) -> minus(x,y) ;
  quot(0,s(y)) -> 0 ;
  quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) ;
";
quotient : TRS = { minus(x,0) -> x,
                   minus(s(x),s(y)) -> minus(x,y),
                   quot(0,s(y)) -> 0,
                   quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) } (4
  rules)
CiME> termcrit "dp";
Termination now uses dependency pair criterion
- : unit = ()
CiME> #time on;
time is now on
CiME> termination quotient;
Entering the termination expert. Verbose level = 0
[0] = 0;
[s](X0) = 1*X0 + 1;
[minus](X0,X1) = 1*X0;
[quot](X0,X1) = 1*X0*X1;
['minus`](X0,X1) = 1*X0*X1;
['quot`](X0,X1) = 1*X0*X1;

Termination proof found.
Execution time: 1.3 sec.
- : unit = ()
CiME>

Known bugs

Since version alpha4, the Diophantine constraint solver seems to be significantly slower in some cases. Not recovered, may be it was a bug of previous versions...

25/6/2009 (formatté avec yamlpp).