Powerset Impossibility

[Paulo J. Matos]

Hello all,

I'm 'implementing' several set theory functions in Alloy, some however
seem completely impossible.
Powerset seems to be one of them. Ignoring the fact that the powerset
function generates huge results, how would one generate the powerset
of a set x of Ts?

Let's assume:
sig T {}

one sig X {
    fld : T
}

X would be something like {x -> t1, x -> t2, x -> t3}.
So we define
fun pow [x : T] : set Z {
...
}

where Z would probably be something like:
sig Z {
   t : T
}

The 'correct result' for pow[X] would probably be something line:
{z -> none, z -> t1, z -> t2, z -> t3, z -> t1 -> t2, z -> t1 -> t3, z
-> t2 -> t3, z -> t1 -> t2 -> t3}

Having said this, this is afaik not possible in allow because this
relation has different arity. I guess my only way out would be to
emulate different arity relations using sig extension. Maybe something
like
abstract sig Z { }
sig Z0 extends Z {}
sig Z1 extends Z { t1 : T }
sig Z2 extends Z { t2 : T -> T }
sig Z3 extends Z { t3 : T -> T -> T }

And then having z0, z1, z2 and z3 atoms on the result from pow.

Would such a solution be possible to define in Alloy?

Cheers,
--
Paulo Jorge Matos - pocm at soton.ac.uk
http://www.personal.soton.ac.uk/pocm
PhD Student @ ECS
University of Southampton, UK
Sponsor ECS runners - Action against Hunger:
http://www.justgiving.com/ecsrunslikethewind

[Felix Chang-2]

On Sat, 22 Mar 2008, Paulo J. Matos wrote:
> I'm 'implementing' several set theory functions in Alloy,
> some however seem completely impossible.

Alloy is first order.

Most *realistic* thorems in set theory requires higher order quantification,
or unbounded universe, or infinite universe, or even uncountably
infinite universe.

Please use a theorem prover like Isabel or ACL2 instead.

Sincerely,
Felix Chang
Alloy4 Developer

[pierrekelsen]

If you tell the Analyzer how many subsets there are, you could use
a solution like the following which enumerates all subsets
of A as C-atoms:
-----------------------
sig A { }

sig B { }

sig C { subset: A->one B }

pred C::equals(c:C){all x : A | this.subset[x] = c.subset[x]}

fact { all  disj x,y:C|  not x.equals[y] }

pred show {}
run show for 5 A, exactly 2 B, exactly 32 C
------------------------
Cheers,

-pierre
--- In alloy-discuss@..., "Paulo J. Matos" <pocmatos@...>
wrote:

>
> Hello all,
>
> I'm 'implementing' several set theory functions in Alloy, some however
> seem completely impossible.
> Powerset seems to be one of them. Ignoring the fact that the powerset
> function generates huge results, how would one generate the powerset
> of a set x of Ts?
>
> Let's assume:
> sig T {}
>
> one sig X {
>     fld : T
> }
>
> X would be something like {x -> t1, x -> t2, x -> t3}.
> So we define
> fun pow [x : T] : set Z {
> ...
> }
>
> where Z would probably be something like:
> sig Z {
>    t : T
> }
>
> The 'correct result' for pow[X] would probably be something line:
> {z -> none, z -> t1, z -> t2, z -> t3, z -> t1 -> t2, z -> t1 -> t3, z
> -> t2 -> t3, z -> t1 -> t2 -> t3}
>
> Having said this, this is afaik not possible in allow because this
> relation has different arity. I guess my only way out would be to
> emulate different arity relations using sig extension. Maybe something
> like
> abstract sig Z { }
> sig Z0 extends Z {}
> sig Z1 extends Z { t1 : T }
> sig Z2 extends Z { t2 : T -> T }
> sig Z3 extends Z { t3 : T -> T -> T }
>
> And then having z0, z1, z2 and z3 atoms on the result from pow.
>
> Would such a solution be possible to define in Alloy?
>
> Cheers,
> --
> Paulo Jorge Matos - pocm at soton.ac.uk
> http://www.personal.soton.ac.uk/pocm
> PhD Student @ ECS
> University of Southampton, UK
> Sponsor ECS runners - Action against Hunger:
> http://www.justgiving.com/ecsrunslikethewind
>

[Paulo J. Matos]

On Mon, Mar 24, 2008 at 12:05 PM, pierrekelsen <pierre.kelsen@...> wrote:

>
>
>
>
>
>
> If you tell the Analyzer how many subsets there are, you could use
>  a solution like the following which enumerates all subsets
>  of A as C-atoms:
>  -----------------------
>  sig A { }
>
>  sig B { }
>
>  sig C { subset: A->one B }
>
>  pred C::equals(c:C){all x : A | this.subset[x] = c.subset[x]}
>
>  fact { all disj x,y:C| not x.equals[y] }
>
>  pred show {}
>  run show for 5 A, exactly 2 B, exactly 32 C

Where I assume that Ax -> B0 means that Ax is in the set and Ax -> B1
then, Ax is not in the set, right?

Thanks you,

Paulo Matos

