[Fwd: Re: [PPL-devel] Re: PPL and parameters]

[Roberto Bagnara]

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


-- 
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