[PPL-devel] Re: Fixpoint + Widening in PPL

[Enea Zaffanella]

Hi, Javier.

J. Nunez Fontarnau wrote:
> Dear Enea
> 
> I would appreciate it to the more if you could shed some light on the following
> problem. Given the logic program
> 
> p(0, X, X) :- !.
> 
> p(N, X, Y) :-
> 
> 	X1 is 0.75*X+1,
> 	N1 is N - 1,
> 	p(N1, X1, Y).
> 
> 
> such that recurses $N$ times over the expression $0.75*X+1$, find a fixpoint by
> which no overflow in the $X$ and $Y$ arguments can be proved.
> 
> My proceeding on this includes the construction of two polyhedra: one for the
> base case; the other for the inductive case. Then I (try to) calculate the
> fixpoint using the program below. But a series of problem arise. For instance,
> for the inductive constraints as shown below (note in particular $B =< 10000$),
> the following abnormal halting error pops up, at the second fixpoint iteration:
> 
> ERROR: Unhandled exception: 'Integer_to_integer_term()'

This seems to be caused by the call to the output function, since the 
Prolog system you are using (i.e., ... ?) cannot handle arbitrary 
precision integers. If you comment away all the calls to display_poly/2 
but the last one printing the fixpoint, then you won't get the exception.

I tested your program using ppl_pl (after commenting all but the last 
polyhedra output). Note that the choice of k=17 is arbitrary ... just to 
let you see that the ppl core is not throwing an exception.

==============================
[zaffanella at spark somepath]$ ppl_pl
Welcome to SWI-Prolog (Multi-threaded, Version 5.2.13)
Copyright (c) 1990-2003 University of Amsterdam.
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
and you are welcome to redistribute it under certain conditions.
Please visit http://www.swi-prolog.org for details.

For help, use ?- help(Topic). or ?- apropos(Word).

?- consult(fixpoint).
Warning: (/somepath/fixpoint.pl:43):
         Singleton variables: [A, B, C]
% fixpoint compiled 0.00 sec, 4,720 bytes

Yes
?- w(17).

Fixpoint

1*A>=0 1*B>=0

reached in 19 iterations

Yes
?-
==============================


Mmmmmhhhh ... not a really interesting invariant.
I may be missing something, but I guess that you are doing something 
wrong. For instance, why using the non-strict inequalities
 > 		 D >= A - 1, 4*E >= 3*B + 4,
to approximate the built-ins
 > 	X1 is 0.75*X+1,
 > 	N1 is N - 1,

?

I would have used equalities instead.
If you do this, you would obtain the following stronger invariant:

==============================
?- w(3).

Fixpoint

2499*A+ -1*B+1*C>=0 1*A+1*B+ -1*C>=0 1*B>=0

reached in 5 iterations

Yes
?-
==============================

> I would be thankful if you could suggest some hints on how to get a fixpoint for
> the program above. It might be that I do not declare enough constraints so that
> sufficient information to assure convergence is included.
> 
> Many Thanks.
> 
>   Ciao,
> Javier

You now have the post-fixpoint. Note though that I have not fully 
understood the link between your original program and the kind of 
analysis you are performing. For instance, where do the bounds A <= 100 
and B <= 10000 come from?

Anyway, in order to improve the fixpoint you can use the 
limited_h79_extrapolation_assign (which is a widening, if you ensure 
that you will always call it by passing the same constraint system), or 
you can conclude your abstract computation by adding one (or more) steps 
of a downward iteration sequence.

Cheers,
Enea.