The CiME system
Version 3.02

Evelyne Contejean, Pierre Courtieu , Julien Forest, Olivier Pons and Xavier Urbain
CNRS-LRI-Universite Paris Sud XI
Cedric-CNAM-ENSIIE

Chapter 1  Tutorial

This chapter is a small tutorial, to present the basic features of CiME in a progressive way.

1.1  The toplevel language

1.1.1  Expressions

The toplevel language is a simple language which allows the user to type-in expressions terminated by a semi-colon, and let CiME evaluate them. Simple expressions are built with integers, booleans and strings, and operations on them:

CiME>12;
 - : int = 12
CiME>"hello world";   
 - : string = "hello world"
CiME>true;
 - : bool = true
CiME>1+2;
 - : int = 3
CiME>3*4-1;
 - : int = 11
CiME>-4*(3-2)+1;
 - : int = -3
CiME>4*4 < 5 or 6 <> 3+1;
 - : bool = true
CiME>true and not false or true;
 - : bool = true

Notice that for each expression, CiME starts with computing its type. In case of typing error, an error message is displayed and no evaluation is performed:

CiME>1+true;
 Typing error: bad type argument in application

1.1.2  Definitions with let

It is possible to give a name to the result of an evaluation, for further use in following expressions:

CiME>let x = 4*5;
 x : int = 20
CiME>x*x-1;
 - : int = 399
CiME>x > 10;
 - : bool = true

An attempt to use an undefined name results in a typing error:

CiME>y+1;
 Typing error: undefined identifier y

Notice that it is allowed to redefine a name:

CiME>let x=1; 
 x : int = 1
CiME>x+3;
 - : int = 4
CiME>let x=2;
 x : int = 2
CiME>x+3;
 - : int = 5

Further note that the second let does not behave like an assignment like in traditional imperative programming languages, but it is a new definition hiding to previous one, like in functional languages. (More precisely, it follows the static binding semantics, see Section ??.)

1.1.3  Definitions of functions

The core language allows the definition of functions, with a let fun construct. Application is denoted by a juxtaposition of the function and its arguments, as in LISP or other functional languages based on lambda-calculus.

CiME>let fun succ x = x+1;
 succ : int -> int = <fun>
CiME>(succ 4);
 - : int = 5
CiME>(succ (succ 6));
 - : int = 8

Notice that putting parentheses around an application is recommended, by not mandatory:

CiME>succ 4;
 - : int = 5
CiME>succ (succ 6);
 - : int = 8

Functions with several arguments are defined analogously:

CiME>let fun norm x y = x*x+y*y;
 norm : int -> int -> int = <fun>
CiME>norm 3 4;
 - : int = 25

Functions may be defined recursively:

CiME>let fun fact n = if n <= 1 then 1 else n * (fact (n-1));
 fact : int -> int = <fun>
CiME>fact 7;
 - : int = 5040
CiME>fact 100;
 - : int =
9332621544394415268169923885626670049071596826438162146859296389521759999322991
5608941463976156518286253697920827223758251185210916864000000000000000000000000

Notice on that last example that integers may have arbitrary size.

1.1.4  Higher-order functions

The core language is fully higher-order polymorphic functional, so that you can use partial application, functions as arguments, polymorphic arguments:

CiME>let fun f x y = x*x+y*y;
 f : int -> int -> int = <fun>
CiME>let g = f 2;
 g : int -> int = <fun>

CiME>g 5;
 - : int = 29
CiME>let fun eval_at_2 f = f 2;
 eval_at_2 : (int -> ’a) -> ’a = <fun>
CiME>eval_at_2 g;
 - : int = 8
CiME>eval_at_2 (fun x -> x+1);
 - : int = 3
CiME>let fun compose f g x = f (g x);
 compose : (’a -> ’b) -> (’c -> ’a) -> ’c -> ’b = <fun>

1.2  More toplevel user interaction

1.2.1  Loading expressions from files

For a more comfortable use, it is possible to write expressions in a file with your favorite text editor, and tell CiME to evaluate them as if they were typed directly. It is done by the directive #load followed by the file name.

Suppose the file test.cim contains then one may do

CiME>#load "test.cim";
 fib : int -> int = <fun>
- : int = 3
- : int = 5
- : int = 987
- : int = 121393