>  ------------------------
>  Cheers,
>
>  -pierre
>  --- In alloy-discuss@..., "Paulo J. Matos" <pocmatos@...>
>  wrote:
>
>
>  >
>  > Hello all,
>  >
>  > I'm 'implementing' several set theory functions in Alloy, some however
>  > seem completely impossible.
>  > Powerset seems to be one of them. Ignoring the fact that the powerset
>  > function generates huge results, how would one generate the powerset
>  > of a set x of Ts?
>  >
>  > Let's assume:
>  > sig T {}
>  >
>  > one sig X {
>  > fld : T
>  > }
>  >
>  > X would be something like {x -> t1, x -> t2, x -> t3}.
>  > So we define
>  > fun pow [x : T] : set Z {
>  > ...
>  > }
>  >
>  > where Z would probably be something like:
>  > sig Z {
>  > t : T
>  > }
>  >
>  > The 'correct result' for pow[X] would probably be something line:
>  > {z -> none, z -> t1, z -> t2, z -> t3, z -> t1 -> t2, z -> t1 -> t3, z
>  > -> t2 -> t3, z -> t1 -> t2 -> t3}
>  >
>  > Having said this, this is afaik not possible in allow because this
>  > relation has different arity. I guess my only way out would be to
>  > emulate different arity relations using sig extension. Maybe something
>  > like
>  > abstract sig Z { }
>  > sig Z0 extends Z {}
>  > sig Z1 extends Z { t1 : T }
>  > sig Z2 extends Z { t2 : T -> T }
>  > sig Z3 extends Z { t3 : T -> T -> T }
>  >
>  > And then having z0, z1, z2 and z3 atoms on the result from pow.
>  >
>  > Would such a solution be possible to define in Alloy?
>  >
>  > Cheers,
>  > --
>  > Paulo Jorge Matos - pocm at soton.ac.uk
>  > http://www.personal.soton.ac.uk/pocm
>  > PhD Student @ ECS
>  > University of Southampton, UK
>  > Sponsor ECS runners - Action against Hunger:
>  > http://www.justgiving.com/ecsrunslikethewind
>  >
>
>  

--
Paulo Jorge Matos - pocm at soton.ac.uk
http://www.personal.soton.ac.uk/pocm
PhD Student @ ECS
University of Southampton, UK
Sponsor ECS runners - Action against Hunger:
http://www.justgiving.com/ecsrunslikethewind

[Felix Chang-2]

On Mon, 24 Mar 2008, pierrekelsen wrote:

> If you tell the Analyzer how many subsets there are, you could use
> a solution like the following which enumerates all subsets
> of A as C-atoms:
> -----------------------
> sig A { }
>
> sig B { }
>
> sig C { subset: A->one B }
>
> pred C::equals(c:C){all x : A | this.subset[x] = c.subset[x]}
>
> fact { all  disj x,y:C|  not x.equals[y] }
>
> pred show {}
> run show for 5 A, exactly 2 B, exactly 32 C

The above formulation uses 24456 vars and 40310 clauses.

You can simplify this as follows:

sig A { }
sig PowerA { value: set A }
fact { all disj x, y: PowerA | x.value != y.value }
run { } for exactly 5 A, exactly 32 PowerA

Then you would not need the extra B sig, and also you can directly
access the subset itself by write ".value" (instead of having
to perform an extra intersection with an B atom).
This new formulation is also more efficient:
7585 vars. 160 primary vars. 13712 clauses

Sincerely,
Felix Chang
Alloy4 Developer

[Paulo J. Matos]

On Mon, Mar 24, 2008 at 12:58 PM, Felix Chang <fschang@...> wrote:

>
>
>
>
>
>
> On Mon, 24 Mar 2008, pierrekelsen wrote:
>  > If you tell the Analyzer how many subsets there are, you could use
>  > a solution like the following which enumerates all subsets
>  > of A as C-atoms:
>  > -----------------------
>  > sig A { }
>  >
>  > sig B { }
>  >
>  > sig C { subset: A->one B }
>  >
>  > pred C::equals(c:C){all x : A | this.subset[x] = c.subset[x]}
>  >
>  > fact { all disj x,y:C| not x.equals[y] }
>  >
>  > pred show {}
>  > run show for 5 A, exactly 2 B, exactly 32 C
>
>  The above formulation uses 24456 vars and 40310 clauses.
>
>  You can simplify this as follows:
>
>  sig A { }
>  sig PowerA { value: set A }
>  fact { all disj x, y: PowerA | x.value != y.value }
>  run { } for exactly 5 A, exactly 32 PowerA
>
>  Then you would not need the extra B sig, and also you can directly
>  access the subset itself by write ".value" (instead of having
>  to perform an extra intersection with an B atom).
>  This new formulation is also more efficient:
>  7585 vars. 160 primary vars. 13712 clauses
>

Thank you very much for the model reformulation.

>
>  Sincerely,
>  Felix Chang
>  Alloy4 Developer
>
>  



--
Paulo Jorge Matos - pocm at soton.ac.uk
http://www.personal.soton.ac.uk/pocm
PhD Student @ ECS
University of Southampton, UK
Sponsor ECS runners - Action against Hunger:
http://www.justgiving.com/ecsrunslikethewind