-------- Original Message -------- Subject: Re: [PPL-devel] Re: PPL and parameters Date: Mon, 9 Feb 2004 12:48:08 +0100 From: Sven Verdoolaege skimo@kotnet.org To: Roberto Bagnara bagnara@cs.unipr.it References: 20040206142357.GK1796@greensroom.kotnet.org 4023E18A.7020208@cs.unipr.it 20040208220817.GD1826@greensroom.kotnet.org 40276EB3.10905@cs.unipr.it

On Mon, Feb 09, 2004 at 12:27:47PM +0100, Roberto Bagnara wrote:

Sven Verdoolaege wrote:

...

The usual. Existentially quantified variables. E.g., { x : \exists a : 4 a + 1 <= x <= 4a + 2 }

The variable `a' is bound to be an integer, right?

Yes.

Am I correct if I say that you are interested in systems of what, IIRC, Masdupuy calls "trapezoid congruences", where a1, ..., an, l, u are rational numbers and k is a natural?

It was just an example. I'm interested in the general case as well. E.g., (Omega notation)

{[dm'] : (Exists k': 32dm' <= 4k'+800j+40000<=32dm'+31 && 0<=i,j,k<=199 && k<k'<=199 && (Exists dm: 32dm <= 800k+4i<=32dm+31 && (Exists x,y: 256x <= dm <= 256x+255 && 256y<= dm'<=256y+255 && 0<=dm-256x = dm'-256y<=255)))};

I'm not sure if that fits "trapezoid congruences". I'd have to look at that concept more closely.

@PhDThesis{Masdupuy93th,

Do you have an electronic copy of that ?

Tell them that, for whoever does a nice job on the subject and is willing to give a seminar, there is a free trip to Parma to be won :-)

I'll keep that in mind.

skimo