[PPL-devel] How to do Powerset element normalization

[Roberto Bagnara]

Pedro Vasconcelos wrote:
> I am starting to use the closed convex polyhedra powerset domain for my
> PhD research. Since I want to use it from Haskell, I'm extending the C
> and Haskell bindings (built on top of the C interface to PPL version
> 0.6.1). So far I have managed to get a minimal interface working --
> creating powersets, adding disjuncts and constraints and outputing
> results.

Hello Pedro,

you may want to use the work of/share your work with Hosung Song,
who is reading this in CC.

By the way, we (the PPL developers) are more and more curious
about these Haskell bindings we have read about in some recent
messages to the mailing list.  It may come as a surprise to you,
but we never saw them and we have not the slightest idea about
how they look like.  Can you give us a pointer?

> Now the question I have is: what is the prefered way to ensure that a
> powerset is Omega-reduced, i.e. all its elements are maximal wrt the
> original partial order (in particular, removing bottom elements)?
> Polyhedra_PowerSet<C_Polyhedron> has a member function `omega_reduce()'
> that is suposed to do just this, but it is protected, so the compiler
> complains if I try to use in the C interface.

The interface for Polyhedra_Powerset is still experimental and we are
still designing it.  Since the release of PPL 0.6.1 we have been very
busy doing other things (a good part of them PPL-related) and this
part of the library has suffered a bit.  It would be nice if we could
take the occasion and work with you and Hosung towards improving and
finishing this part of the work.  This is especially important for us
also in view of the new numerical abstractions we are about to add
to the library: bounding boxes, bounded differences, octagons, grids,
... all of them can be used as arguments to the powerset construction.

So, let us start with your question.  Premise number 1 is that I am
not against providing `omega_reduce()' to the user of Polyhedra_Powerset.
Premise number 2 is that I prefer to be extra-sure providing
`omega_reduce()' to the user of Polyhedra_Powerset is the right thing
to do.  The obvious question I have to ask you is: why would you want
to have access to `omega_reduce()?  What is the effect you wish to
obtain?  Afterall, one may say that a Polyhedra_Powerset and its
omega-reduced counterparts have the same semantics.  (You can
of course reply, and rightly so, "Why do you provide pairwise_reduce()
then?"  This only shows that the interface of powersets needs
more work:  perhaps [I am being provocative here] `pairwise_reduce()'
should not be there.)

To make a parallel with a similar situation with the C_Polyhedron
and NNC_Polyhedron classes, we do not provide a method `minimize()'
to the user.  We rather ask the user to declare what is wanted by
calling `miminized_constraints()' or `minimized_generators()' and
keep polyhedra minimization as an internal business the user needs
not be concerned about.  Up to now, this design choice has proved
its value without showing any drawback.

To come back to the point you raise: is `omega_reduction()' precisely
the things you want, or is it just something that either as a by product
or in combination with other techniques will give you what you really
want?  In the latter case, what is that you really want?  Do you want
reduction to economize memory?  To use less space when printing?
Because you think subsequent operations will be cheaper?

> The only solution I found
> is to use `pairwise_reduce()' instead. It seems to do what I want, but I
> am confused as to the reason for the protected function.

The method `pairwise_reduce()' does a different thing (please consult
the documentation and complain if it does not provide enough information).
And moreover, it is quite expensive.

> Please excuse me (and please tell me!) if this is not the right forum to
> ask these questions.

This is _precisely_ the right forum for these questions.
All the best,

     Roberto

-- 
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it