This is the code I am using to obtain a fixpoint for append. Note that no widening is applied: so far the code is aimed at producing a (possibly) infinite 'iteration'. Though so it does, the polyhedra produced are always the same. Note also that a query to 'fixpoint' will terminate in the base case. (?) Only by changing the order of occurrence of the inductive and base 'fixpoint' clauses, infinite recursive calls are obtained.
Please help. Javier
% Iteration to Post-Fixpoint for Append.
%verbosity(0). verbosity(1).
wappend :-
% Base case make_vars(6, [A, B, C, D, E, F]), ppl_new_Polyhedron_from_dimension(c, 6, Base), ppl_Polyhedron_add_constraints(Base, [A = 0, B >= 0, C = B]), ppl_Polyhedron_get_constraints(Base, BConstr), display_message(['Base constraints ...']), display_message(BConstr),
% Inductive case ppl_new_Polyhedron_from_dimension(c, 6, Induc), ppl_Polyhedron_add_constraints(Induc, [A + F = C + D, B = E, C + D >= A, D >= 0, B >= 0, A >= D + 1]), ppl_Polyhedron_get_constraints(Induc, IConstr), display_message(['Inductive constraints ...']), display_message(IConstr),
% Empty polyhedron ppl_new_Polyhedron_empty_from_dimension(c, 6, Empty),
display_message(['Querying fixpoint/4 ...']),
fixpoint(Induc, Empty, Base, Fixpoint), ppl_Polyhedron_get_constraints(Fixpoint, FConstr), display_message(['Post-Fixpoint ...']), display_message(FConstr),
display_message(['Deleting Base ...']), ppl_delete_Polyhedron(Base), display_message(['Deleting Induc ...']), ppl_delete_Polyhedron(Induc), display_message(['Deleting Empty ...']), ppl_delete_Polyhedron(Empty).
%%%%%%%%%%%%%%%%%%%%%%%%%%% % Post-fixpoint calculation
% Base case fixpoint(_, Previous, Current, Fixpoint) :-
ppl_Polyhedron_contains_Polyhedron(Current, Previous), ppl_Polyhedron_get_constraints(Current, FCurrent), display_message(['Base case: Current ...']), display_message(FCurrent), ppl_Polyhedron_get_constraints(Previous, FPrevious), display_message(['Base case: Previous ...']), display_message(FPrevious),
ppl_new_Polyhedron_from_Polyhedron(c, Current, c, Fixpoint), !.
% Inductive case fixpoint(Induc, Previous, Current, Fixpoint) :-
ppl_delete_Polyhedron(Previous), ppl_new_Polyhedron_from_Polyhedron(c, Current, c, Current1), ppl_Polyhedron_get_constraints(Current1, FCurrent1), display_message(['Inductive case: Current 1 ...']), display_message(FCurrent1), ppl_Polyhedron_get_constraints(Induc, FInduc), display_message(['Inductive case: Induc ...']), display_message(FInduc),
% computations over current1 ppl_Polyhedron_poly_hull_assign(Current1, Induc), ppl_Polyhedron_get_constraints(Current1, FCurrent1a), display_message(['Current 1 after convex hull ...']), display_message(FCurrent1a),
ppl_Polyhedron_get_constraints(CS_P, Current1), ppl_Polyhedra_get_constraints(CS_Q, Induc), widen_extrapolation_init(P, CS_P, Topology), widen_extrapolation_init(Q, CS_Q, Topology), ppl_Polyhedron_H79_widening_assign(P, Q),
display_message(['Recursive query to fixpoint ...']),
fixpoint(Induc, Current, Current1, Fixpoint).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % make_var_list(+I,+Dimension,?VariableList) % constructs a list of variables with indices from I to Dimension - 1. % It is assumed that I =< Dimension.
make_vars(Dim, VarList):- make_var_list(0, Dim, VarList). make_var_list(Dim,Dim,[]):- !. make_var_list(I,Dim,['$VAR'(I)|VarList]):- I1 is I + 1, make_var_list(I1,Dim,VarList).
%%%%%%%%%%%%%%%%%% % Output messages.
display_message(Message):- verbosity(1), !, nl, write_all(Message), nl. display_message(_).
write_all([]). write_all([Phrase|Phrases]):- write(Phrase), write(' '), write_all(Phrases).
On Tue, 7 Sep 2004 10:10:06 +0100 (BST), P M Hill wrote
Hi Javier,
Have a look in ppl/interfaces/Prolog/pl_check.pl
There are tests for the ppl Prolog widening predicates such as ppl_Polyhedron_H79_widening_assign/2.
I have written some longer code that uses the widening to ensure convergence in some analysis but it will not be in the ppl sources.
I'll see if I can find it.
Pat On Tue, 7 Sep 2004, Enea Zaffanella wrote:
J. Nunez Fontarnau wrote:
Hi Enea How are you ?
I need to ask you about fixpoint calculations and widenings in PPL. As
you are
the expertise in all the implementation stuff, I would like to ask
whether there
is any examples on fixpoint calculation with PPL and widening for
Prolog (not
C++). I've noticed a file append?.cc that calculates the fixpoint for
append. I
am trying to rewrite it in Prolog, but I am a bit lost with
the 'reassignment'
of polyhedra 'Previous' and 'Current'
Any suggestions on how to implement this in Prolog would be very much appreciated.
Thanks, Javier
Dear Javier,
I am not sure I have understood your question. As I see it, you are going in the wrong direction, since it seems that you want to repeat the iterative control flow of append*.cc into your Prolog program, whereas I would suggest to go for a more canonical recursive solution.
Namely, your solution sould be something similar to the following
pattern:
%% base case upward_iteration_sequence(Previous, Current, Inductive, Current) :- ppl_Polyhedron_contains_Polyhedron(Previous, Current), !.
%% inductive case. upward_iteration_sequence(Previous, Current, Inductive, Result) :- ppl_delete_Polyhedron(Previous), ppl_new_Polyhedron_from_Polyhedron(c, Current, c, Current1), %% perform the required computation modifying Current1. ...., upward_iteration_sequence(Current, Current1, Inductive, Result).
I hope this is enough. Anyway, Pat is much more expert than me on the Prolog interface of PPL.
Ciao, Enea.
-- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it
Dear Javier,
J. Nunez Fontarnau wrote:
This is the code I am using to obtain a fixpoint for append. Note that no widening is applied: so far the code is aimed at producing a (possibly) infinite 'iteration'. Though so it does, the polyhedra produced are always the same. Note also that a query to 'fixpoint' will terminate in the base case. (?) Only by changing the order of occurrence of the inductive and base 'fixpoint' clauses, infinite recursive calls are obtained.
Please help. Javier
[...]
% Base case fixpoint(_, Previous, Current, Fixpoint) :-
ppl_Polyhedron_contains_Polyhedron(Current, Previous),
I guess that here you have to revert the order of arguments in the containment test. In an upward iteration sequence, it is always the case that the Current polyhedron contains the Previous one. As a side note, I would have placed the cut immediately after the containment test.
% Inductive case fixpoint(Induc, Previous, Current, Fixpoint) :-
ppl_delete_Polyhedron(Previous), ppl_new_Polyhedron_from_Polyhedron(c, Current, c, Current1), ppl_Polyhedron_get_constraints(Current1, FCurrent1), display_message(['Inductive case: Current 1 ...']), display_message(FCurrent1), ppl_Polyhedron_get_constraints(Induc, FInduc), display_message(['Inductive case: Induc ...']), display_message(FInduc),
% computations over current1 ppl_Polyhedron_poly_hull_assign(Current1, Induc),
?
I guess that this is not the computation that you want to perform. You are using poly-hull where an intersection should be used. Moreover, you are not implementing the renaming apart of variables. For a hint of how things could be done, see our tests/append1.cc C++ example.
Very briefly, Previous and Current should be 3-dim polyhedra, whereas Induc is a 6-dim polyhedron. In order to correctly compose them, you should first extend Current1 (the copy of Current) to be a 6-dim polyhedron using the "concatenation" method (that is, implement the renaming apart operation). Then you should intersect it with Induc (that is, compute the conjunction of the results of the recursive call with the constraints in the body of this clause). Finally, you have to remove the last three variables (that is, project the result on the clause's head variables).
Hoping that this is helpful enough.
Ciao, Enea.
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()'
Another constraints setting that produces the same error consists in removing $A <= 100$ and $B =< 10000$, and querying the program with ?- w(100).
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
----------------------
In this program, argument $K$ corresponds to the bounds for triggering a widening operator (in this case the standard: H79).
verbosity(1).
w(K) :-
make_vars(6, [A, B, C, D, E, F]),
% Base case ppl_new_Polyhedron_from_dimension(c, 3, Base), ppl_Polyhedron_add_constraints(Base, [A = 0, B >= 0, C = B]), display_poly(['Base'],Base),
% Inductive case ppl_new_Polyhedron_from_dimension(c, 6, Induc), ppl_Polyhedron_add_constraints(Induc, [A =< 100, A >= 0, B >= 0, B =< 10000, C >= 0, D >= A - 1, 4*E >= 3*B + 4, C = F]), display_poly(['Inductive'],Induc),
% Previous polyhedron ppl_new_Polyhedron_empty_from_dimension(c, 3, Previous),
fixpoint(1, K, Induc, Previous, Base, Fixpoint, N), display_poly(['Fixpoint'],Fixpoint), display_message(['reached in',N,'iterations']).
%%%%%%%%%%%%%%%%%%%%%%%%%%% % Post-fixpoint calculation
% Base case fixpoint(N, _, _, Previous, Current, Fixpoint, N) :-
ppl_Polyhedron_contains_Polyhedron(Previous, Current), !, ppl_new_Polyhedron_from_Polyhedron(c, Current, c, Fixpoint).
% Inductive case fixpoint(N, K, Induc, Previous, Current, Fixpoint, M) :-
make_vars(6, [A, B, C, D, E, F]),
ppl_delete_Polyhedron(Previous), ppl_new_Polyhedron_from_Polyhedron(c, Current, c, Previous1), ppl_delete_Polyhedron(Current), ppl_new_Polyhedron_from_Polyhedron(c, Induc, c, Current1), ppl_new_Polyhedron_from_dimension(c, 3, Aux), ppl_Polyhedron_concatenate_assign(Aux, Previous1), ppl_Polyhedron_intersection_assign(Current1, Aux), ppl_delete_Polyhedron(Aux), ppl_Polyhedron_remove_dimensions(Current1,[D,F,E]), ppl_Polyhedron_poly_hull_assign_and_minimize( Current1, Previous1), (N >= K, ppl_Polyhedron_H79_widening_assign(Current1, Previous1); true), display_poly(['Iteration ', N],Current1), N1 is N+1, fixpoint(N1, K, Induc, Previous1, Current1, Fixpoint, M).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % make_var_list(+I,+Dimension,?VariableList) % constructs a list of variables with indices from I to Dimension - 1. % It is assumed that I =< Dimension.
make_vars(Dim, VarList):- make_var_list(0, Dim, VarList). make_var_list(Dim,Dim,[]):- !. make_var_list(I,Dim,['$VAR'(I)|VarList]):- I1 is I + 1, make_var_list(I1,Dim,VarList).
%%%%%%%%%%%%%%%%%% % Output messages.
display_poly(Message, Polyhedron) :- ppl_Polyhedron_get_constraints(Polyhedron, Constraints), display_message(Message), display_message(Constraints).
display_message(Message):- verbosity(1), !, nl, write_all(Message), nl. display_message(_).
write_all([]). write_all([Phrase|Phrases]):- write(Phrase), write(' '), write_all(Phrases).
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@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.
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.
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.
Dear Javier,
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. :)
reconsidering your program, it seems to me that you forgot to provide these "numerical system bounds" for variables B and C for the base case of your inductive computation. Namely,
ppl_Polyhedron_add_constraints(Base, [A = 0, B >= 0, C = B])
is already allowing for an "overflowing computation", so there is no hope that the final result will be bounded. I guess you should, at the very least, add the constraint B =< 10000 also here.
Ciao, Enea.
participants (3)
-
Enea Zaffanella -
Enea Zaffanella -
J. Nunez Fontarnau