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

[Enea Zaffanella]

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.