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

[J. Nunez Fontarnau]

Dear Enea

The purpose of constraints such as B =< 10000 is to bound the values of variable
B according to the numemrical system underlying it, for instance, for an
imaginary floating point system such that would permit the representation of
values no greater than 10000. The case of A =< 100 has no justification: it was
just a "what if ..." constraint. :)

>From the fixpoint obtained, the analysis shall determine (whenever possible)
whether the program will overflow for some query. In this case, the condition
for overflow would thus be something like $C>1000$ (or rather something with
non strict inequalities in this case).

This logic program converges to the fixpoint $1/(1-0.75)$ independently of the
initial value and the number of iterations. In general, a recurrence relation of
the form $X_{n+1} = A \times X_{n} + B$ converges to a fixpoint $Y^*$ only if
$abs{A} < 1$; if so, $Y^* = B/(1-A)$. Using a relational numerical domain such
as polyhedra, I would like to capture information such as "no query overflows
this program", or "convergence is independent of the number of iterations".

For instance, note that in

> ?- 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

it coincides that $10000/2499 \approx 4$, where $4$ is in fact the fixpoint
value of the relation $X_{n+1} = 0.75 \times X_{n} + B$. I am not sure this has
some explanation. Moreover, $A$ corresponds to the number of iterations in
$X_{n+1}$.

Do you think that from that fixpoint above it is possible to conclude that no
query to the program will cause overflow ?

I wonder also whether PPL provides any facilities for narrowing (downward
iterations).


Many Thanks,
Javier



> > 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.