1.2.2  Interrupting evaluation

If you want to stop an evaluation that takes too much time, you may type Control-C to go back to the toplevel loop:

fib 100;
^CCommand aborted.

1.2.3  Time spent in computation

You may display the CPU time spent evaluating each expression by typing #time on;:

CiME>#time on;
 time is now on
CiME>fib 15;
 Execution time: 0.007998 sec
- : int = 987

To turn off this feature, type #time off;. #time; alone toggles between on and off.

1.2.4  Quitting CiME

You may quit CiME by typing #quit;, or by hitting Control-D.

1.3  Definition of first-order signatures

It is possible to define first order signatures in CiME by giving to signature a string with the description. Arities may be denoted as keywords (constant, unary, binary) or integers. Symbols may be prefix (default), infix or postfix.

CiME>let F_peano = signature "
0 : constant;
s : unary;
+,* : infix binary;
";
 F_peano : signature = signature "* : 2; s : 1; + : 2; 0 : 0"

The set of user variables is defined as follows:

CiME>let X = variables "x,y,z";        
 X : variable_set = variables "z,x,y"

1.4  Definition of Algebra

It is possible to define an algebra on a given signature.

CiME>let A_peano = algebra  F_peano ;
 A_peano : F_peano algebra = algebra F_peano

1.5  Definition of terms

Once you have defined an algebra, you may define terms using the predefined function term which takes as arguments an algebra, and a string denoting a term. Example:

CiME>let t = term A_peano  "s(s(s(0)))*(s(0)+s(s(0)))";
 t : F_peano term = s(s(s(0))) *(s(0)+s(s(0)))
CiME>let u = term A_peano  "s(x)+0+x*s(0)"; 
 u : F_peano term = ((s(x)+0)+x) *s(0)

Beware! As you may see on this last example, CiME does not make any assumptions on the priorities between binary operators of your defined signature. By default, it always associate to the left. To enforce a priority, you have to use parentheses, like below.

CiME>let u = term A_peano  "s(x)+0+(x*s(0))";
 u : F_peano term = (s(x)+0)+(x *s(0))

1.5.1   Terms manipulation

You can also check if there exists a matching from a term to another.

CiME>let u1 = term A_peano  "s(0)+0+(x*s(0))"; 
 u1 : F_peano term = (s(0)+0)+(x *s(0))
CiME>let u2 = term A_peano  "s(0)+0+(0*s(0))"; 
 u2 : F_peano term = (s(0)+0)+(0 *s(0))
CiME>matching u u1;
 - : F_peano substitutions =   
                            (0 solutions)
CiME>matching u u2;
 - : F_peano substitutions =  [x -> 0
                               ] 
                            (1 solutions)

And you can check if two given terms can be unified.

CiME>unify u u1;
 - : F_peano substitutions =  [x -> 0
                               ] 
                            (1 solutions)

In all cases you get a (possibly empty) list of substitutions.

1.6  Rewriting

One may define a rewrite system with the binary function trs, which takes an algebra as first argument, and a string that contains a natural definition of rules as second argument:

CiME>let R_peano = trs A_peano  "
x+0 -> x;
x+s(y) -> s(x+y);
x*0 -> 0;
x*s(y) -> (x*y)+x;
";
 R_peano : F_peano trs
= trs A_peano "  x+0 -> x;
                 
                 x+s(y) -> s(x+y);
                 
                 x *0 -> 0;
                 
                 x *s(y) -> (x *y)+x  "

Given a term and a TRS, you can normalize the term with the TRS, by use of the predefined function normalize:

CiME> normalize R_peano t;
 reduction by [2] x+s(y) -> s(x+y) at pos 1
