156 lines
3.4 KiB
Plaintext
156 lines
3.4 KiB
Plaintext
### Sets
|
|
|
|
[
|
|
Type sets
|
|
Funcon set
|
|
Funcon set-elements
|
|
Funcon is-in-set
|
|
Funcon is-subset
|
|
Funcon set-insert
|
|
Funcon set-unite
|
|
Funcon set-intersect
|
|
Funcon set-difference
|
|
Funcon set-size
|
|
Funcon some-element
|
|
Funcon element-not-in
|
|
]
|
|
|
|
|
|
Meta-variables
|
|
GT <: ground-values
|
|
|
|
|
|
Built-in Type
|
|
sets(GT)
|
|
/*
|
|
`sets(GT)` is the type of possibly-empty finite sets `{V1, ..., Vn}`
|
|
where `V1:GT`, ..., `Vn:GT`.
|
|
*/
|
|
|
|
|
|
Built-in Funcon
|
|
set(_:(GT)*) : =>sets(GT)
|
|
/*
|
|
The notation `{V1, ..., Vn}` for `set(V1, ..., Vn)` is built-in.
|
|
*/
|
|
Assert
|
|
{V*:(GT)*} == set(V*)
|
|
/*
|
|
Note that `set(...)` is not a constructor operation. The order and duplicates
|
|
of argument values are ignored (e.g., `{1,2,1}` denotes the same set as `{1,2}`
|
|
and `{2,1}`).
|
|
*/
|
|
|
|
|
|
Built-in Funcon
|
|
set-elements(_:sets(GT)) : =>(GT)*
|
|
/*
|
|
For each set `S`, the sequence of values `V*` returned by `set-elements(S)`
|
|
contains each element of `S` just once. The order of the values in `V*` is
|
|
unspecified, and may vary between sets (e.g., `set-elements{1,2}` could be
|
|
`(1,2)` and `set-elements{1,2,3}` could be `(3,2,1)`).
|
|
*/
|
|
Assert
|
|
set(set-elements(S)) == S
|
|
|
|
|
|
Built-in Funcon
|
|
is-in-set(_:GT, _:sets(GT)) : =>booleans
|
|
/*
|
|
`is-in-set(GV,S)` tests whether `GV` is in the set `S`.
|
|
*/
|
|
Assert
|
|
is-in-set(GV:GT, { }) == false
|
|
Assert
|
|
is-in-set(GV:GT, {GV}:sets(GT)) == true
|
|
|
|
|
|
Built-in Funcon
|
|
is-subset(_:sets(GT), _:sets(GT)) : =>booleans
|
|
/*
|
|
`is-subset(S1,S2)` tests whether `S1` is a subset of `S2`.
|
|
*/
|
|
Assert
|
|
is-subset({ }, S:sets(GT)) == true
|
|
Assert
|
|
is-subset(S:sets(GT), S) == true
|
|
|
|
|
|
Built-in Funcon
|
|
set-insert(_:GT, _:sets(GT)) : =>sets(GT)
|
|
/*
|
|
`set-insert(GV, S)` returns the set union of `{GV}` and `S`.
|
|
*/
|
|
Assert
|
|
is-in-set(GV:GT, set-insert(GV:GT, S:sets(GT))) == true
|
|
|
|
|
|
Built-in Funcon
|
|
set-unite(_:(sets(GT))*) : =>sets(GT)
|
|
/*
|
|
`set-unite(...)` unites a sequence of sets.
|
|
*/
|
|
Assert
|
|
set-unite(S:sets(GT), S) == S
|
|
Assert
|
|
set-unite(S1:sets(GT), S2:sets(GT)) == set-unite(S2, S1)
|
|
Assert
|
|
set-unite(S1:sets(GT), set-unite(S2:sets(GT), S3:sets(GT))) ==
|
|
set-unite(set-unite(S1, S2), S3)
|
|
Assert
|
|
set-unite(S1:sets(GT), S2:sets(GT), S3:sets(GT)) ==
|
|
set-unite(S1, set-unite(S2, S3))
|
|
Assert
|
|
set-unite(S:sets(GT)) == S
|
|
Assert
|
|
set-unite( ) == { }
|
|
|
|
|
|
Built-in Funcon
|
|
set-intersect(_:(sets(GT))+) : =>sets(GT)
|
|
/*
|
|
`set-intersect(GT,...)` intersects a non-empty sequence of sets.
|
|
*/
|
|
Assert
|
|
set-intersect(S:sets(GT), S) == S
|
|
Assert
|
|
set-intersect(S1:sets(GT), S2:sets(GT)) == set-intersect(S2, S1)
|
|
Assert
|
|
set-intersect(S1:sets(GT), set-intersect(S2:sets(GT), S3:sets(GT))) ==
|
|
set-intersect(set-intersect(S1, S2), S3)
|
|
Assert
|
|
set-intersect(S1:sets(GT), S2:sets(GT), S3:sets(GT)) ==
|
|
set-intersect(S1, set-intersect(S2, S3))
|
|
Assert
|
|
set-intersect(S:sets(GT)) == S
|
|
|
|
|
|
Built-in Funcon
|
|
set-difference(_:sets(GT), _:sets(GT)) : =>sets(GT)
|
|
/*
|
|
`set-difference(S1, S2)` returns the set containing those elements of `S1`
|
|
that are not in `S2`.
|
|
*/
|
|
|
|
Built-in Funcon
|
|
set-size(_:sets(GT)) : =>natural-numbers
|
|
Assert
|
|
set-size(S:sets(GT)) == length(set-elements(S))
|
|
|
|
|
|
Funcon
|
|
some-element(_:sets(GT)) : =>GT?
|
|
Assert
|
|
some-element(S:sets(GT)) == index(1, set-elements(S))
|
|
Assert
|
|
some-element{ } == ( )
|
|
|
|
|
|
Built-in Funcon
|
|
element-not-in(GT:types, _:set(GT)) : =>GT?
|
|
/*
|
|
`element-not-in(GT, S)` gives an element of the type `GT` not in the set
|
|
`S`, or `( )` when `S` is empty. When the set of elements of `GT` is infinite,
|
|
`element-not-in(GT, S)` never gives `( )`.
|
|
*/
|