This chapter is a small tutorial, to present the basic features of CiME in a progressive way.
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
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 ??.)
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.
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>
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
let fun fib n = if n <= 1 then 1 else (fib (n-1)) + (fib (n-2)); fib 3; fib 4; fib 15; fib 25;
then one may load it as follows
CiME>#load "test.cim"; load failed: test.cim: No such file or directory
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.
You may display the CPU time spent evaluating each expression by
typing #time on;:
CiME>#time on; time is now on CiME>fib 15; Typing error: undefined identifier fib
To turn off this feature, type #time off;. #time; alone
toggles between on and off.
You may quit CiME by typing #quit;, or by hitting Control-D.
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"
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
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))
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.
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.
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 : s < + ; s < * ; + < * ; and status: statuses : all other symbols are Lexico ] DP termination of: <xMarked_+s(y) , xMarked_+y> , CRITERION: ORD [ Solution found: RPO with AFS = AFS: and precedence: prec : s < + ; s < * ; + < * ; and status: statuses : all other symbols are Lexico ] ] ] - : bool = true
The previous example shows that CiME can give information about the termination proof search. When the search succeeds, it is possible to ask
for a Coq script 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).
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:
The supported orderings are
In the following example we build two sequence of ordering parameters. The first one parametrises search for firstly a linear polynomial interpretations with coefficients ≤ 3 and a timeout of 10 seconds, secondly a simple polynomial interpretation with coefficients ≤ 2 and a timeout of 15 seconds,thirdly a full RPO with AFS with a timeout of 15 seconds and lastly a matrix interpretation with coefficients ≤ 2, matrices of size 2× 2 and sub-matrices of size 1.
In the second one the timeout being unspecified are infinite.
CiME>let o1 = params "10 linear 3; 15 simple 2; 15 rpo; 30 matrix 2 2 1"; o1 : params = 10 linear 3;15 simple 2;15 rpo 2;30 matrix 2 2 1 CiME>let o2 = params "linear 3; simple 2; rpo; matrix 2 2 1"; o2 : params = 0 linear 3;0 simple 2;0 rpo 2;0 matrix 2 2 1
CiME has its own constraint solver, however some techniques may require the use of an external SAT solver. It can be set by giving, to the Set_sat_solver directive, the invocation name of the SAT solver to be used. Remarks that the SAT solver must fulfil the input/output SAT Format requirements.
For example, provided minisat2 is installed on the computer, one may select it by typing:
#Set_sat_solver "minisat2";
You can build your own heuristics using a small language allowing to combine basic criteria.
The commands of this small language are the following:
CiME>let h1 = heuristic " Repeat Then [ DPG ; Solve [ ST ; RMVx {o2} ] ] "; h1 : heuristic = <heuristic> CiME>let h2 = heuristic " Then [ Repeat lex_manna_ness {o1}; DPM; h1] "; h2 : heuristic = <heuristic> CiME>set_heuristic "h2"; - : unit = () CiME>subtermparams 2; - : unit = ()
You can check the local confluence of a TRS.
CiME>local_confluence R_peano ; - : bool = true
You can check checks in one step both termination and local confluence. This returns false if one of the two properties can not be proved".
CiME>convergence R_peano ; NON LINEAR SOLVE launched NON LINEAR SOLVE launched 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: LEX using polynomial interpretation = [ 0 ] () = 1; [ + ] (X0,X1) = 1*X1 + 1*X0; [ s ] (X0) = 1*X0 + 1; [ * ] (X0,X1) = 1*X1*X0 + 1*X1 + 1*X0; removing <x *s(y),(x *y)+x><x+0,x> [ TRS termination of: [3] x *0 -> 0 [2] x+s(y) -> s(x+y) , CRITERION: LEX using polynomial interpretation = [ 0 ] () = 0; [ + ] (X0,X1) = 2*X1 + 1*X0; [ s ] (X0) = 1*X0 + 1; [ * ] (X0,X1) = 1*X1 + 1*X0; removing <x+s(y),s(x+y)> [ TRS termination of: [3] x *0 -> 0 , CRITERION: ORD [ Solution found: polynomial interpretation = [ 0 ] () = 0; [ * ] (X0,X1) = 1*X1 + 1*X0 + 1; ] ] ] - : bool = true
CiME can performs proof of equality modulo equational theories. Here is a typical example:
let X = variables "x, y, z, u";
let Gsig = signature "
. : infix binary ;
i : unary ;
e : constant ;
";
let Galg = algebra Gsig;
let Grules = trs Galg "
(x . y) . z -> x . (y . z) ;
x . e -> x ;
x . i(x) -> e ;
";
let Gprec = precedence Gsig "i > . > e" ;
let Gstat = status Gsig " ";
let Grpo = rpo Galg Gprec Gstat ;
prove_goal Grpo Grules (term Galg "i(e)") (term Galg "e");
There is no interactive input for srs, you should encode them as a TRS. For example, the standard SRS below1:
(RULES b b b -> a , a a -> a b a , a a a -> b a a )
can be rewritten:2
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))) " ;
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.
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.
Remarks that for proofs of equality you should use the -eq prefix; And that currently only CiME format is available as input and only the Coq format is available as output.
main.opt -eq -noterm -icime equalytyPb.cim -ocoq equalytyProof.v
This document was translated from LATEX by HEVEA.