reduction by [2] x+s(y) -> s(x+y) at pos 1.0
reduction by [1] x+0 -> x at pos 1.0.0
reduction by [4] x *s(y) -> (x *y)+x at pos []
reduction by [4] x *s(y) -> (x *y)+x at pos 0
reduction by [4] x *s(y) -> (x *y)+x at pos 0.0
reduction by [3] x *0 -> 0 at pos 0.0.0
reduction by [2] x+s(y) -> s(x+y) at pos 0.0
reduction by [2] x+s(y) -> s(x+y) at pos 0.0.0
reduction by [2] x+s(y) -> s(x+y) at pos 0.0.0.0
reduction by [1] x+0 -> x at pos 0.0.0.0.0
reduction by [2] x+s(y) -> s(x+y) at pos 0
reduction by [2] x+s(y) -> s(x+y) at pos 0.0
reduction by [2] x+s(y) -> s(x+y) at pos 0.0.0
reduction by [1] x+0 -> x at pos 0.0.0.0
reduction by [2] x+s(y) -> s(x+y) at pos []
reduction by [2] x+s(y) -> s(x+y) at pos 0
reduction by [2] x+s(y) -> s(x+y) at pos 0.0
reduction by [1] x+0 -> x at pos 0.0.0
- : F_peano term = s(s(s(s(s(s(s(s(s(0)))))))))
CiME> normalize R_peano u;
 reduction by [1] x+0 -> x at pos 0
reduction by [4] x *s(y) -> (x *y)+x at pos 1
reduction by [3] x *0 -> 0 at pos 1.0
- : F_peano term = s(x)+(0+x)

This computation may be infinite if the system is not terminating.

1.7  Checking termination of rewrite systems

CiME>termination R_peano;
 NON LINEAR SOLVE launched
NON LINEAR SOLVE launched
SOLVED

 
TRS termination of:
[1] x+0 -> x
[2] x+s(y) -> s(x+y)
[3] x *0 -> 0
[4] x *s(y) -> (x *y)+x
 ,
 CRITERION: MDP
 [ 
      
     DP termination of:
     <xMarked_+s(y) , xMarked_+y>
<xMarked_*s(y) , (x *y)Marked_+x>
<xMarked_*s(y) , xMarked_*y>
 ,
 CRITERION: SG
 [ 
      
     DP termination of:
     <xMarked_*s(y) , xMarked_*y>
 ,
 CRITERION: ORD
 [ 
     Solution found:
     RPO with AFS = AFS: 
     and precedence:
     prec (All symbols are Lex.):  s  <  + ; s  <   * ; +  >  s ; +  <   * ;
                                    *  >  s ;  *  >  + ; 

 ] 

 
DP termination of:
<xMarked_+s(y) , xMarked_+y>
 ,
 CRITERION: ORD
 [ 
     Solution found:
     RPO with AFS = AFS: 
     and precedence:
     prec (All symbols are Lex.):  s  <  + ; s  <   * ; +  >  s ; +  <   * ;
                                    *  >  s ;  *  >  + ; 

 ] 
 ] 
 ] 

- : bool = true

1.7.1  Producing proof trace and proof certificate

The previous example shows that CiME can give information about the termination proof search. When the search succeeds, it is possible to ask for an XML structured trace.

CiME>xml_certify_proof  R_peano;

It is also possible to ask for a certificate that can be checked directly by the Coq proof assistant.

CiME>coq_certify_proof R_peano;

