J. Nunez Fontarnau wrote:
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 ?
If by "overflow" you mean any variable going beyond your 10000 bound, then I guess that you have an overflow here. I should better speak only after checking it, but at a first glance it seems that the fixpoint is describing an unbounded polyhedron.
The library provides the predicate ppl_Polyhedron_is_bounded/1, with the obvious semantics. If you want to know the exact bounds, then you could either directly inspect the generator system or call predicates ppl_Polyhedron_bounds_from_above/2 and ppl_Polyhedron_bounds_from_below/2.
I wonder also whether PPL provides any facilities for narrowing (downward iterations).
Many Thanks, Javier
No narrowing operator is provided (yet). Anyway, you can easily compute a downward iteration sequence of (any) finite length using simply intersection.
Ciao, Enea.