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
25 coordinate b, is denoted (a, b). An ordered pair is an ordered set
26 of two elements. In this module, ordered sets can contain one, two,
27 or 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
50 elements 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
81 defined 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
116 (domain, 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
186 ordered 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)
202 belongs 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])
212 belongs 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
279 rearranging 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
380 explicitly specified, [{atom, atom}] is used as the function
381 type.
382 canonical_relation(SetOfSets) -> BinRel
384 Types:
386 BinRel = binary_relation()
388 SetOfSets = set_of_sets()
389 Returns the binary relation containing the elements (E, Set)
391 such that Set belongs to SetOfSets and E belongs to Set. If
392 SetOfSets is a partition of a set X and R is the equivalence
393 relation in X induced by SetOfSets, then the returned relation
394 is the canonical map from X onto the equivalence classes with
395 respect to R.
396 1> Ss = sofs:from_term([[a,b],[b,c]]),
398 CR = sofs:canonical_relation(Ss),
399 sofs:to_external(CR).
400 [{a,[a,b]},{b,[a,b]},{b,[b,c]},{c,[b,c]}]
401 composite(Function1, Function2) -> Function3
403 Types:
405 Function1 = Function2 = Function3 = a_function()
407 Returns the composite of the functions Function1 and Function2.
409 1> F1 = sofs:a_function([{a,1},{b,2},{c,2}]),
411 F2 = sofs:a_function([{1,x},{2,y},{3,z}]),
412 F = sofs:composite(F1, F2),
413 sofs:to_external(F).
414 [{a,x},{b,y},{c,y}]
415 constant_function(Set, AnySet) -> Function
417 Types:
419 AnySet = anyset()
421 Function = a_function()
422 Set = a_set()
423 Creates the function that maps each element of set Set onto Any‐
425 Set.
426 1> S = sofs:set([a,b]),
428 E = sofs:from_term(1),
429 R = sofs:constant_function(S, E),
430 sofs:to_external(R).
431 [{a,1},{b,1}]
432 converse(BinRel1) -> BinRel2
434 Types:
436 BinRel1 = BinRel2 = binary_relation()
438 Returns the converse of the binary relation BinRel1.
440 1> R1 = sofs:relation([{1,a},{2,b},{3,a}]),
442 R2 = sofs:converse(R1),
443 sofs:to_external(R2).
444 [{a,1},{a,3},{b,2}]
445 difference(Set1, Set2) -> Set3
447 Types:
449 Set1 = Set2 = Set3 = a_set()
451 Returns the difference of the sets Set1 and Set2.
453 digraph_to_family(Graph) -> Family
455 digraph_to_family(Graph, Type) -> Family
457 Types:
459 Graph = digraph:graph()
461 Family = family()
462 Type = type()
463 Creates a family from the directed graph Graph. Each vertex a of
465 Graph is represented by a pair (a, {b[1], ..., b[n]}), where the
466 b[i]:s are the out-neighbors of a. If no type is explicitly
467 specified, [{atom, [atom]}] is used as type of the family. It is
468 assumed that Type is a valid type of the external set of the
469 family.
470 If G is a directed graph, it holds that the vertices and edges
472 of G are the same as the vertices and edges of fam‐
473 ily_to_digraph(digraph_to_family(G)).
474 domain(BinRel) -> Set
476 Types:
478 BinRel = binary_relation()
480 Set = a_set()
481 Returns the domain of the binary relation BinRel.
483 1> R = sofs:relation([{1,a},{1,b},{2,b},{2,c}]),
485 S = sofs:domain(R),
486 sofs:to_external(S).
487 [1,2]
488 drestriction(BinRel1, Set) -> BinRel2
490 Types:
492 BinRel1 = BinRel2 = binary_relation()
494 Set = a_set()
495 Returns the difference between the binary relation BinRel1 and
497 the restriction of BinRel1 to Set.
498 1> R1 = sofs:relation([{1,a},{2,b},{3,c}]),
500 S = sofs:set([2,4,6]),
501 R2 = sofs:drestriction(R1, S),
502 sofs:to_external(R2).
503 [{1,a},{3,c}]
504 drestriction(R, S) is equivalent to difference(R, restriction(R,
506 S)).
507 drestriction(SetFun, Set1, Set2) -> Set3
509 Types:
511 SetFun = set_fun()
513 Set1 = Set2 = Set3 = a_set()
514 Returns a subset of Set1 containing those elements that do not
516 give an element in Set2 as the result of applying SetFun.
517 1> SetFun = {external, fun({_A,B,C}) -> {B,C} end},
519 R1 = sofs:relation([{a,aa,1},{b,bb,2},{c,cc,3}]),
520 R2 = sofs:relation([{bb,2},{cc,3},{dd,4}]),
521 R3 = sofs:drestriction(SetFun, R1, R2),
522 sofs:to_external(R3).
523 [{a,aa,1}]
524 drestriction(F, S1, S2) is equivalent to difference(S1, restric‐
526 tion(F, S1, S2)).
527 empty_set() -> Set
529 Types:
531 Set = a_set()
533 Returns the untyped empty set. empty_set() is equivalent to
535 from_term([], ['_']).
536 extension(BinRel1, Set, AnySet) -> BinRel2
538 Types:
540 AnySet = anyset()
542 BinRel1 = BinRel2 = binary_relation()
543 Set = a_set()
544 Returns the extension of BinRel1 such that for each element E in
546 Set that does not belong to the domain of BinRel1, BinRel2 con‐
547 tains the pair (E, AnySet).
548 1> S = sofs:set([b,c]),
550 A = sofs:empty_set(),
551 R = sofs:family([{a,[1,2]},{b,[3]}]),
552 X = sofs:extension(R, S, A),
553 sofs:to_external(X).
554 [{a,[1,2]},{b,[3]},{c,[]}]
555 family(Tuples) -> Family
557 family(Tuples, Type) -> Family
559 Types:
561 Family = family()
563 Tuples = [tuple()]
564 Type = type()
565 Creates a family of subsets. family(F, T) is equivalent to
567 from_term(F, T) if the result is a family. If no type is explic‐
568 itly specified, [{atom, [atom]}] is used as the family type.
569 family_difference(Family1, Family2) -> Family3
571 Types:
573 Family1 = Family2 = Family3 = family()
575 If Family1 and Family2 are families, then Family3 is the family
577 such that the index set is equal to the index set of Family1,
578 and Family3[i] is the difference between Family1[i] and Fam‐
579 ily2[i] if Family2 maps i, otherwise Family1[i].
580 1> F1 = sofs:family([{a,[1,2]},{b,[3,4]}]),
582 F2 = sofs:family([{b,[4,5]},{c,[6,7]}]),
583 F3 = sofs:family_difference(F1, F2),
584 sofs:to_external(F3).
585 [{a,[1,2]},{b,[3]}]
586 family_domain(Family1) -> Family2
588 Types:
590 Family1 = Family2 = family()
592 If Family1 is a family and Family1[i] is a binary relation for
594 every i in the index set of Family1, then Family2 is the family
595 with the same index set as Family1 such that Family2[i] is the
596 domain of Family1[i].
597 1> FR = sofs:from_term([{a,[{1,a},{2,b},{3,c}]},{b,[]},{c,[{4,d},{5,e}]}]),
599 F = sofs:family_domain(FR),
600 sofs:to_external(F).
601 [{a,[1,2,3]},{b,[]},{c,[4,5]}]
602 family_field(Family1) -> Family2
604 Types:
606 Family1 = Family2 = family()
608 If Family1 is a family and Family1[i] is a binary relation for
610 every i in the index set of Family1, then Family2 is the family
611 with the same index set as Family1 such that Family2[i] is the
612 field of Family1[i].
613 1> FR = sofs:from_term([{a,[{1,a},{2,b},{3,c}]},{b,[]},{c,[{4,d},{5,e}]}]),
615 F = sofs:family_field(FR),
616 sofs:to_external(F).
617 [{a,[1,2,3,a,b,c]},{b,[]},{c,[4,5,d,e]}]
618 family_field(Family1) is equivalent to family_union(fam‐
620 ily_domain(Family1), family_range(Family1)).
621 family_intersection(Family1) -> Family2
623 Types:
625 Family1 = Family2 = family()
627 If Family1 is a family and Family1[i] is a set of sets for every
629 i in the index set of Family1, then Family2 is the family with
630 the same index set as Family1 such that Family2[i] is the inter‐
631 section of Family1[i].
632 If Family1[i] is an empty set for some i, the process exits with
634 a badarg message.
635 1> F1 = sofs:from_term([{a,[[1,2,3],[2,3,4]]},{b,[[x,y,z],[x,y]]}]),
637 F2 = sofs:family_intersection(F1),
638 sofs:to_external(F2).
639 [{a,[2,3]},{b,[x,y]}]
640 family_intersection(Family1, Family2) -> Family3
642 Types:
644 Family1 = Family2 = Family3 = family()
646 If Family1 and Family2 are families, then Family3 is the family
648 such that the index set is the intersection of Family1:s and
649 Family2:s index sets, and Family3[i] is the intersection of Fam‐
650 ily1[i] and Family2[i].
651 1> F1 = sofs:family([{a,[1,2]},{b,[3,4]},{c,[5,6]}]),
653 F2 = sofs:family([{b,[4,5]},{c,[7,8]},{d,[9,10]}]),
654 F3 = sofs:family_intersection(F1, F2),
655 sofs:to_external(F3).
656 [{b,[4]},{c,[]}]
657 family_projection(SetFun, Family1) -> Family2
659 Types:
661 SetFun = set_fun()
663 Family1 = Family2 = family()
664 If Family1 is a family, then Family2 is the family with the same
666 index set as Family1 such that Family2[i] is the result of call‐
667 ing SetFun with Family1[i] as argument.
668 1> F1 = sofs:from_term([{a,[[1,2],[2,3]]},{b,[[]]}]),
670 F2 = sofs:family_projection(fun sofs:union/1, F1),
671 sofs:to_external(F2).
672 [{a,[1,2,3]},{b,[]}]
673 family_range(Family1) -> Family2
675 Types:
677 Family1 = Family2 = family()
679 If Family1 is a family and Family1[i] is a binary relation for
681 every i in the index set of Family1, then Family2 is the family
682 with the same index set as Family1 such that Family2[i] is the
683 range of Family1[i].
684 1> FR = sofs:from_term([{a,[{1,a},{2,b},{3,c}]},{b,[]},{c,[{4,d},{5,e}]}]),
686 F = sofs:family_range(FR),
687 sofs:to_external(F).
688 [{a,[a,b,c]},{b,[]},{c,[d,e]}]
689 family_specification(Fun, Family1) -> Family2
691 Types:
693 Fun = spec_fun()
695 Family1 = Family2 = family()
696 If Family1 is a family, then Family2 is the restriction of Fam‐
698 ily1 to those elements i of the index set for which Fun applied
699 to Family1[i] returns true. If Fun is a tuple {external, Fun2},
700 then Fun2 is applied to the external set of Family1[i], other‐
701 wise Fun is applied to Family1[i].
702 1> F1 = sofs:family([{a,[1,2,3]},{b,[1,2]},{c,[1]}]),
704 SpecFun = fun(S) -> sofs:no_elements(S) =:= 2 end,
705 F2 = sofs:family_specification(SpecFun, F1),
706 sofs:to_external(F2).
707 [{b,[1,2]}]
708 family_to_digraph(Family) -> Graph
710 family_to_digraph(Family, GraphType) -> Graph
712 Types:
714 Graph = digraph:graph()
716 Family = family()
717 GraphType = [digraph:d_type()]
718 Creates a directed graph from family Family. For each pair (a,
720 {b[1], ..., b[n]}) of Family, vertex a and the edges (a, b[i])
721 for 1 <= i <= n are added to a newly created directed graph.
722 If no graph type is specified, digraph:new/0 is used for creat‐
724 ing the directed graph, otherwise argument GraphType is passed
725 on as second argument to digraph:new/1.
726 It F is a family, it holds that F is a subset of digraph_to_fam‐
728 ily(family_to_digraph(F), type(F)). Equality holds if
729 union_of_family(F) is a subset of domain(F).
730 Creating a cycle in an acyclic graph exits the process with a
732 cyclic message.
733 family_to_relation(Family) -> BinRel
735 Types:
737 Family = family()
739 BinRel = binary_relation()
740 If Family is a family, then BinRel is the binary relation con‐
742 taining all pairs (i, x) such that i belongs to the index set of
743 Family and x belongs to Family[i].
744 1> F = sofs:family([{a,[]}, {b,[1]}, {c,[2,3]}]),
746 R = sofs:family_to_relation(F),
747 sofs:to_external(R).
748 [{b,1},{c,2},{c,3}]
749 family_union(Family1) -> Family2
751 Types:
753 Family1 = Family2 = family()
755 If Family1 is a family and Family1[i] is a set of sets for each
757 i in the index set of Family1, then Family2 is the family with
758 the same index set as Family1 such that Family2[i] is the union
759 of Family1[i].
760 1> F1 = sofs:from_term([{a,[[1,2],[2,3]]},{b,[[]]}]),
762 F2 = sofs:family_union(F1),
763 sofs:to_external(F2).
764 [{a,[1,2,3]},{b,[]}]
765 family_union(F) is equivalent to family_projection(fun
767 sofs:union/1, F).
768 family_union(Family1, Family2) -> Family3
770 Types:
772 Family1 = Family2 = Family3 = family()
774 If Family1 and Family2 are families, then Family3 is the family
776 such that the index set is the union of Family1:s and Family2:s
777 index sets, and Family3[i] is the union of Family1[i] and Fam‐
778 ily2[i] if both map i, otherwise Family1[i] or Family2[i].
779 1> F1 = sofs:family([{a,[1,2]},{b,[3,4]},{c,[5,6]}]),
781 F2 = sofs:family([{b,[4,5]},{c,[7,8]},{d,[9,10]}]),
782 F3 = sofs:family_union(F1, F2),
783 sofs:to_external(F3).
784 [{a,[1,2]},{b,[3,4,5]},{c,[5,6,7,8]},{d,[9,10]}]
785 field(BinRel) -> Set
787 Types:
789 BinRel = binary_relation()
791 Set = a_set()
792 Returns the field of the binary relation BinRel.
794 1> R = sofs:relation([{1,a},{1,b},{2,b},{2,c}]),
796 S = sofs:field(R),
797 sofs:to_external(S).
798 [1,2,a,b,c]
799 field(R) is equivalent to union(domain(R), range(R)).
801 from_external(ExternalSet, Type) -> AnySet
803 Types:
805 ExternalSet = external_set()
807 AnySet = anyset()
808 Type = type()
809 Creates a set from the external set ExternalSet and the type
811 Type. It is assumed that Type is a valid type of ExternalSet.
812 from_sets(ListOfSets) -> Set
814 Types:
816 Set = a_set()
818 ListOfSets = [anyset()]
819 Returns the unordered set containing the sets of list ListOf‐
821 Sets.
822 1> S1 = sofs:relation([{a,1},{b,2}]),
824 S2 = sofs:relation([{x,3},{y,4}]),
825 S = sofs:from_sets([S1,S2]),
826 sofs:to_external(S).
827 [[{a,1},{b,2}],[{x,3},{y,4}]]
828 from_sets(TupleOfSets) -> Ordset
830 Types:
832 Ordset = ordset()
834 TupleOfSets = tuple_of(anyset())
835 Returns the ordered set containing the sets of the non-empty
837 tuple TupleOfSets.
838 from_term(Term) -> AnySet
840 from_term(Term, Type) -> AnySet
842 Types:
844 AnySet = anyset()
846 Term = term()
847 Type = type()
848 Creates an element of Sets by traversing term Term, sorting
850 lists, removing duplicates, and deriving or verifying a valid
851 type for the so obtained external set. An explicitly specified
852 type Type can be used to limit the depth of the traversal; an
853 atomic type stops the traversal, as shown by the following exam‐
854 ple where "foo" and {"foo"} are left unmodified:
855 1> S = sofs:from_term([{{"foo"},[1,1]},{"foo",[2,2]}], [{atom,[atom]}]),
857 sofs:to_external(S).
858 [{{"foo"},[1]},{"foo",[2]}]
859 from_term can be used for creating atomic or ordered sets. The
861 only purpose of such a set is that of later building unordered
862 sets, as all functions in this module that do anything operate
863 on unordered sets. Creating unordered sets from a collection of
864 ordered sets can be the way to go if the ordered sets are big
865 and one does not want to waste heap by rebuilding the elements
866 of the unordered set. The following example shows that a set can
867 be built "layer by layer":
868 1> A = sofs:from_term(a),
870 S = sofs:set([1,2,3]),
871 P1 = sofs:from_sets({A,S}),
872 P2 = sofs:from_term({b,[6,5,4]}),
873 Ss = sofs:from_sets([P1,P2]),
874 sofs:to_external(Ss).
875 [{a,[1,2,3]},{b,[4,5,6]}]
876 Other functions that create sets are from_external/2 and
878 from_sets/1. Special cases of from_term/2 are a_function/1,2,
879 empty_set/0, family/1,2, relation/1,2, and set/1,2.
880 image(BinRel, Set1) -> Set2
882 Types:
884 BinRel = binary_relation()
886 Set1 = Set2 = a_set()
887 Returns the image of set Set1 under the binary relation BinRel.
889 1> R = sofs:relation([{1,a},{2,b},{2,c},{3,d}]),
891 S1 = sofs:set([1,2]),
892 S2 = sofs:image(R, S1),
893 sofs:to_external(S2).
894 [a,b,c]
895 intersection(SetOfSets) -> Set
897 Types:
899 Set = a_set()
901 SetOfSets = set_of_sets()
902 Returns the intersection of the set of sets SetOfSets.
904 Intersecting an empty set of sets exits the process with a
906 badarg message.
907 intersection(Set1, Set2) -> Set3
909 Types:
911 Set1 = Set2 = Set3 = a_set()
913 Returns the intersection of Set1 and Set2.
915 intersection_of_family(Family) -> Set
917 Types:
919 Family = family()
921 Set = a_set()
922 Returns the intersection of family Family.
924 Intersecting an empty family exits the process with a badarg
926 message.
927 1> F = sofs:family([{a,[0,2,4]},{b,[0,1,2]},{c,[2,3]}]),
929 S = sofs:intersection_of_family(F),
930 sofs:to_external(S).
931 [2]
932 inverse(Function1) -> Function2
934 Types:
936 Function1 = Function2 = a_function()
938 Returns the inverse of function Function1.
940 1> R1 = sofs:relation([{1,a},{2,b},{3,c}]),
942 R2 = sofs:inverse(R1),
943 sofs:to_external(R2).
944 [{a,1},{b,2},{c,3}]
945 inverse_image(BinRel, Set1) -> Set2
947 Types:
949 BinRel = binary_relation()
951 Set1 = Set2 = a_set()
952 Returns the inverse image of Set1 under the binary relation Bin‐
954 Rel.
955 1> R = sofs:relation([{1,a},{2,b},{2,c},{3,d}]),
957 S1 = sofs:set([c,d,e]),
958 S2 = sofs:inverse_image(R, S1),
959 sofs:to_external(S2).
960 [2,3]
961 is_a_function(BinRel) -> Bool
963 Types:
965 Bool = boolean()
967 BinRel = binary_relation()
968 Returns true if the binary relation BinRel is a function or the
970 untyped empty set, otherwise false.
971 is_disjoint(Set1, Set2) -> Bool
973 Types:
975 Bool = boolean()
977 Set1 = Set2 = a_set()
978 Returns true if Set1 and Set2 are disjoint, otherwise false.
980 is_empty_set(AnySet) -> Bool
982 Types:
984 AnySet = anyset()
986 Bool = boolean()
987 Returns true if AnySet is an empty unordered set, otherwise
989 false.
990 is_equal(AnySet1, AnySet2) -> Bool
992 Types:
994 AnySet1 = AnySet2 = anyset()
996 Bool = boolean()
997 Returns true if AnySet1 and AnySet2 are equal, otherwise false.
999 The following example shows that ==/2 is used when comparing
1000 sets for equality:
1001 1> S1 = sofs:set([1.0]),
1003 S2 = sofs:set([1]),
1004 sofs:is_equal(S1, S2).
1005 true
1006 is_set(AnySet) -> Bool
1008 Types:
1010 AnySet = anyset()
1012 Bool = boolean()
1013 Returns true if AnySet is an unordered set, and false if AnySet
1015 is an ordered set or an atomic set.
1016 is_sofs_set(Term) -> Bool
1018 Types:
1020 Bool = boolean()
1022 Term = term()
1023 Returns true if Term is an unordered set, an ordered set, or an
1025 atomic set, otherwise false.
1026 is_subset(Set1, Set2) -> Bool
1028 Types:
1030 Bool = boolean()
1032 Set1 = Set2 = a_set()
1033 Returns true if Set1 is a subset of Set2, otherwise false.
1035 is_type(Term) -> Bool
1037 Types:
1039 Bool = boolean()
1041 Term = term()
1042 Returns true if term Term is a type.
1044 join(Relation1, I, Relation2, J) -> Relation3
1046 Types:
1048 Relation1 = Relation2 = Relation3 = relation()
1050 I = J = integer() >= 1
1051 Returns the natural join of the relations Relation1 and Rela‐
1053 tion2 on coordinates I and J.
1054 1> R1 = sofs:relation([{a,x,1},{b,y,2}]),
1056 R2 = sofs:relation([{1,f,g},{1,h,i},{2,3,4}]),
1057 J = sofs:join(R1, 3, R2, 1),
1058 sofs:to_external(J).
1059 [{a,x,1,f,g},{a,x,1,h,i},{b,y,2,3,4}]
1060 multiple_relative_product(TupleOfBinRels, BinRel1) -> BinRel2
1062 Types:
1064 TupleOfBinRels = tuple_of(BinRel)
1066 BinRel = BinRel1 = BinRel2 = binary_relation()
1067 If TupleOfBinRels is a non-empty tuple {R[1], ..., R[n]} of
1069 binary relations and BinRel1 is a binary relation, then BinRel2
1070 is the multiple relative product of the ordered set (R[i], ...,
1071 R[n]) and BinRel1.
1072 1> Ri = sofs:relation([{a,1},{b,2},{c,3}]),
1074 R = sofs:relation([{a,b},{b,c},{c,a}]),
1075 MP = sofs:multiple_relative_product({Ri, Ri}, R),
1076 sofs:to_external(sofs:range(MP)).
1077 [{1,2},{2,3},{3,1}]
1078 no_elements(ASet) -> NoElements
1080 Types:
1082 ASet = a_set() | ordset()
1084 NoElements = integer() >= 0
1085 Returns the number of elements of the ordered or unordered set
1087 ASet.
1088 partition(SetOfSets) -> Partition
1090 Types:
1092 SetOfSets = set_of_sets()
1094 Partition = a_set()
1095 Returns the partition of the union of the set of sets SetOfSets
1097 such that two elements are considered equal if they belong to
1098 the same elements of SetOfSets.
1099 1> Sets1 = sofs:from_term([[a,b,c],[d,e,f],[g,h,i]]),
1101 Sets2 = sofs:from_term([[b,c,d],[e,f,g],[h,i,j]]),
1102 P = sofs:partition(sofs:union(Sets1, Sets2)),
1103 sofs:to_external(P).
1104 [[a],[b,c],[d],[e,f],[g],[h,i],[j]]
1105 partition(SetFun, Set) -> Partition
1107 Types:
1109 SetFun = set_fun()
1111 Partition = Set = a_set()
1112 Returns the partition of Set such that two elements are consid‐
1114 ered equal if the results of applying SetFun are equal.
1115 1> Ss = sofs:from_term([[a],[b],[c,d],[e,f]]),
1117 SetFun = fun(S) -> sofs:from_term(sofs:no_elements(S)) end,
1118 P = sofs:partition(SetFun, Ss),
1119 sofs:to_external(P).
1120 [[[a],[b]],[[c,d],[e,f]]]
1121 partition(SetFun, Set1, Set2) -> {Set3, Set4}
1123 Types:
1125 SetFun = set_fun()
1127 Set1 = Set2 = Set3 = Set4 = a_set()
1128 Returns a pair of sets that, regarded as constituting a set,
1130 forms a partition of Set1. If the result of applying SetFun to
1131 an element of Set1 gives an element in Set2, the element belongs
1132 to Set3, otherwise the element belongs to Set4.
1133 1> R1 = sofs:relation([{1,a},{2,b},{3,c}]),
1135 S = sofs:set([2,4,6]),
1136 {R2,R3} = sofs:partition(1, R1, S),
1137 {sofs:to_external(R2),sofs:to_external(R3)}.
1138 {[{2,b}],[{1,a},{3,c}]}
1139 partition(F, S1, S2) is equivalent to {restriction(F, S1, S2),
1141 drestriction(F, S1, S2)}.
1142 partition_family(SetFun, Set) -> Family
1144 Types:
1146 Family = family()
1148 SetFun = set_fun()
1149 Set = a_set()
1150 Returns family Family where the indexed set is a partition of
1152 Set such that two elements are considered equal if the results
1153 of applying SetFun are the same value i. This i is the index
1154 that Family maps onto the equivalence class.
1155 1> S = sofs:relation([{a,a,a,a},{a,a,b,b},{a,b,b,b}]),
1157 SetFun = {external, fun({A,_,C,_}) -> {A,C} end},
1158 F = sofs:partition_family(SetFun, S),
1159 sofs:to_external(F).
1160 [{{a,a},[{a,a,a,a}]},{{a,b},[{a,a,b,b},{a,b,b,b}]}]
1161 product(TupleOfSets) -> Relation
1163 Types:
1165 Relation = relation()
1167 TupleOfSets = tuple_of(a_set())
1168 Returns the Cartesian product of the non-empty tuple of sets
1170 TupleOfSets. If (x[1], ..., x[n]) is an element of the n-ary
1171 relation Relation, then x[i] is drawn from element i of TupleOf‐
1172 Sets.
1173 1> S1 = sofs:set([a,b]),
1175 S2 = sofs:set([1,2]),
1176 S3 = sofs:set([x,y]),
1177 P3 = sofs:product({S1,S2,S3}),
1178 sofs:to_external(P3).
1179 [{a,1,x},{a,1,y},{a,2,x},{a,2,y},{b,1,x},{b,1,y},{b,2,x},{b,2,y}]
1180 product(Set1, Set2) -> BinRel
1182 Types:
1184 BinRel = binary_relation()
1186 Set1 = Set2 = a_set()
1187 Returns the Cartesian product of Set1 and Set2.
1189 1> S1 = sofs:set([1,2]),
1191 S2 = sofs:set([a,b]),
1192 R = sofs:product(S1, S2),
1193 sofs:to_external(R).
1194 [{1,a},{1,b},{2,a},{2,b}]
1195 product(S1, S2) is equivalent to product({S1, S2}).
1197 projection(SetFun, Set1) -> Set2
1199 Types:
1201 SetFun = set_fun()
1203 Set1 = Set2 = a_set()
1204 Returns the set created by substituting each element of Set1 by
1206 the result of applying SetFun to the element.
1207 If SetFun is a number i >= 1 and Set1 is a relation, then the
1209 returned set is the projection of Set1 onto coordinate i.
1210 1> S1 = sofs:from_term([{1,a},{2,b},{3,a}]),
1212 S2 = sofs:projection(2, S1),
1213 sofs:to_external(S2).
1214 [a,b]
1215 range(BinRel) -> Set
1217 Types:
1219 BinRel = binary_relation()
1221 Set = a_set()
1222 Returns the range of the binary relation BinRel.
1224 1> R = sofs:relation([{1,a},{1,b},{2,b},{2,c}]),
1226 S = sofs:range(R),
1227 sofs:to_external(S).
1228 [a,b,c]
1229 relation(Tuples) -> Relation
1231 relation(Tuples, Type) -> Relation
1233 Types:
1235 N = integer()
1237 Type = N | type()
1238 Relation = relation()
1239 Tuples = [tuple()]
1240 Creates a relation. relation(R, T) is equivalent to from_term(R,
1242 T), if T is a type and the result is a relation. If Type is an
1243 integer N, then [{atom, ..., atom}]), where the tuple size is N,
1244 is used as type of the relation. If no type is explicitly speci‐
1245 fied, the size of the first tuple of Tuples is used if there is
1246 such a tuple. relation([]) is equivalent to relation([], 2).
1247 relation_to_family(BinRel) -> Family
1249 Types:
1251 Family = family()
1253 BinRel = binary_relation()
1254 Returns family Family such that the index set is equal to the
1256 domain of the binary relation BinRel, and Family[i] is the image
1257 of the set of i under BinRel.
1258 1> R = sofs:relation([{b,1},{c,2},{c,3}]),
1260 F = sofs:relation_to_family(R),
1261 sofs:to_external(F).
1262 [{b,[1]},{c,[2,3]}]
1263 relative_product(ListOfBinRels) -> BinRel2
1265 relative_product(ListOfBinRels, BinRel1) -> BinRel2
1267 Types:
1269 ListOfBinRels = [BinRel, ...]
1271 BinRel = BinRel1 = BinRel2 = binary_relation()
1272 If ListOfBinRels is a non-empty list [R[1], ..., R[n]] of binary
1274 relations and BinRel1 is a binary relation, then BinRel2 is the
1275 relative product of the ordered set (R[i], ..., R[n]) and Bin‐
1276 Rel1.
1277 If BinRel1 is omitted, the relation of equality between the ele‐
1279 ments of the Cartesian product of the ranges of R[i], range R[1]
1280 x ... x range R[n], is used instead (intuitively, nothing is
1281 "lost").
1282 1> TR = sofs:relation([{1,a},{1,aa},{2,b}]),
1284 R1 = sofs:relation([{1,u},{2,v},{3,c}]),
1285 R2 = sofs:relative_product([TR, R1]),
1286 sofs:to_external(R2).
1287 [{1,{a,u}},{1,{aa,u}},{2,{b,v}}]
1288 Notice that relative_product([R1], R2) is different from rela‐
1290 tive_product(R1, R2); the list of one element is not identified
1291 with the element itself.
1292 relative_product(BinRel1, BinRel2) -> BinRel3
1294 Types:
1296 BinRel1 = BinRel2 = BinRel3 = binary_relation()
1298 Returns the relative product of the binary relations BinRel1 and
1300 BinRel2.
1301 relative_product1(BinRel1, BinRel2) -> BinRel3
1303 Types:
1305 BinRel1 = BinRel2 = BinRel3 = binary_relation()
1307 Returns the relative product of the converse of the binary rela‐
1309 tion BinRel1 and the binary relation BinRel2.
1310 1> R1 = sofs:relation([{1,a},{1,aa},{2,b}]),
1312 R2 = sofs:relation([{1,u},{2,v},{3,c}]),
1313 R3 = sofs:relative_product1(R1, R2),
1314 sofs:to_external(R3).
1315 [{a,u},{aa,u},{b,v}]
1316 relative_product1(R1, R2) is equivalent to relative_product(con‐
1318 verse(R1), R2).
1319 restriction(BinRel1, Set) -> BinRel2
1321 Types:
1323 BinRel1 = BinRel2 = binary_relation()
1325 Set = a_set()
1326 Returns the restriction of the binary relation BinRel1 to Set.
1328 1> R1 = sofs:relation([{1,a},{2,b},{3,c}]),
1330 S = sofs:set([1,2,4]),
1331 R2 = sofs:restriction(R1, S),
1332 sofs:to_external(R2).
1333 [{1,a},{2,b}]
1334 restriction(SetFun, Set1, Set2) -> Set3
1336 Types:
1338 SetFun = set_fun()
1340 Set1 = Set2 = Set3 = a_set()
1341 Returns a subset of Set1 containing those elements that gives an
1343 element in Set2 as the result of applying SetFun.
1344 1> S1 = sofs:relation([{1,a},{2,b},{3,c}]),
1346 S2 = sofs:set([b,c,d]),
1347 S3 = sofs:restriction(2, S1, S2),
1348 sofs:to_external(S3).
1349 [{2,b},{3,c}]
1350 set(Terms) -> Set
1352 set(Terms, Type) -> Set
1354 Types:
1356 Set = a_set()
1358 Terms = [term()]
1359 Type = type()
1360 Creates an unordered set. set(L, T) is equivalent to
1362 from_term(L, T), if the result is an unordered set. If no type
1363 is explicitly specified, [atom] is used as the set type.
1364 specification(Fun, Set1) -> Set2
1366 Types:
1368 Fun = spec_fun()
1370 Set1 = Set2 = a_set()
1371 Returns the set containing every element of Set1 for which Fun
1373 returns true. If Fun is a tuple {external, Fun2}, Fun2 is
1374 applied to the external set of each element, otherwise Fun is
1375 applied to each element.
1376 1> R1 = sofs:relation([{a,1},{b,2}]),
1378 R2 = sofs:relation([{x,1},{x,2},{y,3}]),
1379 S1 = sofs:from_sets([R1,R2]),
1380 S2 = sofs:specification(fun sofs:is_a_function/1, S1),
1381 sofs:to_external(S2).
1382 [[{a,1},{b,2}]]
1383 strict_relation(BinRel1) -> BinRel2
1385 Types:
1387 BinRel1 = BinRel2 = binary_relation()
1389 Returns the strict relation corresponding to the binary relation
1391 BinRel1.
1392 1> R1 = sofs:relation([{1,1},{1,2},{2,1},{2,2}]),
1394 R2 = sofs:strict_relation(R1),
1395 sofs:to_external(R2).
1396 [{1,2},{2,1}]
1397 substitution(SetFun, Set1) -> Set2
1399 Types:
1401 SetFun = set_fun()
1403 Set1 = Set2 = a_set()
1404 Returns a function, the domain of which is Set1. The value of an
1406 element of the domain is the result of applying SetFun to the
1407 element.
1408 1> L = [{a,1},{b,2}].
1410 [{a,1},{b,2}]
1411 2> sofs:to_external(sofs:projection(1,sofs:relation(L))).
1412 [a,b]
1413 3> sofs:to_external(sofs:substitution(1,sofs:relation(L))).
1414 [{{a,1},a},{{b,2},b}]
1415 4> SetFun = {external, fun({A,_}=E) -> {E,A} end},
1416 sofs:to_external(sofs:projection(SetFun,sofs:relation(L))).
1417 [{{a,1},a},{{b,2},b}]
1418 The relation of equality between the elements of {a,b,c}:
1420 1> I = sofs:substitution(fun(A) -> A end, sofs:set([a,b,c])),
1422 sofs:to_external(I).
1423 [{a,a},{b,b},{c,c}]
1424 Let SetOfSets be a set of sets and BinRel a binary relation. The
1426 function that maps each element Set of SetOfSets onto the image
1427 of Set under BinRel is returned by the following function:
1428 images(SetOfSets, BinRel) ->
1430 Fun = fun(Set) -> sofs:image(BinRel, Set) end,
1431 sofs:substitution(Fun, SetOfSets).
1432 External unordered sets are represented as sorted lists. So,
1434 creating the image of a set under a relation R can traverse all
1435 elements of R (to that comes the sorting of results, the image).
1436 In image/2, BinRel is traversed once for each element of SetOf‐
1437 Sets, which can take too long. The following efficient function
1438 can be used instead under the assumption that the image of each
1439 element of SetOfSets under BinRel is non-empty:
1440 images2(SetOfSets, BinRel) ->
1442 CR = sofs:canonical_relation(SetOfSets),
1443 R = sofs:relative_product1(CR, BinRel),
1444 sofs:relation_to_family(R).
1445 symdiff(Set1, Set2) -> Set3
1447 Types:
1449 Set1 = Set2 = Set3 = a_set()
1451 Returns the symmetric difference (or the Boolean sum) of Set1
1453 and Set2.
1454 1> S1 = sofs:set([1,2,3]),
1456 S2 = sofs:set([2,3,4]),
1457 P = sofs:symdiff(S1, S2),
1458 sofs:to_external(P).
1459 [1,4]
1460 symmetric_partition(Set1, Set2) -> {Set3, Set4, Set5}
1462 Types:
1464 Set1 = Set2 = Set3 = Set4 = Set5 = a_set()
1466 Returns a triple of sets:
1468 * Set3 contains the elements of Set1 that do not belong to
1470 Set2.
1471 * Set4 contains the elements of Set1 that belong to Set2.
1473 * Set5 contains the elements of Set2 that do not belong to
1475 Set1.
1476 to_external(AnySet) -> ExternalSet
1478 Types:
1480 ExternalSet = external_set()
1482 AnySet = anyset()
1483 Returns the external set of an atomic, ordered, or unordered
1485 set.
1486 to_sets(ASet) -> Sets
1488 Types:
1490 ASet = a_set() | ordset()
1492 Sets = tuple_of(AnySet) | [AnySet]
1493 AnySet = anyset()
1494 Returns the elements of the ordered set ASet as a tuple of sets,
1496 and the elements of the unordered set ASet as a sorted list of
1497 sets without duplicates.
1498 type(AnySet) -> Type
1500 Types:
1502 AnySet = anyset()
1504 Type = type()
1505 Returns the type of an atomic, ordered, or unordered set.
1507 union(SetOfSets) -> Set
1509 Types:
1511 Set = a_set()
1513 SetOfSets = set_of_sets()
1514 Returns the union of the set of sets SetOfSets.
1516 union(Set1, Set2) -> Set3
1518 Types:
1520 Set1 = Set2 = Set3 = a_set()
1522 Returns the union of Set1 and Set2.
1524 union_of_family(Family) -> Set
1526 Types:
1528 Family = family()
1530 Set = a_set()
1531 Returns the union of family Family.
1533 1> F = sofs:family([{a,[0,2,4]},{b,[0,1,2]},{c,[2,3]}]),
1535 S = sofs:union_of_family(F),
1536 sofs:to_external(S).
1537 [0,1,2,3,4]
1538 weak_relation(BinRel1) -> BinRel2
1540 Types:
1542 BinRel1 = BinRel2 = binary_relation()
1544 Returns a subset S of the weak relation W corresponding to the
1546 binary relation BinRel1. Let F be the field of BinRel1. The sub‐
1547 set S is defined so that x S y if x W y for some x in F and for
1548 some y in F.
1549 1> R1 = sofs:relation([{1,1},{1,2},{3,1}]),
1551 R2 = sofs:weak_relation(R1),
1552 sofs:to_external(R2).
1553 [{1,1},{1,2},{2,2},{3,1},{3,3}]
1554
1556 dict(3), digraph(3), orddict(3), ordsets(3), sets(3)
1557Ericsson AB stdlib 3.10 sofs(3)