In order to compile this certificate you need the coccinelle coq library (see http://a3pat.ensiie.fr/pub/index.en.html) for the correspondences between CiME, Coq and Coccinelle versions).

1.7.2  Giving a strategy

To prove termination, CiME tries to transform recursively well-foundedness problems into others that are equivalent wrt termination but easier to solve, until he gets trivial problems or problems that are proved directly using a well-founded ordering (pair).

A method allowing to translate a well-foundedness problem into a set of new problems is called criterion

Basic criteria include:

• LEX the lexicographic combination criterion.
• DP the dependency pairs criterion.
• DPM the marked dependency pairs criterion.
• DPO orienting all dependency pairs, generating ordering constraints.
• SCC the basic graph criterion (components decomposition)
• RMVx removing of strictly oriented pairs on component (with the remaining ones weakly oriented) wrt orderings.
• ST the sub-term criterion.
• …
  and of course
• SolveOrd solving the ordering constraints with an ordering pair.

The supported orderings are

• Polynomial interpretations (linear , simple, simple mixed and quadratic)
• matrix interpretations
• LPO (with or without AFS)

Specifying orderings

In the following example we ask CiME to try for 3 seconds to find a linear interpretation with coefficient bound 2, then to try for 5 seconds to find an RPO with AFS, and finally to try for 10 seconds to find a matrix interpretation with coefficient bound 1, matrices of size 3x3 and non-zero constraint on sub-matrices of size 1x1 or 2x2. mnorderparams sets strictly monotonic orderings and orderparams sets weakly monotonic orderings.

CiME>mnorderparams {("linear",{2;3});("rpo",{2;5;2});("matrix",{1;10;3;1;2})};
 - : unit = ()
CiME>orderparams {("linear",{2;3});("rpo",{2;5;2});("matrix",{1;10;3;1})};
 - : unit = ()

CiME has its own constraint solver but it can also try to use an external SAT solver. This can be set by giving, to the Set_sat_solver directive, the name of the SAT solver to be used.

For example, provided minisat2 is installed on the computer, one may select it by typing:

CiME>#Set_sat_solver "minisat2";
 CiME> h : heuristic = <heuristic>

Combining criteria

You can build your own heuristics using a small language allowing to combine basic criteria.

The commands of this small language are the following:

• Use applies the criterion given in argument.
• Solve takes a list of heuristics to try on a goal (when one succeeds, stops).
• Then takes a list of heuristics, each of which has to succeed on all sub-problems generated by the previous one.
• Repeat applies repeatedly a heuristic until it fails.

CiME>let h = heuristic "Then [Use DPM; Use DPO; Use SolveOrd]";
 - : unit = ()
CiME>set_heuristic "h";
 - : bool = true

1.8  Checking confluence of rewrite systems

You can check the local confluence of a TRS.

CiME>confluence  R_peano ;
 CiME> - : unit = ()

1.9  String rewriting

There is no interactive input for srs, you should encode them as a TRS. For example, the standard SRS below¹:

(RULES
b b b  -> a ,
a a  -> a b a ,
a a a  -> b a a 
)

can be rewritten:²

let R_trs_0_variable =  variables "__x" ;
let R_trs_0_signature =  signature "b : 1; a : 1" ;
let R_trs_0_algebra =  algebra R_trs_0_signature ;
let R_trs_0 =
 trs R_trs_0_algebra "
   b(b(b(__x))) -> a(__x);x
   
   a(a(__x)) -> a(b(a(__x)));
   
   a(a(a(__x))) -> b(a(a(__x))) 
  " ;

1.10  Using CiME in batch mode

CiME can also manage files in batch mode.

A typical use is

cime  -icime  preamble_file.cim -itrs trs_file.trs -oxml xml_file_trace.xml

where trs_file.trs is the file containing the term rewriting system you want to check for termination, preamble_file.cim is a CiME file containing information to drive the proof (heuristics, orders, SAT solver name, etc.), and xml_file_trace.xml is the resulting proof trace.

A efficient strategy is given by the preamble below:

CiME>#Set_sat_solver "minisat2";
CiME>
CiME>orderparams {("linear",{3;10});("rpo",{0;25;2});("simple",{2;15});("matrix",{1;50;3;1})};
CiME>subtermparams 0;
CiME>let h = heuristic
CiME>"Then [Use DPM; Repeat Then [ Use SCC; Solve[Use ST;Use RMVx;Then [ DPSG; SolveOrd ]] ] ]";
CiME>set_heuristic "h";

You may also produce a coq certificate from an xml or cpf file by the following commands:

cime  -ixml xml_file_trace.xml -ocoq coq_certificate.v

or

cime  -icpf cpf_file_trace.xml -ocoq coq_certificate.v

This is the way to generate certificates for traces from other provers.

The accepted input and output formats are listed below and can be mixed freely.

1.10.1  Input formats

• cime
• srs : the tpdb format for string rewriting system http://www.lri.fr/~marche/tpdb/format.pdf
• trs : the tpdb format for term rewriting system http://www.lri.fr/~marche/tpdb/format.pdf
• xml : described by the dtd http://a3pat.ensiie.fr/pub/a3pat.dtd
• cfp : the new Certification Problem Format http://cl-informatik.uibk.ac.at/software/cpf/

1.10.2  Output format

• cime
• srs
• trs
• xml
• cfp
• coq http://coq.inria.fr/

1

Bouchare.01.srs from the TPDB data base

2

The conversion can be made automatically using CiME in batch mode by typing:cime3 -isrs Bouchare.01.srs -ocime -

Index

This document was translated from L^AT_EX by H^EV^EA.