WWW interface: [Indicating a program, saving result, options-[TNA, NTI, Comparison, Version], tips]
Language: [Boundedness annotations, norms-[term-size, user defined, symbolic], size relations]

cTI WWW interface

Indicating a program

Saving a result

Options

Tips

When following a link, options just previously selected are not preserved. Reanalyze the current page to get the options into the link.

Language

The language supported is SICStus-Prolog, including the ISO-standard. The current implementation assumes that programs are executed with the occurs check enabled (since 0.16). I.e., we assume that a goal like s(X) = X fails. Note that other Prologs like SWI allow an implicit occurs check. Directives related to the environment (e.g. include/1) are currently not handled. An appropriate warning is issued. In addition, the following built-in predicates are recognized (as of 0.21):
dif/2, false/0, if/3, keysort/2, sort/2, format/2, ground/1
'C'/3, assert/1, compare/3, display/1, erase/1, get0/1, get0/2, length/2, name/2, not/1, numbervars/3, recorda/3, recorded/3, recordz/3, retractall/1, statistics/2, tab/1, ttynl/0, ttyput/1.

Goals of unknown predicates are considered nonterminating (since 0.21). A predicate is unknown if it has no visible definition and is not known to the system as a built-in predicate.

To permit more advanced termination proofs, the following annotations are provided.

Boundedness annotations

A formula stating the boundedness of variables with b(V) using conjunction(,/2) and disjunction (;/2). In the following example we ensure in t/3, that As or Cs are bound (finite and ground). cTI will therefore prove the termination property of t/3 under this particular condition.
t(As, Bs, Cs) :-
	cti:{b(As);b(Cs)}, % check this condition
	app(As,Bs,Cs).

app([], As, As).
app([E|Es], Fs, [E|Gs]) :-
	app(Es, Fs, Gs).
Try this example
app(A,B,C)terminates_if b(A);b(C).
t(A,B,C)terminates_if true.
The obtained result says that t/3 will always terminate, even if t/3 is used with free variables. In this case, an error due to the predicate {}/1 terminates the computation.

Norms

Term-size norm

By default cTI uses the symbolic norm term-size defined as follows:
       ||t||Term-Size = 1 + Sum(i=1..n, ||ti||Term-Size) if t = f(t1,...tn), n > 0
= 0 if t is a constant
= t if t is a variable

Examples

||0||Term-Size = 0
||s(0)||Term-Size = 1
||s(s(0))||Term-Size = 2
||f(0,0)||Term-Size = 1

User defined norms - term mappings

We provide several ways to specify norms (since 0.22c). They are all indicated with directives.
Term mapping :- cti:norm_tmap(Eqs).
Some function symbols (or constants) are mapped into other terms prior to using the term-size norm. Eqs is a list of equations of the form LHS=RHS.

Restrictions. The syntax of norms is restricted as follows. For equations LHS=RHS: LHS must be a term with all arguments free distinct variables. RHS must not contain the functors on the left hand side of all equations. Further, RHS must only contain variables of LHS. All LHS must be different.

Example:

Symbolic norm :- cti:snorm(Cls).
The argument Cls is a list of terms term_size(T,Expr) and (optionally) at the end default(Constant). The argument Expr is an expression, composed of positive integers, +/2,*/2 and n(Term) indicating the size of a term.

Example: :- cti:snorm([term_size(a,2)]).

TerminWeb syntax :- cti:twnorm(Defsizes).
The norm in the style of TermiWeb with the same restrictions as for cti:snorm/1. (Snorms are simply a syntactic variant of TermiWebs norms).

A norm similar to the well known list-length norm can be obtained by adding one of the following directives.

:- cti:norm_tmap([ [_|Xs] = l(Xs) ]).
:- cti:snorm([term_size([_|Xs], 1+n(Xs))]).
All occurrences of the list constructor are replaced by l/1, ignoring the element of the list. This corresponds to the following list-length norm:
       ||t||List-Length = 1 + ||t2||List-Length if t = [t1|t2]
= 1 + Sum(i=1..n, ||ti||List-Length) if t = f(t1,...tn), n > 0 and f/n is not the list constructor
= 0 if t is a constant
= t if t is a variable
Notice the difference to the usual list-length norm which maps all other function symbols to 0. Such a norm usually weakens the result for programs that use both lists and other function symbols. Type inference would be needed to apply different norms within the same predicate.
:- cti:norm_tmap([ [_|Xs] = l(Xs) ]).
app2(A,B,Bs,Cs) :-
	app([A,B], Bs, Cs).

app([], As, As).
app([E|Es], Fs, [E|Gs]) :-
	app(Es, Fs, Gs).

list_lensx([], 0).
list_lensx([_|Xs], s(N)) :-
	list_lensx(Xs, N).

app2len(N, Bs,Cs) :-
	list_lensx(As, N),
	app(As, Bs, Cs).
Try it using list-length norm via term mapping, default term-size, simulating the traditional list-length norm
:- cti:norm_tmap([ op(A,B) = xop(A,A,B) ]).
rewrite(op(op(A,B),C),op(A,op(B,C))) :- !.
rewrite(op(A,op(B,C)),op(A,L)) :-
        rewrite(op(B,C),L).

normal_form(F,N) :- rewrite(F,F1), !, normal_form(F1,N).
normal_form(F,F).
Try this example with term mapping, or a symbolic norm; and without.

Size relations between variables

Syntax: cti:{Linexpr1 =< Linexpr2} The size (w.r.t. the currently used norm) of variables is denoted by n(V). These annotations are used to improve the precision of the analysis.
t2(As,Bs,Cs):-
	cti:{n(Bs) > n(As)},
	app(As,Bs,Cs).

app([], As, As).
app([E|Es], Fs, [E|Gs]) :-
	app(Es, Fs, Gs).
Try it.
Valid HTML 4.0 cTI, Fred Mesnard (Université de La Réunion), Ulrich Neumerkel (Technische Universität Wien)