Forlan Manual

The `Set` Module

Synopsis

signature SET structure Set :> SET

This module implements an abstract type of finite sets.

Interface

type 'a set val memb : 'a Sort.total_ordering -> 'a * 'a set -> bool val fromList : 'a Sort.total_ordering -> 'a list -> 'a set val toList : 'a set -> 'a list val isEmpty : 'a set -> bool val isNonEmpty : 'a set -> bool val size : 'a set -> int val hd : 'a set -> 'a val tl : 'a set -> 'a set val compare : 'a Sort.total_ordering -> 'a set * 'a set -> order val subset : 'a Sort.total_ordering -> 'a set * 'a set -> bool val equal : 'a Sort.total_ordering -> 'a set * 'a set -> bool val all : ('a -> bool) -> 'a set -> bool val exists : ('a -> bool) -> 'a set -> bool val empty : 'a set val sing : 'a -> 'a set val filter : ('a -> bool) -> 'a set -> 'a set val partition : ('a -> bool) -> 'a set -> 'a set * 'a set val position : ('a -> bool) -> 'a set -> int option val map : 'b Sort.total_ordering -> ('a -> 'b) -> 'a set -> 'b set val mapFromList : 'b Sort.total_ordering -> ('a -> 'b) -> 'a list -> 'b set val mapToList : ('a -> 'b) -> 'a set -> 'b list val union : 'a Sort.total_ordering -> 'a set * 'a set -> 'a set val genUnion : 'a Sort.total_ordering -> 'a set list -> 'a set val inter : 'a Sort.total_ordering -> 'a set * 'a set -> 'a set val genInter : 'a Sort.total_ordering -> 'a set list -> 'a set val minus : 'a Sort.total_ordering -> 'a set * 'a set -> 'a set val comparePair : 'a Sort.total_ordering * 'b Sort.total_ordering -> ('a * 'b) Sort.total_ordering val times : 'a set * 'b set -> ('a * 'b) set val compareTriple : 'a Sort.total_ordering * 'b Sort.total_ordering * 'c Sort.total_ordering -> ('a * 'b * 'c) Sort.total_ordering val times3 : 'a set * 'b set * 'c set -> ('a * 'b * 'c) set val compareList : 'a Sort.total_ordering -> 'a list Sort.total_ordering val genTimes : 'a set list -> 'a list set

Description

type 'a set

This is the abstract type of finite sets of values of type 'a.

The module's values are specified with the help of the abstract proposition saying that a value xs of type 'a set is compatible with a value cmp of type 'a Sort.total_ordering.

memb cmp (x, ys)

Informally, if ys is compatible with cmp, then memb tests whether x is a member (element) of ys. Formally, memb must be understood in relationship to the specifications of the module's other values.

In a context where we know that a value xs of type 'a set is compatible with a value cmp of type 'a Sort.total_ordering, when we say that x is an element of xs, this means that x is a value of type 'a such that memb cmp (x, xs).

fromList cmp xs

returns the set that is compatible with cmp and whose elements are the elements of xs, i.e., the set ys such that:

for all 1 <= i <= length xs, memb cmp (List.sub(xs, i), ys);
for all values y of type 'a, if memb cmp (y, ys), then there is an 1 <= i <= length xs such that Sort.equal cmp (y, List.sub(xs, i)).

toList xs

If xs is compatible with a value cmp of type 'a Sort.total_ordering, then toList returns the list consisting of the elements of xs, listed in strictly ascending order according to cmp, i.e., the list ys such that:

Sort.sorted (false, cmp) ys;
for all values x of type 'a, if memb cmp (x, xs), then there is an 1 <= i <= length ys such that Sort.equal cmp (x, List.sub(ys, i));
for all 1 <= i <= length ys, memb cmp (List.sub(ys, i), xs).

isEmpty xs

If xs is compatible with a value cmp of type 'a Sort.total_ordering, then isEmpty tests whether xs is empty, i.e., whether there is no value x of type 'a such that memb cmp (x, xs).

isNonEmpty xs

If xs is compatible with a value cmp of type 'a Sort.total_ordering, then isNonEmpty tests whether xs is nonempty, i.e., whether there is a value x of type 'a such that memb cmp (x, xs).

size xs

If xs is compatible with a value cmp of type 'a Sort.total_ordering, then size returns the size of xs, i.e., the length of toList xs.

hd xs

If xs is compatible with a value cmp of type 'a Sort.total_ordering, then hd returns the head of xs, i.e., the first element of toList xs. It raises Empty if this list is empty.

tl xs

If xs is compatible with a value cmp of type 'a Sort.total_ordering, then tl returns the tail of xs, i.e., fromList cmp (tl(toList xs)). It raises Empty if toList xs is the empty list.

compare cmp (xs, ys)

If xs and ys are compatible with cmp, then compare first compares size xs and size ys, returning LESS if the former is less than the latter, and GREATER if the former is greater than the latter. If the sizes are equal, it works through the corresponding elements of toList xs and toList ys, using cmp to compare those elements, until a result of LESS or GREATER is found, in which case that result in returned. If all comparisons result in EQUAL, then compare returns EQUAL.

Unfortunately, compare cmp isn't an 'a Sort.total_ordering. But does satisfy the formulas of the definition of 'a set Sort.total_ordering for all values xs, ys and zs of type 'a set that are compatible with cmp. In addition, we have that compare cmp (xs, ys) = EQUAL iff equal cmp (xs, ys), where the function equal is specified below.

subset cmp (xs, ys)

If xs and ys are compatible with cmp, then subset tests whether xs is a subset of ys, i.e., whether, for all values z of type 'a, if memb cmp (z, xs), then memb cmp (z, ys).

equal cmp (xs, ys)

If xs and ys are compatible with cmp, then equal tests whether xs is equal to ys, i.e., whether, for all values z of type 'a, memb cmp (z, xs) iff memb cmp (z, ys).

all f xs

If xs is compatible with a value cmp of type 'a Sort.total_ordering, then all tests whether, for all elements x of xs, f x, i.e., whether, for all values x of type 'a, if

memb cmp (x,
xs)

, then f x.

exists f xs

If xs is compatible with a value cmp of type 'a Sort.total_ordering, then exists tests whether, there is an element x of xs such that f x, i.e., whether there is a value x of type 'a such that

memb cmp (x,
xs)

and f x.

empty

If cmp is a value of type 'a Sort.total_ordering, then empty is the set that is compatible with cmp and has no elements, i.e., the set xs such that there is no value x of 'a such that

memb cmp (x,
xs)

sing x

If cmp is a value of type 'a Sort.total_ordering, then sing returns the set that is compatible with cmp and whose only element is x, i.e., the set ys such that, for all values y of type 'a, memb cmp (y, ys) iff Sort.equal cmp (y, x).

filter f xs

If xs is compatible with a value cmp of type 'a Sort.total_ordering, then filter returns the set that is compatible with cmp and consists of the elements of xs on which f returns true, i.e., the set ys such that, for all values y of type 'a, memb cmp (y, ys) iff memb cmp (y, xs) and f y.

partition f xs

If xs is compatible with a value cmp of type 'a Sort.total_ordering, then filter returns the pair of sets (ys, zs) such that ys and zs are compatible with cmp, ys consists of the elements of xs on which f returns true, and zs consists of the elements of xs on which f returns false, i.e., such that

for all values y of type 'a, memb cmp (y, ys) iff memb cmp (y, xs) and f y;
for all values z of type 'a, memb cmp (z, zs) iff memb cmp (z, xs) and not(f z).

position f xs

If xs is compatible with a value cmp of type 'a Sort.total_ordering, then position behaves the same as ListAux.position f (toList xs).

map cmp' f xs

If cmp is a value of type 'a Sort.total_ordering, cmp' is a value of type 'b Sort.total_ordering, and xs is compatible with cmp, then map returns the set that is compatible with cmp' and consists of the set of all f x such that x is in xs, i.e., the set ys such that, for all values y of type 'b,

memb
cmp' (y, ys)

iff

Sort.equal
cmp' (y, f x)

, for some value x of type 'a such that

memb
cmp (x, xs)

mapFromList cmp f xs

If cmp is a value of type 'b total_ordering, then mapFromList returns fromList cmp (map f xs).

mapToList f xs

If xs is compatible with a value cmp of type 'a Sort.total_ordering, then mapToList returns map f (toList xs).

union cmp (xs, ys)

If xs and ys are compatible with cmp, then union returns the set that is compatible with cmp and is the union of xs and ys, i.e., the set zs such that, for all values z of type 'a, memb cmp (z, zs) iff memb cmp (z, xs) or memb cmp (z, ys).

genUnion cmp xss

If all the elements of xss are compatible with cmp, then genUnion returns the set that is compatible with cmp and is the generalized union of the elements of xss, i.e., the set ys such that, for all values y of type 'a, memb cmp (y, ys) iff there is an element xs of xss such that memb cmp (y, xs).

inter cmp (xs, ys)

If xs and ys are compatible with cmp, then inter returns the set that is compatible with cmp and is the intersection of xs and ys, i.e., the set zs such that, for all values z of type 'a, memb cmp (z, zs) iff memb cmp (z, xs) and memb cmp (z, ys).

genInter cmp xss

If all the elements of xss are compatible with cmp, then genInter returns the set that is compatible with cmp and is the generalized intersection of the elements of xss, i.e., the set ys such that, for all values y of type 'a, memb cmp (y, ys) iff for all elements xs of xss, memb cmp (y, xs). An error message is issued when xss is the empty list.

minus cmp (xs, ys)

If xs and ys are compatible with cmp, then minus returns the set that is compatible with cmp and is the difference of xs and ys, i.e., the set zs such that, for all values z of type 'a, memb cmp (z, zs) iff memb cmp (z, xs) and not(memb cmp (z, ys)).

comparePair (cmp1, cmp2) ((x, y), (x', y'))

works lexicographically, first using cmp1 on (x, x'), and then using cmp2 on (y, y'). I.e., it returns

  case cmp1(x, x') of
       LESS    => LESS
     | EQUAL   => cmp2(y, y')
     | GREATER => GREATER

times(xs, ys)

If xs is compatible with a value cmp1 of type 'a Sort.total_ordering, and ys is compatible with a value cmp2 of type 'b Sort.total_ordering, then times returns the set that is compatible with comparePair(cmp1, cmp2) and is the product of xs and ys, i.e., the set zs such that, for all values p of type 'a * 'b, memb (compairPair(cmp1, cmp2)) (p, zs) iff memb cmp1 (#1 p, xs) and memb cmp2 (#2 p, ys).

compareTriple

is like comparePair, but for triples.

times3

is like times, but for triples, ordered using compareTriple.

compareList cmp (xs, ys)

first compares the lengths of xs and ys, returning LESS, if xs is shorter than ys, and GREATER, if xs is longer than ys. When the lengths are equal, it works lexicographically, using cmp to compare corresponding elements of xs and ys, and yielding the first non-EQUAL result. If all comparisons result in EQUAL, then compareList returns EQUAL.

genTimes xss

If all the elements of xss are compatible with a value cmp of type 'a Sort.total_ordering, then genTimes returns the set that is compatible with compareList cmp and is the generalized product of the elements of xss, i.e., the set yss such that, for all values ys of type 'a list, memb (compareList cmp) (ys, yss) iff length ys = length xss and, for all 1 <= i <= length xss, memb cmp (ListAux.sub(ys, i), ListAux.sub(xss, i)).

[ Top | Parent | Root | Contents | Index ]

Forlan Manual

The Set Module

Synopsis

Interface

Description

The `Set` Module