public_html
in Your home directory, that can be referred
to by http://your.site/~yourname/
. Please be aware that
the files in public_html
are accessible to the general
public.
This is the only method to analyse programs that are larger than ~6Kb.
:- cti:snorm([term_size(a,2)]).
. Same for hanoiapp.suc.
.emacs
. With C-c C-t the current buffer is
analyzed.
(require 'browse-url) ;; can be customized to a particular browser (require 'webjump) (defun cti-analyse-buffer () "Analyse current buffer with cTI" (interactive) (browse-url (concat "http://www.complang.tuwien.ac.at/cti/cgi/cti?texta=" (webjump-url-encode (buffer-string)) "&rows=0" ;; No need to edit the program ;; Add further options here ;; "&skipcomp=" ;; Skip comparison ))) (global-set-key "\C-c\C-t" 'cti-analyse-buffer) ;;
It seems, however, that the actual observed speedups rarely reach a factor of 2. On the other hand, the larger the program the bigger the speedup obtained.
If NTI labels the result of cTI as optimal, then there is no better (more general)
termination condition built with the given predicates
(i.e. b(X)
etc.) to ensure termination. In other words: for all
modes not covered by the termination condition: there is (at least)
one universally nonterminating query. All nonterminating queries used
in NTI's reasoning are displayed. Notice however, that quite often, a
more elaborate language for termination conditions could describe
larger classes of terminating queries. Consider for example app/3
.
Here the inferred condition app(A,B,C) terminates_if
b(A);b(C)
is labeled optimal. However, there are many
terminating queries that do not fall under the inferred condition.
E.g., queries, where the list-length is bound:
app([_],_,_)
, and other less evident queries:
app([a|_],_,[b|_])
.
If NTI was not able to prove optimality this is due to a weakness in cTI or NTI. The still unresolved cases are shown, i.e. where neither a proof of termination (by cTI), nor of non-termination (by NTI) was possible. Cases implied by the indicated ones but more complex are omitted.
The following options are available:
false
as
the termination condition.
To help NTI finding interesting queries the directive
nti:nonterminating_goal/1
can be used. Notice that this
directive does not affect the correctness of the obtained result. To
obtain best results try to ground all arguments as much as possible.
E.g. to prove that Plümer's turing/4
does not terminate
add the directive :- nti:nonterminating_goal(turing(t([],' ',[]),s0,[p(s0,' ',s1,' ',r),p(s1,' ',s0,' ',l)],y)).
.
In this example, we added the directive in the text field while
reusing the original program pl5.2.2.
0.22e
2007-02-21 Server upgrade from 1.5 Mlips to 23 Mlips 2007-02-21 Remote flag disabled 2006-06-05 0.26i fixes bug with operator declarations 2002-02-04 0.26h fixes bug with pending constraints 2001-02-28 0.26f Fixes NTI bug found by Etienne Payet 2001-02-12 Web-Interface highlighting of optimal solutions 2001-02-12 NTI: new directive to help to find proofs of nontermination 2001-02-11 Web-Interface: Same/Next button for stepping through lists 2001-02-08 0.26e NTI shows now all nontermination proofs involved 2001-01-04 0.31 (0.30) experimental 2000-09-23 Web-Interface: Textfield and URL are taken together 2000-09-22 0.26b better presentation of results 2000-09-22 Web-Interface outlining 2000-09-22 0.26a NTI improvements 2000-09-18 first NTI installed 2000-09-16 0.26 (0.25) 2000-09-13 0.22e: some incorrect : handling fixed 2000-05-26 Web-Interface: faster machine accessible (type r in version field) 2000-05-18 Web-Interface: tooltips added 2000-05-17 0.22c: norms via term mappings 2000-05-10 0.22b: improved presentation of DCG conditions 2000-05-07 0.22a: Web-Interface: show stderr if important messages are there issue warnings about ignored directives, in particular dynamic/1 etc. 2000-04-22 0.22 stable, formulas are presented in a canonical form 2000-04-12 0.19 stable 2000-04-12 0.18 2000-03-21 Web-Interface: SELECT instead of RADIO 2000-03-20 new option optimal 2000-03-20 0.17 runs with 3.8.2, more fixes 2000-03-20 0.16 fixes most known bugs 2000-03-14 0.15x same as 0.15 but compiled with new SICStus 3.8.2, evidently broken 2000-03-14 0.15 improvements 2000-03-08 0.14a new syntax, experiments with termination neutral arguments 2000-03-07 0.14 boundedness annotations and size relations 2000-02-22 0.13 2000-02-22 Web-Interface: Versions supported 1999-07-03 new Web-interface 1999-06-30 0.04
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.
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.
||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 |
||0
||Term-Size = 0
||s(0)
||Term-Size = 1
||s(s(0))
||Term-Size = 2
||f(0,0)
||Term-Size = 1
:- cti:norm_tmap(Eqs).
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:
:- cti:snorm(Cls).
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)]).
:- cti:twnorm(Defsizes)
.
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 |
:- 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.
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.