Rel Module
signature REL
structure Rel :> REL
This module provides various operations on finite relations, i.e., finite sets of ordered pairs.
type ('a,'b) rel = ('a * 'b) Set.set
val domain : 'a Sort.total_ordering -> ('a, 'b) rel -> 'a Set.set
val range : 'b Sort.total_ordering -> ('a, 'b) rel -> 'b Set.set
val relationFromTo : 'a Sort.total_ordering * 'b Sort.total_ordering
-> ('a, 'b) rel * 'a Set.set * 'b Set.set -> bool
val relationOn : 'a Sort.total_ordering -> ('a, 'a) rel * 'a Set.set -> bool
val apply : 'a Sort.total_ordering * 'b Sort.total_ordering
-> ('a, 'b) rel * 'a Set.set -> 'b Set.set
val reflexive : 'a Sort.total_ordering -> ('a, 'a) rel * 'a Set.set -> bool
val symmetric : 'a Sort.total_ordering -> ('a, 'a) rel -> bool
val antisymmetric : 'a Sort.total_ordering -> ('a, 'a) rel -> bool
val transitive : 'a Sort.total_ordering -> ('a, 'a) rel -> bool
val total : 'a Sort.total_ordering -> ('a, 'a) rel * 'a Set.set -> bool
val inverse : 'a Sort.total_ordering * 'b Sort.total_ordering
-> ('a, 'b) rel -> ('b, 'a) rel
val reflexiveClosure : 'a Sort.total_ordering
-> ('a, 'a) rel * 'a Set.set -> ('a, 'a) rel
val transitiveClosure : 'a Sort.total_ordering -> ('a, 'a) rel -> ('a, 'a) rel
val reflexiveTransitiveClosure : 'a Sort.total_ordering
-> ('a, 'a) rel * 'a Set.set -> ('a, 'a) rel
val symmetricClosure : 'a Sort.total_ordering -> ('a, 'a) rel -> ('a, 'a) rel
val transitiveSymmetricClosure : 'a Sort.total_ordering -> ('a, 'a) rel -> ('a, 'a) rel
val reflexiveTransitiveSymmetricClosure : 'a Sort.total_ordering
-> ('a, 'a) rel * 'a Set.set -> ('a, 'a) rel
val compose : 'a Sort.total_ordering * 'b Sort.total_ordering * 'c Sort.total_ordering
-> ('b, 'c) rel * ('a, 'b) rel -> ('a, 'c) rel
val function : 'a Sort.total_ordering -> ('a, 'b) rel -> bool
val functionFromTo : 'a Sort.total_ordering * 'b Sort.total_ordering
-> ('a, 'b) rel * 'a Set.set * 'b Set.set -> bool
val injection : 'a Sort.total_ordering * 'b Sort.total_ordering -> ('a, 'b) rel -> bool
val bijectionFromTo : 'a Sort.total_ordering * 'b Sort.total_ordering
-> ('a, 'b) rel * 'a Set.set * 'b Set.set -> bool
val bijectionFromAvoiding : 'a Sort.total_ordering * 'b Sort.total_ordering
-> ('a, 'b) rel * 'a Set.set * 'b Set.set -> bool
val bijectionFromSupersetAvoiding : 'a Sort.total_ordering * 'b Sort.total_ordering
-> ('a, 'b) rel * 'a Set.set * 'b Set.set -> bool
val applyFunction : 'a Sort.total_ordering -> ('a, 'b) rel -> 'a -> 'b
val restrictFunction : 'a Sort.total_ordering * 'b Sort.total_ordering
-> ('a, 'b) rel * 'a Set.set -> ('a, 'b) rel
val updateFunction : 'a Sort.total_ordering * 'b Sort.total_ordering
-> ('a, 'b) rel * 'a * 'b -> ('a, 'b) rel
val mlFunctionToFunction : 'a Sort.total_ordering * 'b Sort.total_ordering
-> ('a -> 'b) * 'a Set.set -> ('a, 'b) rel
type ('a,'b) rel = ('a * 'b) Set.set
'a to values of type 'b, i.e., finite sets of values of type 'a * 'b.
The module's values are specified with the help of the abstract proposition saying that a value rel of type ('a, 'b)rel is compatible with a value cmp of type 'a Sort.total_ordering and a value cmp' of type 'b Sort.total_ordering.
In a context where we know that a value rel of type ('a, 'b)rel is compatible with a values cmp and cmp' of types 'a Sort.total_ordering and 'b Sort.total_ordering, respectively, when we say that (x, y) is an element (or member) of rel, this means that x and y are values of types 'a and 'b, respectively, such that Set.memb (Set.comparePair(cmp, cmp'))
((x, y), rel).
domain cmp rel
rel is compatible with cmp and a value cmp' of type 'b Sort.total_ordering, then domain returns the set that is compatible with cmp and is the domain of rel.
range cmp' rel
rel is compatible with a value cmp of type 'a Sort.total_ordering and cmp', then range returns the set that is compatible with cmp' and is the range of rel.
relationFromTo (cmp, cmp') (rel, xs, ys)
rel is compatible with cmp and cmp', xs is compatible with cmp, and ys is compatible with cmp', then relationFromTo tests whether rel is a relation from xs to ys.
relationOn cmp (rel, xs)
rel is compatible with cmp and cmp, and xs is compatible with cmp, then relationOn tests whether rel is a relation on xs.
apply (cmp, cmp') (rel, xs)
rel is compatible with cmp and cmp', and xs is compatible with cmp, then apply returns the set that is compatible with cmp' and whose elements are all those values y of type 'b such that there is a value x of type 'a such that x is a member of xs and (x, y) is a member of rel.
reflexive cmp (rel, xs)
rel is compatible with cmp and cmp, and xs is compatible with cmp, then reflexive tests whether rel is reflexive on xs.
symmetric cmp rel
rel is compatible with cmp and cmp, then symmetric tests whether rel is symmetric.
antisymmetric cmp rel
rel is compatible with cmp and cmp, then antisymmetric tests whether rel is antisymmetric.
transitive cmp rel
rel is compatible with cmp and cmp, then symmetric tests whether rel is transitive.
total cmp (rel, xs)
rel is compatible with cmp and cmp, and xs is compatible with cmp, then total tests whether rel is total on xs.
inverse (cmp, cmp') rel
rel is compatible with cmp and cmp', then inverse returns the inverse of rel, which is compatible with cmp' and cmp.
reflexiveClosure cmp (rel, xs)
rel is compatible with cmp and cmp, and xs is compatible with cmp, then reflexiveClosure returns the relation that is compatible with cmp and cmp and is the reflexive closure of rel with respect to xs.
transitiveClosure cmp rel
rel is compatible with cmp and cmp, then transitiveClosure returns the relation that is compatible with cmp and cmp and is the transitive closure of rel.
reflexiveTransitiveClosure cmp (rel, xs)
rel is compatible with cmp and cmp, and xs is compatible with cmp, then reflexiveTransitiveClosure returns the relation that is compatible with cmp and and cmp and is the reflexive, transitive closure of rel with respect to xs.
symmetricClosure cmp rel
rel is compatible with cmp and cmp, then symmetricClosure returns the relation that is compatible with cmp and cmp and is the symmetric closure of rel.
transitiveSymmetricClosure cmp rel
rel is compatible with cmp and cmp, then transitiveSymmetricClosure returns the relation that is compatible with cmp and cmp and is the transitive, symmetric closure of rel.
reflexiveTransitiveSymmetricClosure cmp (rel, xs)
rel is compatible with cmp and cmp, and xs is compatible with cmp, then reflexiveTransitiveSymmetricClosure returns the relation that is compatible with cmp and cmp and is the reflexive, transitive, symmetric closure of rel with respect to xs.
compose (cmp, cmp', cmp'') (rel2, rel1)
rel2 is compatible with cmp' and cmp'', and rel1 is compatible with cmp and cmp', then compose returns the relation that is compatible with cmp and cmp'' and is the composition of rel2 and rel1.
function cmp rel
rel is compatible with cmp and a value cmp' of type 'a Sort.total_ordering, then function tests whether rel is a function.
functionFromTo (cmp, cmp') (rel, xs, ys)
rel is compatible with cmp and cmp', xs is compatible with cmp, and ys is compatible with cmp', then functionFromTo tests whether rel is a function from xs to ys.
injection (cmp, cmp') rel
rel is compatible with cmp and cmp', then injection tests whether rel is an injection.
bijectionFromTo (cmp, cmp') (rel, xs, ys)
rel is compatible with cmp and cmp', xs is compatible with cmp, and ys is compatible with cmp', then bijectionFromTo tests whether rel is a bijection from xs to ys.
bijectionFromAvoiding (cmp, cmp') (rel, xs, ys)
rel is compatible with cmp and cmp', xs is compatible with cmp, and ys is compatible with cmp', then bijectionFromAvoiding tests whether rel is a bijection from xs to a set that is disjoint from ys.
bijectionFromSupersetAvoiding (cmp, cmp') (rel, xs, ys)
rel is compatible with cmp and cmp', xs is compatible with cmp, and ys is compatible with cmp', then bijectionFromSupersetAvoiding tests whether rel is a bijection from a superset of xs to a set that is disjoint from ys.
applyFunction cmp (rel, x)
rel is compatible with cmp and a value cmp' of type 'b Sort.total_ordering, then applyFunction applies the function rel to x. It issues an error message if rel is not a function, or if x is not in the domain of rel.
restrictFunction (cmp, cmp') (rel, xs)
rel is compatible with cmp and cmp', and xs is compatible with cmp, then restrictFunction returns the function that is compatible with cmp and cmp' and is the restriction of rel to xs. Issues an error message if rel isn't a function, or if xs isn't a subset of the domain of rel.
updateFunction (cmp, cmp') (rel, x, y)
rel is compatible with cmp and cmp', then updateFunction returns the function that is compatible with cmp and cmp' and is the updating of the function rel to send x to y. Issues an error message if rel isn't a function.
mlFunctionToFunction (cmp, cmp') (f, xs)
xs is compatible with cmp, then mlFunctionToFunction returns the function rel that is compatible with cmp and cmp', whose domain is xs, and where, for all elements x of xs, (x, f x) is a member of rel. Issues an error message if f raises an exception when called on one or more elements of xs. (Will fail to terminate, if f fails to terminate when called on one or more elements of xs.)
Forlan Version 4.15
Copyright © 2022 Alley Stoughton