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