[YICES-HELP] Represent a set

[Paulo J. Matos]

On Mon, Dec 1, 2008 at 6:58 PM, Lee Pike <leepike at galois.com> wrote:
> To represent a set, I wouldn't use a datatype but rather a function with
> type T -> BOOLEAN, where T is the type of the elements of the set.  Consider
> for example the following, where I define a closed set of reals.  Of course,
> your set definition can be arbitrarily complex.
>
> set(min : REAL, max : REAL) : [REAL -> BOOLEAN] =
>  {x : REAL |     min <= x
>              AND x <= max
>  };
>

I have come back to this subject after a few months working  on something else.
After looking at this more closely won't this kind of representation,
which seems based on the idea of representing a set using its
characteristic predicate require the use of quantifiers?

Doesn't seem that the top expression is based on yices syntax, so if
it were in yices, quantifiers would have to be involved, right? [given
that I don't think yices supports set comprehension as the one used
above]

Cheers,

Paulo Matos

> Regards,
> Lee
>
>
> On Nov 27, 2008, at 9:07 AM, Paulo J. Matos wrote:
>
>> Hi all,
>>
>> I would like to represent a datatype set in Yices, however, I don't
>> really know what's the best way to approach this.
>> Yices seems to supports lots of datatypes but I can't see the best way
>> to extend any of them to represent sets. For example if I chose arrays
>> (which I think yices support), how would I assure that no element is
>> added twice, since in a set there are no duplicated elements?
>>
>> And by the way, would it be possible for a set to contain itself another
>> set?
>>
>> --
>> Paulo Jorge Matos - pocmatos at gmail.com
>> Webpage: http://www.personal.soton.ac.uk/pocm
>>
>
> --
> Galois, Inc.
> <http://www.galois.com>
> <http://www.cs.indiana.edu/~lepike/>
>
> Phone: +1 503.626.6616 ext. 135
> Fax: +1 503.350.0833
>
>
>
>
>
>
>
>
>
>



-- 
Paulo Jorge Matos - pocmatos at gmail.com
Webpage: http://www.personal.soton.ac.uk/pocm