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:

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:

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

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 Version 4.12
Copyright © 2019 Alley Stoughton