1sofs(3) Erlang Module Definition sofs(3)
2
6 sofs - Functions for manipulating sets of sets.
7
9 This module provides operations on finite sets and relations repre‐
10 sented as sets. Intuitively, a set is a collection of elements; every
11 element belongs to the set, and the set contains every element.
12 Given a set A and a sentence S(x), where x is a free variable, a new
14 set B whose elements are exactly those elements of A for which S(x)
15 holds can be formed, this is denoted B = {x in A : S(x)}. Sentences are
16 expressed using the logical operators "for some" (or "there exists"),
17 "for all", "and", "or", "not". If the existence of a set containing all
18 the specified elements is known (as is always the case in this module),
19 this is denoted B = {x : S(x)}.
20 * The unordered set containing the elements a, b, and c is denoted
22 {a, b, c}. This notation is not to be confused with tuples.
23 The ordered pair of a and b, with first coordinate a and second co‐
25 ordinate b, is denoted (a, b). An ordered pair is an ordered set of
26 two elements. In this module, ordered sets can contain one, two, or
27 more elements, and parentheses are used to enclose the elements.
28 Unordered sets and ordered sets are orthogonal, again in this mod‐
30 ule; there is no unordered set equal to any ordered set.
31 * The empty set contains no elements.
33 Set A is equal to set B if they contain the same elements, which is
35 denoted A = B. Two ordered sets are equal if they contain the same
36 number of elements and have equal elements at each coordinate.
37 Set B is a subset of set A if A contains all elements that B con‐
39 tains.
40 The union of two sets A and B is the smallest set that contains all
42 elements of A and all elements of B.
43 The intersection of two sets A and B is the set that contains all
45 elements of A that belong to B.
46 Two sets are disjoint if their intersection is the empty set.
48 The difference of two sets A and B is the set that contains all el‐
50 ements of A that do not belong to B.
51 The symmetric difference of two sets is the set that contains those
53 element that belong to either of the two sets, but not both.
54 The union of a collection of sets is the smallest set that contains
56 all the elements that belong to at least one set of the collection.
57 The intersection of a non-empty collection of sets is the set that
59 contains all elements that belong to every set of the collection.
60 * The Cartesian product of two sets X and Y, denoted X x Y, is the
62 set {a : a = (x, y) for some x in X and for some y in Y}.
63 A relation is a subset of X x Y. Let R be a relation. The fact that
65 (x, y) belongs to R is written as x R y. As relations are sets, the
66 definitions of the last item (subset, union, and so on) apply to
67 relations as well.
68 The domain of R is the set {x : x R y for some y in Y}.
70 The range of R is the set {y : x R y for some x in X}.
72 The converse of R is the set {a : a = (y, x) for some (x, y) in R}.
74 If A is a subset of X, the image of A under R is the set {y : x R y
76 for some x in A}. If B is a subset of Y, the inverse image of B is
77 the set {x : x R y for some y in B}.
78 If R is a relation from X to Y, and S is a relation from Y to Z,
80 the relative product of R and S is the relation T from X to Z de‐
81 fined so that x T z if and only if there exists an element y in Y
82 such that x R y and y S z.
83 The restriction of R to A is the set S defined so that x S y if and
85 only if there exists an element x in A such that x R y.
86 If S is a restriction of R to A, then R is an extension of S to X.
88 If X = Y, then R is called a relation in X.
90 The field of a relation R in X is the union of the domain of R and
92 the range of R.
93 If R is a relation in X, and if S is defined so that x S y if x R y
95 and not x = y, then S is the strict relation corresponding to R.
96 Conversely, if S is a relation in X, and if R is defined so that x
97 R y if x S y or x = y, then R is the weak relation corresponding to
98 S.
99 A relation R in X is reflexive if x R x for every element x of X,
101 it is symmetric if x R y implies that y R x, and it is transitive
102 if x R y and y R z imply that x R z.
103 * A function F is a relation, a subset of X x Y, such that the domain
105 of F is equal to X and such that for every x in X there is a unique
106 element y in Y with (x, y) in F. The latter condition can be formu‐
107 lated as follows: if x F y and x F z, then y = z. In this module,
108 it is not required that the domain of F is equal to X for a rela‐
109 tion to be considered a function.
110 Instead of writing (x, y) in F or x F y, we write F(x) = y when F
112 is a function, and say that F maps x onto y, or that the value of F
113 at x is y.
114 As functions are relations, the definitions of the last item (do‐
116 main, range, and so on) apply to functions as well.
117 If the converse of a function F is a function F', then F' is called
119 the inverse of F.
120 The relative product of two functions F1 and F2 is called the com‐
122 posite of F1 and F2 if the range of F1 is a subset of the domain of
123 F2.
124 * Sometimes, when the range of a function is more important than the
126 function itself, the function is called a family.
127 The domain of a family is called the index set, and the range is
129 called the indexed set.
130 If x is a family from I to X, then x[i] denotes the value of the
132 function at index i. The notation "a family in X" is used for such
133 a family.
134 When the indexed set is a set of subsets of a set X, we call x a
136 family of subsets of X.
137 If x is a family of subsets of X, the union of the range of x is
139 called the union of the family x.
140 If x is non-empty (the index set is non-empty), the intersection of
142 the family x is the intersection of the range of x.
143 In this module, the only families that are considered are families
145 of subsets of some set X; in the following, the word "family" is
146 used for such families of subsets.
147 * A partition of a set X is a collection S of non-empty subsets of X
149 whose union is X and whose elements are pairwise disjoint.
150 A relation in a set is an equivalence relation if it is reflexive,
152 symmetric, and transitive.
153 If R is an equivalence relation in X, and x is an element of X, the
155 equivalence class of x with respect to R is the set of all those
156 elements y of X for which x R y holds. The equivalence classes con‐
157 stitute a partitioning of X. Conversely, if C is a partition of X,
158 the relation that holds for any two elements of X if they belong to
159 the same equivalence class, is an equivalence relation induced by
160 the partition C.
161 If R is an equivalence relation in X, the canonical map is the
163 function that maps every element of X onto its equivalence class.
164 * Relations as defined above (as sets of ordered pairs) are from now
166 on referred to as binary relations.
167 We call a set of ordered sets (x[1], ..., x[n]) an (n-ary) rela‐
169 tion, and say that the relation is a subset of the Cartesian prod‐
170 uct X[1] x ... x X[n], where x[i] is an element of X[i], 1 <= i <=
171 n.
172 The projection of an n-ary relation R onto coordinate i is the set
174 {x[i] : (x[1], ..., x[i], ..., x[n]) in R for some x[j] in X[j], 1
175 <= j <= n and not i = j}. The projections of a binary relation R
176 onto the first and second coordinates are the domain and the range
177 of R, respectively.
178 The relative product of binary relations can be generalized to n-
180 ary relations as follows. Let TR be an ordered set (R[1], ...,
181 R[n]) of binary relations from X to Y[i] and S a binary relation
182 from (Y[1] x ... x Y[n]) to Z. The relative product of TR and S is
183 the binary relation T from X to Z defined so that x T z if and only
184 if there exists an element y[i] in Y[i] for each 1 <= i <= n such
185 that x R[i] y[i] and (y[1], ..., y[n]) S z. Now let TR be a an or‐
186 dered set (R[1], ..., R[n]) of binary relations from X[i] to Y[i]
187 and S a subset of X[1] x ... x X[n]. The multiple relative product
188 of TR and S is defined to be the set {z : z = ((x[1], ..., x[n]),
189 (y[1],...,y[n])) for some (x[1], ..., x[n]) in S and for some
190 (x[i], y[i]) in R[i], 1 <= i <= n}.
191 The natural join of an n-ary relation R and an m-ary relation S on
193 coordinate i and j is defined to be the set {z : z = (x[1], ...,
194 x[n], y[1], ..., y[j-1], y[j+1], ..., y[m]) for some (x[1], ...,
195 x[n]) in R and for some (y[1], ..., y[m]) in S such that x[i] =
196 y[j]}.
197 * The sets recognized by this module are represented by elements of
199 the relation Sets, which is defined as the smallest set such that:
200 * For every atom T, except '_', and for every term X, (T, X) be‐
202 longs to Sets (atomic sets).
203 * (['_'], []) belongs to Sets (the untyped empty set).
205 * For every tuple T = {T[1], ..., T[n]} and for every tuple X =
207 {X[1], ..., X[n]}, if (T[i], X[i]) belongs to Sets for every 1 <=
208 i <= n, then (T, X) belongs to Sets (ordered sets).
209 * For every term T, if X is the empty list or a non-empty sorted
211 list [X[1], ..., X[n]] without duplicates such that (T, X[i]) be‐
212 longs to Sets for every 1 <= i <= n, then ([T], X) belongs to
213 Sets (typed unordered sets).
214 An external set is an element of the range of Sets.
216 A type is an element of the domain of Sets.
218 If S is an element (T, X) of Sets, then T is a valid type of X, T
220 is the type of S, and X is the external set of S. from_term/2 cre‐
221 ates a set from a type and an Erlang term turned into an external
222 set.
223 The sets represented by Sets are the elements of the range of func‐
225 tion Set from Sets to Erlang terms and sets of Erlang terms:
226 * Set(T,Term) = Term, where T is an atom
228 * Set({T[1], ..., T[n]}, {X[1], ..., X[n]}) = (Set(T[1], X[1]),
230 ..., Set(T[n], X[n]))
231 * Set([T], [X[1], ..., X[n]]) = {Set(T, X[1]), ..., Set(T, X[n])}
233 * Set([T], []) = {}
235 When there is no risk of confusion, elements of Sets are identified
237 with the sets they represent. For example, if U is the result of
238 calling union/2 with S1 and S2 as arguments, then U is said to be
239 the union of S1 and S2. A more precise formulation is that Set(U)
240 is the union of Set(S1) and Set(S2).
241 The types are used to implement the various conditions that sets must
243 fulfill. As an example, consider the relative product of two sets R and
244 S, and recall that the relative product of R and S is defined if R is a
245 binary relation to Y and S is a binary relation from Y. The function
246 that implements the relative product, relative_product/2, checks that
247 the arguments represent binary relations by matching [{A,B}] against
248 the type of the first argument (Arg1 say), and [{C,D}] against the type
249 of the second argument (Arg2 say). The fact that [{A,B}] matches the
250 type of Arg1 is to be interpreted as Arg1 representing a binary rela‐
251 tion from X to Y, where X is defined as all sets Set(x) for some ele‐
252 ment x in Sets the type of which is A, and similarly for Y. In the same
253 way Arg2 is interpreted as representing a binary relation from W to Z.
254 Finally it is checked that B matches C, which is sufficient to ensure
255 that W is equal to Y. The untyped empty set is handled separately: its
256 type, ['_'], matches the type of any unordered set.
257 A few functions of this module (drestriction/3, family_projection/2,
259 partition/2, partition_family/2, projection/2, restriction/3, substitu‐
260 tion/2) accept an Erlang function as a means to modify each element of
261 a given unordered set. Such a function, called SetFun in the following,
262 can be specified as a functional object (fun), a tuple {external, Fun},
263 or an integer:
264 * If SetFun is specified as a fun, the fun is applied to each element
266 of the given set and the return value is assumed to be a set.
267 * If SetFun is specified as a tuple {external, Fun}, Fun is applied
269 to the external set of each element of the given set and the return
270 value is assumed to be an external set. Selecting the elements of
271 an unordered set as external sets and assembling a new unordered
272 set from a list of external sets is in the present implementation
273 more efficient than modifying each element as a set. However, this
274 optimization can only be used when the elements of the unordered
275 set are atomic or ordered sets. It must also be the case that the
276 type of the elements matches some clause of Fun (the type of the
277 created set is the result of applying Fun to the type of the given
278 set), and that Fun does nothing but selecting, duplicating, or re‐
279 arranging parts of the elements.
280 * Specifying a SetFun as an integer I is equivalent to specifying
282 {external, fun(X) -> element(I, X) end}, but is to be preferred, as
283 it makes it possible to handle this case even more efficiently.
284 Examples of SetFuns:
286 fun sofs:union/1
288 fun(S) -> sofs:partition(1, S) end
289 {external, fun(A) -> A end}
290 {external, fun({A,_,C}) -> {C,A} end}
291 {external, fun({_,{_,C}}) -> C end}
292 {external, fun({_,{_,{_,E}=C}}) -> {E,{E,C}} end}
293 2
294 The order in which a SetFun is applied to the elements of an unordered
296 set is not specified, and can change in future versions of this module.
297 The execution time of the functions of this module is dominated by the
299 time it takes to sort lists. When no sorting is needed, the execution
300 time is in the worst case proportional to the sum of the sizes of the
301 input arguments and the returned value. A few functions execute in con‐
302 stant time: from_external/2, is_empty_set/1, is_set/1, is_sofs_set/1,
303 to_external/1 type/1.
304 The functions of this module exit the process with a badarg, bad_func‐
306 tion, or type_mismatch message when given badly formed arguments or
307 sets the types of which are not compatible.
308 When comparing external sets, operator ==/2 is used.
310
312 anyset() = ordset() | a_set()
313 Any kind of set (also included are the atomic sets).
315 binary_relation() = relation()
317 A binary relation.
319 external_set() = term()
321 An external set.
323 family() = a_function()
325 A family (of subsets).
327 a_function() = relation()
329 A function.
331 ordset()
333 An ordered set.
335 relation() = a_set()
337 An n-ary relation.
339 a_set()
341 An unordered set.
343 set_of_sets() = a_set()
345 An unordered set of unordered sets.
347 set_fun() =
349 integer() >= 1 |
350 {external, fun((external_set()) -> external_set())} |
351 fun((anyset()) -> anyset())
352 A SetFun.
354 spec_fun() =
356 {external, fun((external_set()) -> boolean())} |
357 fun((anyset()) -> boolean())
358 type() = term()
360 A type.
362 tuple_of(T)
364 A tuple where the elements are of type T.
366
368 a_function(Tuples) -> Function
369 a_function(Tuples, Type) -> Function
371 Types:
373 Function = a_function()
375 Tuples = [tuple()]
376 Type = type()
377 Creates a function. a_function(F, T) is equivalent to
379 from_term(F, T) if the result is a function. If no type is ex‐
380 plicitly specified, [{atom, atom}] is used as the function type.
381 canonical_relation(SetOfSets) -> BinRel
383 Types:
385 BinRel = binary_relation()
387 SetOfSets = set_of_sets()
388 Returns the binary relation containing the elements (E, Set)
390 such that Set belongs to SetOfSets and E belongs to Set. If
391 SetOfSets is a partition of a set X and R is the equivalence re‐
392 lation in X induced by SetOfSets, then the returned relation is
393 the canonical map from X onto the equivalence classes with re‐
394 spect to R.
395 1> Ss = sofs:from_term([[a,b],[b,c]]),
397 CR = sofs:canonical_relation(Ss),
398 sofs:to_external(CR).
399 [{a,[a,b]},{b,[a,b]},{b,[b,c]},{c,[b,c]}]
400 composite(Function1, Function2) -> Function3
402 Types:
404 Function1 = Function2 = Function3 = a_function()
406 Returns the composite of the functions Function1 and Function2.
408 1> F1 = sofs:a_function([{a,1},{b,2},{c,2}]),
410 F2 = sofs:a_function([{1,x},{2,y},{3,z}]),
411 F = sofs:composite(F1, F2),
412 sofs:to_external(F).
413 [{a,x},{b,y},{c,y}]
414 constant_function(Set, AnySet) -> Function
416 Types:
418 AnySet = anyset()
420 Function = a_function()
421 Set = a_set()
422 Creates the function that maps each element of set Set onto Any‐
424 Set.
425 1> S = sofs:set([a,b]),
427 E = sofs:from_term(1),
428 R = sofs:constant_function(S, E),
429 sofs:to_external(R).
430 [{a,1},{b,1}]
431 converse(BinRel1) -> BinRel2
433 Types:
435 BinRel1 = BinRel2 = binary_relation()
437 Returns the converse of the binary relation BinRel1.
439 1> R1 = sofs:relation([{1,a},{2,b},{3,a}]),
441 R2 = sofs:converse(R1),
442 sofs:to_external(R2).
443 [{a,1},{a,3},{b,2}]
444 difference(Set1, Set2) -> Set3
446 Types:
448 Set1 = Set2 = Set3 = a_set()
450 Returns the difference of the sets Set1 and Set2.
452 digraph_to_family(Graph) -> Family
454 digraph_to_family(Graph, Type) -> Family
456 Types:
458 Graph = digraph:graph()
460 Family = family()
461 Type = type()
462 Creates a family from the directed graph Graph. Each vertex a of
464 Graph is represented by a pair (a, {b[1], ..., b[n]}), where the
465 b[i]:s are the out-neighbors of a. If no type is explicitly
466 specified, [{atom, [atom]}] is used as type of the family. It is
467 assumed that Type is a valid type of the external set of the
468 family.
469 If G is a directed graph, it holds that the vertices and edges
471 of G are the same as the vertices and edges of family_to_di‐
472 graph(digraph_to_family(G)).
473 domain(BinRel) -> Set
475 Types:
477 BinRel = binary_relation()
479 Set = a_set()
480 Returns the domain of the binary relation BinRel.
482 1> R = sofs:relation([{1,a},{1,b},{2,b},{2,c}]),
484 S = sofs:domain(R),
485 sofs:to_external(S).
486 [1,2]
487 drestriction(BinRel1, Set) -> BinRel2
489 Types:
491 BinRel1 = BinRel2 = binary_relation()
493 Set = a_set()
494 Returns the difference between the binary relation BinRel1 and
496 the restriction of BinRel1 to Set.
497 1> R1 = sofs:relation([{1,a},{2,b},{3,c}]),
499 S = sofs:set([2,4,6]),
500 R2 = sofs:drestriction(R1, S),
501 sofs:to_external(R2).
502 [{1,a},{3,c}]
503 drestriction(R, S) is equivalent to difference(R, restriction(R,
505 S)).
506 drestriction(SetFun, Set1, Set2) -> Set3
508 Types:
510 SetFun = set_fun()
512 Set1 = Set2 = Set3 = a_set()
513 Returns a subset of Set1 containing those elements that do not
515 give an element in Set2 as the result of applying SetFun.
516 1> SetFun = {external, fun({_A,B,C}) -> {B,C} end},
518 R1 = sofs:relation([{a,aa,1},{b,bb,2},{c,cc,3}]),
519 R2 = sofs:relation([{bb,2},{cc,3},{dd,4}]),
520 R3 = sofs:drestriction(SetFun, R1, R2),
521 sofs:to_external(R3).
522 [{a,aa,1}]
523 drestriction(F, S1, S2) is equivalent to difference(S1, restric‐
525 tion(F, S1, S2)).
526 empty_set() -> Set
528 Types:
530 Set = a_set()
532 Returns the untyped empty set. empty_set() is equivalent to
534 from_term([], ['_']).
535 extension(BinRel1, Set, AnySet) -> BinRel2
537 Types:
539 AnySet = anyset()
541 BinRel1 = BinRel2 = binary_relation()
542 Set = a_set()
543 Returns the extension of BinRel1 such that for each element E in
545 Set that does not belong to the domain of BinRel1, BinRel2 con‐
546 tains the pair (E, AnySet).
547 1> S = sofs:set([b,c]),
549 A = sofs:empty_set(),
550 R = sofs:family([{a,[1,2]},{b,[3]}]),
551 X = sofs:extension(R, S, A),
552 sofs:to_external(X).
553 [{a,[1,2]},{b,[3]},{c,[]}]
554 family(Tuples) -> Family
556 family(Tuples, Type) -> Family
558 Types:
560 Family = family()
562 Tuples = [tuple()]
563 Type = type()
564 Creates a family of subsets. family(F, T) is equivalent to
566 from_term(F, T) if the result is a family. If no type is explic‐
567 itly specified, [{atom, [atom]}] is used as the family type.
568 family_difference(Family1, Family2) -> Family3
570 Types:
572 Family1 = Family2 = Family3 = family()
574 If Family1 and Family2 are families, then Family3 is the family
576 such that the index set is equal to the index set of Family1,
577 and Family3[i] is the difference between Family1[i] and Fam‐
578 ily2[i] if Family2 maps i, otherwise Family1[i].
579 1> F1 = sofs:family([{a,[1,2]},{b,[3,4]}]),
581 F2 = sofs:family([{b,[4,5]},{c,[6,7]}]),
582 F3 = sofs:family_difference(F1, F2),
583 sofs:to_external(F3).
584 [{a,[1,2]},{b,[3]}]
585 family_domain(Family1) -> Family2
587 Types:
589 Family1 = Family2 = family()
591 If Family1 is a family and Family1[i] is a binary relation for
593 every i in the index set of Family1, then Family2 is the family
594 with the same index set as Family1 such that Family2[i] is the
595 domain of Family1[i].
596 1> FR = sofs:from_term([{a,[{1,a},{2,b},{3,c}]},{b,[]},{c,[{4,d},{5,e}]}]),
598 F = sofs:family_domain(FR),
599 sofs:to_external(F).
600 [{a,[1,2,3]},{b,[]},{c,[4,5]}]
601 family_field(Family1) -> Family2
603 Types:
605 Family1 = Family2 = family()
607 If Family1 is a family and Family1[i] is a binary relation for
609 every i in the index set of Family1, then Family2 is the family
610 with the same index set as Family1 such that Family2[i] is the
611 field of Family1[i].
612 1> FR = sofs:from_term([{a,[{1,a},{2,b},{3,c}]},{b,[]},{c,[{4,d},{5,e}]}]),
614 F = sofs:family_field(FR),
615 sofs:to_external(F).
616 [{a,[1,2,3,a,b,c]},{b,[]},{c,[4,5,d,e]}]
617 family_field(Family1) is equivalent to family_union(family_do‐
619 main(Family1), family_range(Family1)).
620 family_intersection(Family1) -> Family2
622 Types:
624 Family1 = Family2 = family()
626 If Family1 is a family and Family1[i] is a set of sets for every
628 i in the index set of Family1, then Family2 is the family with
629 the same index set as Family1 such that Family2[i] is the inter‐
630 section of Family1[i].
631 If Family1[i] is an empty set for some i, the process exits with
633 a badarg message.
634 1> F1 = sofs:from_term([{a,[[1,2,3],[2,3,4]]},{b,[[x,y,z],[x,y]]}]),
636 F2 = sofs:family_intersection(F1),
637 sofs:to_external(F2).
638 [{a,[2,3]},{b,[x,y]}]
639 family_intersection(Family1, Family2) -> Family3
641 Types:
643 Family1 = Family2 = Family3 = family()
645 If Family1 and Family2 are families, then Family3 is the family
647 such that the index set is the intersection of Family1:s and
648 Family2:s index sets, and Family3[i] is the intersection of Fam‐
649 ily1[i] and Family2[i].
650 1> F1 = sofs:family([{a,[1,2]},{b,[3,4]},{c,[5,6]}]),
652 F2 = sofs:family([{b,[4,5]},{c,[7,8]},{d,[9,10]}]),
653 F3 = sofs:family_intersection(F1, F2),
654 sofs:to_external(F3).
655 [{b,[4]},{c,[]}]
656 family_projection(SetFun, Family1) -> Family2
658 Types:
660 SetFun = set_fun()
662 Family1 = Family2 = family()
663 If Family1 is a family, then Family2 is the family with the same
665 index set as Family1 such that Family2[i] is the result of call‐
666 ing SetFun with Family1[i] as argument.
667 1> F1 = sofs:from_term([{a,[[1,2],[2,3]]},{b,[[]]}]),
669 F2 = sofs:family_projection(fun sofs:union/1, F1),
670 sofs:to_external(F2).
671 [{a,[1,2,3]},{b,[]}]
672 family_range(Family1) -> Family2
674 Types:
676 Family1 = Family2 = family()
678 If Family1 is a family and Family1[i] is a binary relation for
680 every i in the index set of Family1, then Family2 is the family
681 with the same index set as Family1 such that Family2[i] is the
682 range of Family1[i].
683 1> FR = sofs:from_term([{a,[{1,a},{2,b},{3,c}]},{b,[]},{c,[{4,d},{5,e}]}]),
685 F = sofs:family_range(FR),
686 sofs:to_external(F).
687 [{a,[a,b,c]},{b,[]},{c,[d,e]}]
688 family_specification(Fun, Family1) -> Family2
690 Types:
692 Fun = spec_fun()
694 Family1 = Family2 = family()
695 If Family1 is a family, then Family2 is the restriction of Fam‐
697 ily1 to those elements i of the index set for which Fun applied
698 to Family1[i] returns true. If Fun is a tuple {external, Fun2},
699 then Fun2 is applied to the external set of Family1[i], other‐
700 wise Fun is applied to Family1[i].
701 1> F1 = sofs:family([{a,[1,2,3]},{b,[1,2]},{c,[1]}]),
703 SpecFun = fun(S) -> sofs:no_elements(S) =:= 2 end,
704 F2 = sofs:family_specification(SpecFun, F1),
705 sofs:to_external(F2).
706 [{b,[1,2]}]
707 family_to_digraph(Family) -> Graph
709 family_to_digraph(Family, GraphType) -> Graph
711 Types:
713 Graph = digraph:graph()
715 Family = family()
716 GraphType = [digraph:d_type()]
717 Creates a directed graph from family Family. For each pair (a,
719 {b[1], ..., b[n]}) of Family, vertex a and the edges (a, b[i])
720 for 1 <= i <= n are added to a newly created directed graph.
721 If no graph type is specified, digraph:new/0 is used for creat‐
723 ing the directed graph, otherwise argument GraphType is passed
724 on as second argument to digraph:new/1.
725 It F is a family, it holds that F is a subset of digraph_to_fam‐
727 ily(family_to_digraph(F), type(F)). Equality holds if
728 union_of_family(F) is a subset of domain(F).
729 Creating a cycle in an acyclic graph exits the process with a
731 cyclic message.
732 family_to_relation(Family) -> BinRel
734 Types:
736 Family = family()
738 BinRel = binary_relation()
739 If Family is a family, then BinRel is the binary relation con‐
741 taining all pairs (i, x) such that i belongs to the index set of
742 Family and x belongs to Family[i].
743 1> F = sofs:family([{a,[]}, {b,[1]}, {c,[2,3]}]),
745 R = sofs:family_to_relation(F),
746 sofs:to_external(R).
747 [{b,1},{c,2},{c,3}]
748 family_union(Family1) -> Family2
750 Types:
752 Family1 = Family2 = family()
754 If Family1 is a family and Family1[i] is a set of sets for each
756 i in the index set of Family1, then Family2 is the family with
757 the same index set as Family1 such that Family2[i] is the union
758 of Family1[i].
759 1> F1 = sofs:from_term([{a,[[1,2],[2,3]]},{b,[[]]}]),
761 F2 = sofs:family_union(F1),
762 sofs:to_external(F2).
763 [{a,[1,2,3]},{b,[]}]
764 family_union(F) is equivalent to family_projection(fun
766 sofs:union/1, F).
767 family_union(Family1, Family2) -> Family3
769 Types:
771 Family1 = Family2 = Family3 = family()
773 If Family1 and Family2 are families, then Family3 is the family
775 such that the index set is the union of Family1:s and Family2:s
776 index sets, and Family3[i] is the union of Family1[i] and Fam‐
777 ily2[i] if both map i, otherwise Family1[i] or Family2[i].
778 1> F1 = sofs:family([{a,[1,2]},{b,[3,4]},{c,[5,6]}]),
780 F2 = sofs:family([{b,[4,5]},{c,[7,8]},{d,[9,10]}]),
781 F3 = sofs:family_union(F1, F2),
782 sofs:to_external(F3).
783 [{a,[1,2]},{b,[3,4,5]},{c,[5,6,7,8]},{d,[9,10]}]
784 field(BinRel) -> Set
786 Types:
788 BinRel = binary_relation()
790 Set = a_set()
791 Returns the field of the binary relation BinRel.
793 1> R = sofs:relation([{1,a},{1,b},{2,b},{2,c}]),
795 S = sofs:field(R),
796 sofs:to_external(S).
797 [1,2,a,b,c]
798 field(R) is equivalent to union(domain(R), range(R)).
800 from_external(ExternalSet, Type) -> AnySet
802 Types:
804 ExternalSet = external_set()
806 AnySet = anyset()
807 Type = type()
808 Creates a set from the external set ExternalSet and the type
810 Type. It is assumed that Type is a valid type of ExternalSet.
811 from_sets(ListOfSets) -> Set
813 Types:
815 Set = a_set()
817 ListOfSets = [anyset()]
818 Returns the unordered set containing the sets of list ListOf‐
820 Sets.
821 1> S1 = sofs:relation([{a,1},{b,2}]),
823 S2 = sofs:relation([{x,3},{y,4}]),
824 S = sofs:from_sets([S1,S2]),
825 sofs:to_external(S).
826 [[{a,1},{b,2}],[{x,3},{y,4}]]
827 from_sets(TupleOfSets) -> Ordset
829 Types:
831 Ordset = ordset()
833 TupleOfSets = tuple_of(anyset())
834 Returns the ordered set containing the sets of the non-empty tu‐
836 ple TupleOfSets.
837 from_term(Term) -> AnySet
839 from_term(Term, Type) -> AnySet
841 Types:
843 AnySet = anyset()
845 Term = term()
846 Type = type()
847 Creates an element of Sets by traversing term Term, sorting
849 lists, removing duplicates, and deriving or verifying a valid
850 type for the so obtained external set. An explicitly specified
851 type Type can be used to limit the depth of the traversal; an
852 atomic type stops the traversal, as shown by the following exam‐
853 ple where "foo" and {"foo"} are left unmodified:
854 1> S = sofs:from_term([{{"foo"},[1,1]},{"foo",[2,2]}], [{atom,[atom]}]),
856 sofs:to_external(S).
857 [{{"foo"},[1]},{"foo",[2]}]
858 from_term can be used for creating atomic or ordered sets. The
860 only purpose of such a set is that of later building unordered
861 sets, as all functions in this module that do anything operate
862 on unordered sets. Creating unordered sets from a collection of
863 ordered sets can be the way to go if the ordered sets are big
864 and one does not want to waste heap by rebuilding the elements
865 of the unordered set. The following example shows that a set can
866 be built "layer by layer":
867 1> A = sofs:from_term(a),
869 S = sofs:set([1,2,3]),
870 P1 = sofs:from_sets({A,S}),
871 P2 = sofs:from_term({b,[6,5,4]}),
872 Ss = sofs:from_sets([P1,P2]),
873 sofs:to_external(Ss).
874 [{a,[1,2,3]},{b,[4,5,6]}]
875 Other functions that create sets are from_external/2 and
877 from_sets/1. Special cases of from_term/2 are a_function/1,2,
878 empty_set/0, family/1,2, relation/1,2, and set/1,2.
879 image(BinRel, Set1) -> Set2
881 Types:
883 BinRel = binary_relation()
885 Set1 = Set2 = a_set()
886 Returns the image of set Set1 under the binary relation BinRel.
888 1> R = sofs:relation([{1,a},{2,b},{2,c},{3,d}]),
890 S1 = sofs:set([1,2]),
891 S2 = sofs:image(R, S1),
892 sofs:to_external(S2).
893 [a,b,c]
894 intersection(SetOfSets) -> Set
896 Types:
898 Set = a_set()
900 SetOfSets = set_of_sets()
901 Returns the intersection of the set of sets SetOfSets.
903 Intersecting an empty set of sets exits the process with a
905 badarg message.
906 intersection(Set1, Set2) -> Set3
908 Types:
910 Set1 = Set2 = Set3 = a_set()
912 Returns the intersection of Set1 and Set2.
914 intersection_of_family(Family) -> Set
916 Types:
918 Family = family()
920 Set = a_set()
921 Returns the intersection of family Family.
923 Intersecting an empty family exits the process with a badarg
925 message.
926 1> F = sofs:family([{a,[0,2,4]},{b,[0,1,2]},{c,[2,3]}]),
928 S = sofs:intersection_of_family(F),
929 sofs:to_external(S).
930 [2]
931 inverse(Function1) -> Function2
933 Types:
935 Function1 = Function2 = a_function()
937 Returns the inverse of function Function1.
939 1> R1 = sofs:relation([{1,a},{2,b},{3,c}]),
941 R2 = sofs:inverse(R1),
942 sofs:to_external(R2).
943 [{a,1},{b,2},{c,3}]
944 inverse_image(BinRel, Set1) -> Set2
946 Types:
948 BinRel = binary_relation()
950 Set1 = Set2 = a_set()
951 Returns the inverse image of Set1 under the binary relation Bin‐
953 Rel.
954 1> R = sofs:relation([{1,a},{2,b},{2,c},{3,d}]),
956 S1 = sofs:set([c,d,e]),
957 S2 = sofs:inverse_image(R, S1),
958 sofs:to_external(S2).
959 [2,3]
960 is_a_function(BinRel) -> Bool
962 Types:
964 Bool = boolean()
966 BinRel = binary_relation()
967 Returns true if the binary relation BinRel is a function or the
969 untyped empty set, otherwise false.
970 is_disjoint(Set1, Set2) -> Bool
972 Types:
974 Bool = boolean()
976 Set1 = Set2 = a_set()
977 Returns true if Set1 and Set2 are disjoint, otherwise false.
979 is_empty_set(AnySet) -> Bool
981 Types:
983 AnySet = anyset()
985 Bool = boolean()
986 Returns true if AnySet is an empty unordered set, otherwise
988 false.
989 is_equal(AnySet1, AnySet2) -> Bool
991 Types:
993 AnySet1 = AnySet2 = anyset()
995 Bool = boolean()
996 Returns true if AnySet1 and AnySet2 are equal, otherwise false.
998 The following example shows that ==/2 is used when comparing
999 sets for equality:
1000 1> S1 = sofs:set([1.0]),
1002 S2 = sofs:set([1]),
1003 sofs:is_equal(S1, S2).
1004 true
1005 is_set(AnySet) -> Bool
1007 Types:
1009 AnySet = anyset()
1011 Bool = boolean()
1012 Returns true if AnySet is an unordered set, and false if AnySet
1014 is an ordered set or an atomic set.
1015 is_sofs_set(Term) -> Bool
1017 Types:
1019 Bool = boolean()
1021 Term = term()
1022 Returns true if Term is an unordered set, an ordered set, or an
1024 atomic set, otherwise false.
1025 is_subset(Set1, Set2) -> Bool
1027 Types:
1029 Bool = boolean()
1031 Set1 = Set2 = a_set()
1032 Returns true if Set1 is a subset of Set2, otherwise false.
1034 is_type(Term) -> Bool
1036 Types:
1038 Bool = boolean()
1040 Term = term()
1041 Returns true if term Term is a type.
1043 join(Relation1, I, Relation2, J) -> Relation3
1045 Types:
1047 Relation1 = Relation2 = Relation3 = relation()
1049 I = J = integer() >= 1
1050 Returns the natural join of the relations Relation1 and Rela‐
1052 tion2 on coordinates I and J.
1053 1> R1 = sofs:relation([{a,x,1},{b,y,2}]),
1055 R2 = sofs:relation([{1,f,g},{1,h,i},{2,3,4}]),
1056 J = sofs:join(R1, 3, R2, 1),
1057 sofs:to_external(J).
1058 [{a,x,1,f,g},{a,x,1,h,i},{b,y,2,3,4}]
1059 multiple_relative_product(TupleOfBinRels, BinRel1) -> BinRel2
1061 Types:
1063 TupleOfBinRels = tuple_of(BinRel)
1065 BinRel = BinRel1 = BinRel2 = binary_relation()
1066 If TupleOfBinRels is a non-empty tuple {R[1], ..., R[n]} of bi‐
1068 nary relations and BinRel1 is a binary relation, then BinRel2 is
1069 the multiple relative product of the ordered set (R[i], ...,
1070 R[n]) and BinRel1.
1071 1> Ri = sofs:relation([{a,1},{b,2},{c,3}]),
1073 R = sofs:relation([{a,b},{b,c},{c,a}]),
1074 MP = sofs:multiple_relative_product({Ri, Ri}, R),
1075 sofs:to_external(sofs:range(MP)).
1076 [{1,2},{2,3},{3,1}]
1077 no_elements(ASet) -> NoElements
1079 Types:
1081 ASet = a_set() | ordset()
1083 NoElements = integer() >= 0
1084 Returns the number of elements of the ordered or unordered set
1086 ASet.
1087 partition(SetOfSets) -> Partition
1089 Types:
1091 SetOfSets = set_of_sets()
1093 Partition = a_set()
1094 Returns the partition of the union of the set of sets SetOfSets
1096 such that two elements are considered equal if they belong to
1097 the same elements of SetOfSets.
1098 1> Sets1 = sofs:from_term([[a,b,c],[d,e,f],[g,h,i]]),
1100 Sets2 = sofs:from_term([[b,c,d],[e,f,g],[h,i,j]]),
1101 P = sofs:partition(sofs:union(Sets1, Sets2)),
1102 sofs:to_external(P).
1103 [[a],[b,c],[d],[e,f],[g],[h,i],[j]]
1104 partition(SetFun, Set) -> Partition
1106 Types:
1108 SetFun = set_fun()
1110 Partition = Set = a_set()
1111 Returns the partition of Set such that two elements are consid‐
1113 ered equal if the results of applying SetFun are equal.
1114 1> Ss = sofs:from_term([[a],[b],[c,d],[e,f]]),
1116 SetFun = fun(S) -> sofs:from_term(sofs:no_elements(S)) end,
1117 P = sofs:partition(SetFun, Ss),
1118 sofs:to_external(P).
1119 [[[a],[b]],[[c,d],[e,f]]]
1120 partition(SetFun, Set1, Set2) -> {Set3, Set4}
1122 Types:
1124 SetFun = set_fun()
1126 Set1 = Set2 = Set3 = Set4 = a_set()
1127 Returns a pair of sets that, regarded as constituting a set,
1129 forms a partition of Set1. If the result of applying SetFun to
1130 an element of Set1 gives an element in Set2, the element belongs
1131 to Set3, otherwise the element belongs to Set4.
1132 1> R1 = sofs:relation([{1,a},{2,b},{3,c}]),
1134 S = sofs:set([2,4,6]),
1135 {R2,R3} = sofs:partition(1, R1, S),
1136 {sofs:to_external(R2),sofs:to_external(R3)}.
1137 {[{2,b}],[{1,a},{3,c}]}
1138 partition(F, S1, S2) is equivalent to {restriction(F, S1, S2),
1140 drestriction(F, S1, S2)}.
1141 partition_family(SetFun, Set) -> Family
1143 Types:
1145 Family = family()
1147 SetFun = set_fun()
1148 Set = a_set()
1149 Returns family Family where the indexed set is a partition of
1151 Set such that two elements are considered equal if the results
1152 of applying SetFun are the same value i. This i is the index
1153 that Family maps onto the equivalence class.
1154 1> S = sofs:relation([{a,a,a,a},{a,a,b,b},{a,b,b,b}]),
1156 SetFun = {external, fun({A,_,C,_}) -> {A,C} end},
1157 F = sofs:partition_family(SetFun, S),
1158 sofs:to_external(F).
1159 [{{a,a},[{a,a,a,a}]},{{a,b},[{a,a,b,b},{a,b,b,b}]}]
1160 product(TupleOfSets) -> Relation
1162 Types:
1164 Relation = relation()
1166 TupleOfSets = tuple_of(a_set())
1167 Returns the Cartesian product of the non-empty tuple of sets Tu‐
1169 pleOfSets. If (x[1], ..., x[n]) is an element of the n-ary rela‐
1170 tion Relation, then x[i] is drawn from element i of TupleOfSets.
1171 1> S1 = sofs:set([a,b]),
1173 S2 = sofs:set([1,2]),
1174 S3 = sofs:set([x,y]),
1175 P3 = sofs:product({S1,S2,S3}),
1176 sofs:to_external(P3).
1177 [{a,1,x},{a,1,y},{a,2,x},{a,2,y},{b,1,x},{b,1,y},{b,2,x},{b,2,y}]
1178 product(Set1, Set2) -> BinRel
1180 Types:
1182 BinRel = binary_relation()
1184 Set1 = Set2 = a_set()
1185 Returns the Cartesian product of Set1 and Set2.
1187 1> S1 = sofs:set([1,2]),
1189 S2 = sofs:set([a,b]),
1190 R = sofs:product(S1, S2),
1191 sofs:to_external(R).
1192 [{1,a},{1,b},{2,a},{2,b}]
1193 product(S1, S2) is equivalent to product({S1, S2}).
1195 projection(SetFun, Set1) -> Set2
1197 Types:
1199 SetFun = set_fun()
1201 Set1 = Set2 = a_set()
1202 Returns the set created by substituting each element of Set1 by
1204 the result of applying SetFun to the element.
1205 If SetFun is a number i >= 1 and Set1 is a relation, then the
1207 returned set is the projection of Set1 onto coordinate i.
1208 1> S1 = sofs:from_term([{1,a},{2,b},{3,a}]),
1210 S2 = sofs:projection(2, S1),
1211 sofs:to_external(S2).
1212 [a,b]
1213 range(BinRel) -> Set
1215 Types:
1217 BinRel = binary_relation()
1219 Set = a_set()
1220 Returns the range of the binary relation BinRel.
1222 1> R = sofs:relation([{1,a},{1,b},{2,b},{2,c}]),
1224 S = sofs:range(R),
1225 sofs:to_external(S).
1226 [a,b,c]
1227 relation(Tuples) -> Relation
1229 relation(Tuples, Type) -> Relation
1231 Types:
1233 N = integer()
1235 Type = N | type()
1236 Relation = relation()
1237 Tuples = [tuple()]
1238 Creates a relation. relation(R, T) is equivalent to from_term(R,
1240 T), if T is a type and the result is a relation. If Type is an
1241 integer N, then [{atom, ..., atom}]), where the tuple size is N,
1242 is used as type of the relation. If no type is explicitly speci‐
1243 fied, the size of the first tuple of Tuples is used if there is
1244 such a tuple. relation([]) is equivalent to relation([], 2).
1245 relation_to_family(BinRel) -> Family
1247 Types:
1249 Family = family()
1251 BinRel = binary_relation()
1252 Returns family Family such that the index set is equal to the
1254 domain of the binary relation BinRel, and Family[i] is the image
1255 of the set of i under BinRel.
1256 1> R = sofs:relation([{b,1},{c,2},{c,3}]),
1258 F = sofs:relation_to_family(R),
1259 sofs:to_external(F).
1260 [{b,[1]},{c,[2,3]}]
1261 relative_product(ListOfBinRels) -> BinRel2
1263 relative_product(ListOfBinRels, BinRel1) -> BinRel2
1265 Types:
1267 ListOfBinRels = [BinRel, ...]
1269 BinRel = BinRel1 = BinRel2 = binary_relation()
1270 If ListOfBinRels is a non-empty list [R[1], ..., R[n]] of binary
1272 relations and BinRel1 is a binary relation, then BinRel2 is the
1273 relative product of the ordered set (R[i], ..., R[n]) and Bin‐
1274 Rel1.
1275 If BinRel1 is omitted, the relation of equality between the ele‐
1277 ments of the Cartesian product of the ranges of R[i], range R[1]
1278 x ... x range R[n], is used instead (intuitively, nothing is
1279 "lost").
1280 1> TR = sofs:relation([{1,a},{1,aa},{2,b}]),
1282 R1 = sofs:relation([{1,u},{2,v},{3,c}]),
1283 R2 = sofs:relative_product([TR, R1]),
1284 sofs:to_external(R2).
1285 [{1,{a,u}},{1,{aa,u}},{2,{b,v}}]
1286 Notice that relative_product([R1], R2) is different from rela‐
1288 tive_product(R1, R2); the list of one element is not identified
1289 with the element itself.
1290 relative_product(BinRel1, BinRel2) -> BinRel3
1292 Types:
1294 BinRel1 = BinRel2 = BinRel3 = binary_relation()
1296 Returns the relative product of the binary relations BinRel1 and
1298 BinRel2.
1299 relative_product1(BinRel1, BinRel2) -> BinRel3
1301 Types:
1303 BinRel1 = BinRel2 = BinRel3 = binary_relation()
1305 Returns the relative product of the converse of the binary rela‐
1307 tion BinRel1 and the binary relation BinRel2.
1308 1> R1 = sofs:relation([{1,a},{1,aa},{2,b}]),
1310 R2 = sofs:relation([{1,u},{2,v},{3,c}]),
1311 R3 = sofs:relative_product1(R1, R2),
1312 sofs:to_external(R3).
1313 [{a,u},{aa,u},{b,v}]
1314 relative_product1(R1, R2) is equivalent to relative_product(con‐
1316 verse(R1), R2).
1317 restriction(BinRel1, Set) -> BinRel2
1319 Types:
1321 BinRel1 = BinRel2 = binary_relation()
1323 Set = a_set()
1324 Returns the restriction of the binary relation BinRel1 to Set.
1326 1> R1 = sofs:relation([{1,a},{2,b},{3,c}]),
1328 S = sofs:set([1,2,4]),
1329 R2 = sofs:restriction(R1, S),
1330 sofs:to_external(R2).
1331 [{1,a},{2,b}]
1332 restriction(SetFun, Set1, Set2) -> Set3
1334 Types:
1336 SetFun = set_fun()
1338 Set1 = Set2 = Set3 = a_set()
1339 Returns a subset of Set1 containing those elements that gives an
1341 element in Set2 as the result of applying SetFun.
1342 1> S1 = sofs:relation([{1,a},{2,b},{3,c}]),
1344 S2 = sofs:set([b,c,d]),
1345 S3 = sofs:restriction(2, S1, S2),
1346 sofs:to_external(S3).
1347 [{2,b},{3,c}]
1348 set(Terms) -> Set
1350 set(Terms, Type) -> Set
1352 Types:
1354 Set = a_set()
1356 Terms = [term()]
1357 Type = type()
1358 Creates an unordered set. set(L, T) is equivalent to
1360 from_term(L, T), if the result is an unordered set. If no type
1361 is explicitly specified, [atom] is used as the set type.
1362 specification(Fun, Set1) -> Set2
1364 Types:
1366 Fun = spec_fun()
1368 Set1 = Set2 = a_set()
1369 Returns the set containing every element of Set1 for which Fun
1371 returns true. If Fun is a tuple {external, Fun2}, Fun2 is ap‐
1372 plied to the external set of each element, otherwise Fun is ap‐
1373 plied to each element.
1374 1> R1 = sofs:relation([{a,1},{b,2}]),
1376 R2 = sofs:relation([{x,1},{x,2},{y,3}]),
1377 S1 = sofs:from_sets([R1,R2]),
1378 S2 = sofs:specification(fun sofs:is_a_function/1, S1),
1379 sofs:to_external(S2).
1380 [[{a,1},{b,2}]]
1381 strict_relation(BinRel1) -> BinRel2
1383 Types:
1385 BinRel1 = BinRel2 = binary_relation()
1387 Returns the strict relation corresponding to the binary relation
1389 BinRel1.
1390 1> R1 = sofs:relation([{1,1},{1,2},{2,1},{2,2}]),
1392 R2 = sofs:strict_relation(R1),
1393 sofs:to_external(R2).
1394 [{1,2},{2,1}]
1395 substitution(SetFun, Set1) -> Set2
1397 Types:
1399 SetFun = set_fun()
1401 Set1 = Set2 = a_set()
1402 Returns a function, the domain of which is Set1. The value of an
1404 element of the domain is the result of applying SetFun to the
1405 element.
1406 1> L = [{a,1},{b,2}].
1408 [{a,1},{b,2}]
1409 2> sofs:to_external(sofs:projection(1,sofs:relation(L))).
1410 [a,b]
1411 3> sofs:to_external(sofs:substitution(1,sofs:relation(L))).
1412 [{{a,1},a},{{b,2},b}]
1413 4> SetFun = {external, fun({A,_}=E) -> {E,A} end},
1414 sofs:to_external(sofs:projection(SetFun,sofs:relation(L))).
1415 [{{a,1},a},{{b,2},b}]
1416 The relation of equality between the elements of {a,b,c}:
1418 1> I = sofs:substitution(fun(A) -> A end, sofs:set([a,b,c])),
1420 sofs:to_external(I).
1421 [{a,a},{b,b},{c,c}]
1422 Let SetOfSets be a set of sets and BinRel a binary relation. The
1424 function that maps each element Set of SetOfSets onto the image
1425 of Set under BinRel is returned by the following function:
1426 images(SetOfSets, BinRel) ->
1428 Fun = fun(Set) -> sofs:image(BinRel, Set) end,
1429 sofs:substitution(Fun, SetOfSets).
1430 External unordered sets are represented as sorted lists. So,
1432 creating the image of a set under a relation R can traverse all
1433 elements of R (to that comes the sorting of results, the image).
1434 In image/2, BinRel is traversed once for each element of SetOf‐
1435 Sets, which can take too long. The following efficient function
1436 can be used instead under the assumption that the image of each
1437 element of SetOfSets under BinRel is non-empty:
1438 images2(SetOfSets, BinRel) ->
1440 CR = sofs:canonical_relation(SetOfSets),
1441 R = sofs:relative_product1(CR, BinRel),
1442 sofs:relation_to_family(R).
1443 symdiff(Set1, Set2) -> Set3
1445 Types:
1447 Set1 = Set2 = Set3 = a_set()
1449 Returns the symmetric difference (or the Boolean sum) of Set1
1451 and Set2.
1452 1> S1 = sofs:set([1,2,3]),
1454 S2 = sofs:set([2,3,4]),
1455 P = sofs:symdiff(S1, S2),
1456 sofs:to_external(P).
1457 [1,4]
1458 symmetric_partition(Set1, Set2) -> {Set3, Set4, Set5}
1460 Types:
1462 Set1 = Set2 = Set3 = Set4 = Set5 = a_set()
1464 Returns a triple of sets:
1466 * Set3 contains the elements of Set1 that do not belong to
1468 Set2.
1469 * Set4 contains the elements of Set1 that belong to Set2.
1471 * Set5 contains the elements of Set2 that do not belong to
1473 Set1.
1474 to_external(AnySet) -> ExternalSet
1476 Types:
1478 ExternalSet = external_set()
1480 AnySet = anyset()
1481 Returns the external set of an atomic, ordered, or unordered
1483 set.
1484 to_sets(ASet) -> Sets
1486 Types:
1488 ASet = a_set() | ordset()
1490 Sets = tuple_of(AnySet) | [AnySet]
1491 AnySet = anyset()
1492 Returns the elements of the ordered set ASet as a tuple of sets,
1494 and the elements of the unordered set ASet as a sorted list of
1495 sets without duplicates.
1496 type(AnySet) -> Type
1498 Types:
1500 AnySet = anyset()
1502 Type = type()
1503 Returns the type of an atomic, ordered, or unordered set.
1505 union(SetOfSets) -> Set
1507 Types:
1509 Set = a_set()
1511 SetOfSets = set_of_sets()
1512 Returns the union of the set of sets SetOfSets.
1514 union(Set1, Set2) -> Set3
1516 Types:
1518 Set1 = Set2 = Set3 = a_set()
1520 Returns the union of Set1 and Set2.
1522 union_of_family(Family) -> Set
1524 Types:
1526 Family = family()
1528 Set = a_set()
1529 Returns the union of family Family.
1531 1> F = sofs:family([{a,[0,2,4]},{b,[0,1,2]},{c,[2,3]}]),
1533 S = sofs:union_of_family(F),
1534 sofs:to_external(S).
1535 [0,1,2,3,4]
1536 weak_relation(BinRel1) -> BinRel2
1538 Types:
1540 BinRel1 = BinRel2 = binary_relation()
1542 Returns a subset S of the weak relation W corresponding to the
1544 binary relation BinRel1. Let F be the field of BinRel1. The sub‐
1545 set S is defined so that x S y if x W y for some x in F and for
1546 some y in F.
1547 1> R1 = sofs:relation([{1,1},{1,2},{3,1}]),
1549 R2 = sofs:weak_relation(R1),
1550 sofs:to_external(R2).
1551 [{1,1},{1,2},{2,2},{3,1},{3,3}]
1552
1554 dict(3), digraph(3), orddict(3), ordsets(3), sets(3)
1555Ericsson AB stdlib 3.17.2 sofs(3)