1sofs(3) Erlang Module Definition sofs(3)
2
3
4
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
13 The data representing sofs as used by this module is to be regarded as
14 opaque by other modules. In abstract terms, the representation is a
15 composite type of existing Erlang terms. See note on data types. Any
16 code assuming knowledge of the format is running on thin ice.
17
18 Given a set A and a sentence S(x), where x is a free variable, a new
19 set B whose elements are exactly those elements of A for which S(x)
20 holds can be formed, this is denoted B = {x in A : S(x)}. Sentences are
21 expressed using the logical operators "for some" (or "there exists"),
22 "for all", "and", "or", "not". If the existence of a set containing all
23 the specified elements is known (as is always the case in this module),
24 this is denoted B = {x : S(x)}.
25
26 * The unordered set containing the elements a, b, and c is denoted
27 {a, b, c}. This notation is not to be confused with tuples.
28
29 The ordered pair of a and b, with first coordinate a and second co‐
30 ordinate b, is denoted (a, b). An ordered pair is an ordered set of
31 two elements. In this module, ordered sets can contain one, two, or
32 more elements, and parentheses are used to enclose the elements.
33
34 Unordered sets and ordered sets are orthogonal, again in this mod‐
35 ule; there is no unordered set equal to any ordered set.
36
37 * The empty set contains no elements.
38
39 Set A is equal to set B if they contain the same elements, which is
40 denoted A = B. Two ordered sets are equal if they contain the same
41 number of elements and have equal elements at each coordinate.
42
43 Set B is a subset of set A if A contains all elements that B con‐
44 tains.
45
46 The union of two sets A and B is the smallest set that contains all
47 elements of A and all elements of B.
48
49 The intersection of two sets A and B is the set that contains all
50 elements of A that belong to B.
51
52 Two sets are disjoint if their intersection is the empty set.
53
54 The difference of two sets A and B is the set that contains all el‐
55 ements of A that do not belong to B.
56
57 The symmetric difference of two sets is the set that contains those
58 element that belong to either of the two sets, but not both.
59
60 The union of a collection of sets is the smallest set that contains
61 all the elements that belong to at least one set of the collection.
62
63 The intersection of a non-empty collection of sets is the set that
64 contains all elements that belong to every set of the collection.
65
66 * The Cartesian product of two sets X and Y, denoted X x Y, is the
67 set {a : a = (x, y) for some x in X and for some y in Y}.
68
69 A relation is a subset of X x Y. Let R be a relation. The fact that
70 (x, y) belongs to R is written as x R y. As relations are sets, the
71 definitions of the last item (subset, union, and so on) apply to
72 relations as well.
73
74 The domain of R is the set {x : x R y for some y in Y}.
75
76 The range of R is the set {y : x R y for some x in X}.
77
78 The converse of R is the set {a : a = (y, x) for some (x, y) in R}.
79
80 If A is a subset of X, the image of A under R is the set {y : x R y
81 for some x in A}. If B is a subset of Y, the inverse image of B is
82 the set {x : x R y for some y in B}.
83
84 If R is a relation from X to Y, and S is a relation from Y to Z,
85 the relative product of R and S is the relation T from X to Z de‐
86 fined so that x T z if and only if there exists an element y in Y
87 such that x R y and y S z.
88
89 The restriction of R to A is the set S defined so that x S y if and
90 only if there exists an element x in A such that x R y.
91
92 If S is a restriction of R to A, then R is an extension of S to X.
93
94 If X = Y, then R is called a relation in X.
95
96 The field of a relation R in X is the union of the domain of R and
97 the range of R.
98
99 If R is a relation in X, and if S is defined so that x S y if x R y
100 and not x = y, then S is the strict relation corresponding to R.
101 Conversely, if S is a relation in X, and if R is defined so that x
102 R y if x S y or x = y, then R is the weak relation corresponding to
103 S.
104
105 A relation R in X is reflexive if x R x for every element x of X,
106 it is symmetric if x R y implies that y R x, and it is transitive
107 if x R y and y R z imply that x R z.
108
109 * A function F is a relation, a subset of X x Y, such that the domain
110 of F is equal to X and such that for every x in X there is a unique
111 element y in Y with (x, y) in F. The latter condition can be formu‐
112 lated as follows: if x F y and x F z, then y = z. In this module,
113 it is not required that the domain of F is equal to X for a rela‐
114 tion to be considered a function.
115
116 Instead of writing (x, y) in F or x F y, we write F(x) = y when F
117 is a function, and say that F maps x onto y, or that the value of F
118 at x is y.
119
120 As functions are relations, the definitions of the last item (do‐
121 main, range, and so on) apply to functions as well.
122
123 If the converse of a function F is a function F', then F' is called
124 the inverse of F.
125
126 The relative product of two functions F1 and F2 is called the com‐
127 posite of F1 and F2 if the range of F1 is a subset of the domain of
128 F2.
129
130 * Sometimes, when the range of a function is more important than the
131 function itself, the function is called a family.
132
133 The domain of a family is called the index set, and the range is
134 called the indexed set.
135
136 If x is a family from I to X, then x[i] denotes the value of the
137 function at index i. The notation "a family in X" is used for such
138 a family.
139
140 When the indexed set is a set of subsets of a set X, we call x a
141 family of subsets of X.
142
143 If x is a family of subsets of X, the union of the range of x is
144 called the union of the family x.
145
146 If x is non-empty (the index set is non-empty), the intersection of
147 the family x is the intersection of the range of x.
148
149 In this module, the only families that are considered are families
150 of subsets of some set X; in the following, the word "family" is
151 used for such families of subsets.
152
153 * A partition of a set X is a collection S of non-empty subsets of X
154 whose union is X and whose elements are pairwise disjoint.
155
156 A relation in a set is an equivalence relation if it is reflexive,
157 symmetric, and transitive.
158
159 If R is an equivalence relation in X, and x is an element of X, the
160 equivalence class of x with respect to R is the set of all those
161 elements y of X for which x R y holds. The equivalence classes con‐
162 stitute a partitioning of X. Conversely, if C is a partition of X,
163 the relation that holds for any two elements of X if they belong to
164 the same equivalence class, is an equivalence relation induced by
165 the partition C.
166
167 If R is an equivalence relation in X, the canonical map is the
168 function that maps every element of X onto its equivalence class.
169
170 * Relations as defined above (as sets of ordered pairs) are from now
171 on referred to as binary relations.
172
173 We call a set of ordered sets (x[1], ..., x[n]) an (n-ary) rela‐
174 tion, and say that the relation is a subset of the Cartesian prod‐
175 uct X[1] x ... x X[n], where x[i] is an element of X[i], 1 <= i <=
176 n.
177
178 The projection of an n-ary relation R onto coordinate i is the set
179 {x[i] : (x[1], ..., x[i], ..., x[n]) in R for some x[j] in X[j], 1
180 <= j <= n and not i = j}. The projections of a binary relation R
181 onto the first and second coordinates are the domain and the range
182 of R, respectively.
183
184 The relative product of binary relations can be generalized to n-
185 ary relations as follows. Let TR be an ordered set (R[1], ...,
186 R[n]) of binary relations from X to Y[i] and S a binary relation
187 from (Y[1] x ... x Y[n]) to Z. The relative product of TR and S is
188 the binary relation T from X to Z defined so that x T z if and only
189 if there exists an element y[i] in Y[i] for each 1 <= i <= n such
190 that x R[i] y[i] and (y[1], ..., y[n]) S z. Now let TR be a an or‐
191 dered set (R[1], ..., R[n]) of binary relations from X[i] to Y[i]
192 and S a subset of X[1] x ... x X[n]. The multiple relative product
193 of TR and S is defined to be the set {z : z = ((x[1], ..., x[n]),
194 (y[1],...,y[n])) for some (x[1], ..., x[n]) in S and for some
195 (x[i], y[i]) in R[i], 1 <= i <= n}.
196
197 The natural join of an n-ary relation R and an m-ary relation S on
198 coordinate i and j is defined to be the set {z : z = (x[1], ...,
199 x[n], y[1], ..., y[j-1], y[j+1], ..., y[m]) for some (x[1], ...,
200 x[n]) in R and for some (y[1], ..., y[m]) in S such that x[i] =
201 y[j]}.
202
203 * The sets recognized by this module are represented by elements of
204 the relation Sets, which is defined as the smallest set such that:
205
206 * For every atom T, except '_', and for every term X, (T, X) be‐
207 longs to Sets (atomic sets).
208
209 * (['_'], []) belongs to Sets (the untyped empty set).
210
211 * For every tuple T = {T[1], ..., T[n]} and for every tuple X =
212 {X[1], ..., X[n]}, if (T[i], X[i]) belongs to Sets for every 1 <=
213 i <= n, then (T, X) belongs to Sets (ordered sets).
214
215 * For every term T, if X is the empty list or a non-empty sorted
216 list [X[1], ..., X[n]] without duplicates such that (T, X[i]) be‐
217 longs to Sets for every 1 <= i <= n, then ([T], X) belongs to
218 Sets (typed unordered sets).
219
220 An external set is an element of the range of Sets.
221
222 A type is an element of the domain of Sets.
223
224 If S is an element (T, X) of Sets, then T is a valid type of X, T
225 is the type of S, and X is the external set of S. from_term/2 cre‐
226 ates a set from a type and an Erlang term turned into an external
227 set.
228
229 The sets represented by Sets are the elements of the range of func‐
230 tion Set from Sets to Erlang terms and sets of Erlang terms:
231
232 * Set(T,Term) = Term, where T is an atom
233
234 * Set({T[1], ..., T[n]}, {X[1], ..., X[n]}) = (Set(T[1], X[1]),
235 ..., Set(T[n], X[n]))
236
237 * Set([T], [X[1], ..., X[n]]) = {Set(T, X[1]), ..., Set(T, X[n])}
238
239 * Set([T], []) = {}
240
241 When there is no risk of confusion, elements of Sets are identified
242 with the sets they represent. For example, if U is the result of
243 calling union/2 with S1 and S2 as arguments, then U is said to be
244 the union of S1 and S2. A more precise formulation is that Set(U)
245 is the union of Set(S1) and Set(S2).
246
247 The types are used to implement the various conditions that sets must
248 fulfill. As an example, consider the relative product of two sets R and
249 S, and recall that the relative product of R and S is defined if R is a
250 binary relation to Y and S is a binary relation from Y. The function
251 that implements the relative product, relative_product/2, checks that
252 the arguments represent binary relations by matching [{A,B}] against
253 the type of the first argument (Arg1 say), and [{C,D}] against the type
254 of the second argument (Arg2 say). The fact that [{A,B}] matches the
255 type of Arg1 is to be interpreted as Arg1 representing a binary rela‐
256 tion from X to Y, where X is defined as all sets Set(x) for some ele‐
257 ment x in Sets the type of which is A, and similarly for Y. In the same
258 way Arg2 is interpreted as representing a binary relation from W to Z.
259 Finally it is checked that B matches C, which is sufficient to ensure
260 that W is equal to Y. The untyped empty set is handled separately: its
261 type, ['_'], matches the type of any unordered set.
262
263 A few functions of this module (drestriction/3, family_projection/2,
264 partition/2, partition_family/2, projection/2, restriction/3, substitu‐
265 tion/2) accept an Erlang function as a means to modify each element of
266 a given unordered set. Such a function, called SetFun in the following,
267 can be specified as a functional object (fun), a tuple {external, Fun},
268 or an integer:
269
270 * If SetFun is specified as a fun, the fun is applied to each element
271 of the given set and the return value is assumed to be a set.
272
273 * If SetFun is specified as a tuple {external, Fun}, Fun is applied
274 to the external set of each element of the given set and the return
275 value is assumed to be an external set. Selecting the elements of
276 an unordered set as external sets and assembling a new unordered
277 set from a list of external sets is in the present implementation
278 more efficient than modifying each element as a set. However, this
279 optimization can only be used when the elements of the unordered
280 set are atomic or ordered sets. It must also be the case that the
281 type of the elements matches some clause of Fun (the type of the
282 created set is the result of applying Fun to the type of the given
283 set), and that Fun does nothing but selecting, duplicating, or re‐
284 arranging parts of the elements.
285
286 * Specifying a SetFun as an integer I is equivalent to specifying
287 {external, fun(X) -> element(I, X) end}, but is to be preferred, as
288 it makes it possible to handle this case even more efficiently.
289
290 Examples of SetFuns:
291
292 fun sofs:union/1
293 fun(S) -> sofs:partition(1, S) end
294 {external, fun(A) -> A end}
295 {external, fun({A,_,C}) -> {C,A} end}
296 {external, fun({_,{_,C}}) -> C end}
297 {external, fun({_,{_,{_,E}=C}}) -> {E,{E,C}} end}
298 2
299
300 The order in which a SetFun is applied to the elements of an unordered
301 set is not specified, and can change in future versions of this module.
302
303 The execution time of the functions of this module is dominated by the
304 time it takes to sort lists. When no sorting is needed, the execution
305 time is in the worst case proportional to the sum of the sizes of the
306 input arguments and the returned value. A few functions execute in con‐
307 stant time: from_external/2, is_empty_set/1, is_set/1, is_sofs_set/1,
308 to_external/1 type/1.
309
310 The functions of this module exit the process with a badarg, bad_func‐
311 tion, or type_mismatch message when given badly formed arguments or
312 sets the types of which are not compatible.
313
314 When comparing external sets, operator ==/2 is used.
315
317 anyset() = ordset() | a_set()
318
319 Any kind of set (also included are the atomic sets).
320
321 binary_relation() = relation()
322
323 A binary relation.
324
325 external_set() = term()
326
327 An external set.
328
329 family() = a_function()
330
331 A family (of subsets).
332
333 a_function() = relation()
334
335 A function.
336
337 ordset()
338
339 An ordered set.
340
341 relation() = a_set()
342
343 An n-ary relation.
344
345 a_set()
346
347 An unordered set.
348
349 set_of_sets() = a_set()
350
351 An unordered set of unordered sets.
352
353 set_fun() =
354 integer() >= 1 |
355 {external, fun((external_set()) -> external_set())} |
356 fun((anyset()) -> anyset())
357
358 A SetFun.
359
360 spec_fun() =
361 {external, fun((external_set()) -> boolean())} |
362 fun((anyset()) -> boolean())
363
364 type() = term()
365
366 A type.
367
368 tuple_of(T)
369
370 A tuple where the elements are of type T.
371
373 a_function(Tuples) -> Function
374
375 a_function(Tuples, Type) -> Function
376
377 Types:
378
379 Function = a_function()
380 Tuples = [tuple()]
381 Type = type()
382
383 Creates a function. a_function(F, T) is equivalent to
384 from_term(F, T) if the result is a function. If no type is ex‐
385 plicitly specified, [{atom, atom}] is used as the function type.
386
387 canonical_relation(SetOfSets) -> BinRel
388
389 Types:
390
391 BinRel = binary_relation()
392 SetOfSets = set_of_sets()
393
394 Returns the binary relation containing the elements (E, Set)
395 such that Set belongs to SetOfSets and E belongs to Set. If
396 SetOfSets is a partition of a set X and R is the equivalence re‐
397 lation in X induced by SetOfSets, then the returned relation is
398 the canonical map from X onto the equivalence classes with re‐
399 spect to R.
400
401 1> Ss = sofs:from_term([[a,b],[b,c]]),
402 CR = sofs:canonical_relation(Ss),
403 sofs:to_external(CR).
404 [{a,[a,b]},{b,[a,b]},{b,[b,c]},{c,[b,c]}]
405
406 composite(Function1, Function2) -> Function3
407
408 Types:
409
410 Function1 = Function2 = Function3 = a_function()
411
412 Returns the composite of the functions Function1 and Function2.
413
414 1> F1 = sofs:a_function([{a,1},{b,2},{c,2}]),
415 F2 = sofs:a_function([{1,x},{2,y},{3,z}]),
416 F = sofs:composite(F1, F2),
417 sofs:to_external(F).
418 [{a,x},{b,y},{c,y}]
419
420 constant_function(Set, AnySet) -> Function
421
422 Types:
423
424 AnySet = anyset()
425 Function = a_function()
426 Set = a_set()
427
428 Creates the function that maps each element of set Set onto Any‐
429 Set.
430
431 1> S = sofs:set([a,b]),
432 E = sofs:from_term(1),
433 R = sofs:constant_function(S, E),
434 sofs:to_external(R).
435 [{a,1},{b,1}]
436
437 converse(BinRel1) -> BinRel2
438
439 Types:
440
441 BinRel1 = BinRel2 = binary_relation()
442
443 Returns the converse of the binary relation BinRel1.
444
445 1> R1 = sofs:relation([{1,a},{2,b},{3,a}]),
446 R2 = sofs:converse(R1),
447 sofs:to_external(R2).
448 [{a,1},{a,3},{b,2}]
449
450 difference(Set1, Set2) -> Set3
451
452 Types:
453
454 Set1 = Set2 = Set3 = a_set()
455
456 Returns the difference of the sets Set1 and Set2.
457
458 digraph_to_family(Graph) -> Family
459
460 digraph_to_family(Graph, Type) -> Family
461
462 Types:
463
464 Graph = digraph:graph()
465 Family = family()
466 Type = type()
467
468 Creates a family from the directed graph Graph. Each vertex a of
469 Graph is represented by a pair (a, {b[1], ..., b[n]}), where the
470 b[i]:s are the out-neighbors of a. If no type is explicitly
471 specified, [{atom, [atom]}] is used as type of the family. It is
472 assumed that Type is a valid type of the external set of the
473 family.
474
475 If G is a directed graph, it holds that the vertices and edges
476 of G are the same as the vertices and edges of family_to_di‐
477 graph(digraph_to_family(G)).
478
479 domain(BinRel) -> Set
480
481 Types:
482
483 BinRel = binary_relation()
484 Set = a_set()
485
486 Returns the domain of the binary relation BinRel.
487
488 1> R = sofs:relation([{1,a},{1,b},{2,b},{2,c}]),
489 S = sofs:domain(R),
490 sofs:to_external(S).
491 [1,2]
492
493 drestriction(BinRel1, Set) -> BinRel2
494
495 Types:
496
497 BinRel1 = BinRel2 = binary_relation()
498 Set = a_set()
499
500 Returns the difference between the binary relation BinRel1 and
501 the restriction of BinRel1 to Set.
502
503 1> R1 = sofs:relation([{1,a},{2,b},{3,c}]),
504 S = sofs:set([2,4,6]),
505 R2 = sofs:drestriction(R1, S),
506 sofs:to_external(R2).
507 [{1,a},{3,c}]
508
509 drestriction(R, S) is equivalent to difference(R, restriction(R,
510 S)).
511
512 drestriction(SetFun, Set1, Set2) -> Set3
513
514 Types:
515
516 SetFun = set_fun()
517 Set1 = Set2 = Set3 = a_set()
518
519 Returns a subset of Set1 containing those elements that do not
520 give an element in Set2 as the result of applying SetFun.
521
522 1> SetFun = {external, fun({_A,B,C}) -> {B,C} end},
523 R1 = sofs:relation([{a,aa,1},{b,bb,2},{c,cc,3}]),
524 R2 = sofs:relation([{bb,2},{cc,3},{dd,4}]),
525 R3 = sofs:drestriction(SetFun, R1, R2),
526 sofs:to_external(R3).
527 [{a,aa,1}]
528
529 drestriction(F, S1, S2) is equivalent to difference(S1, restric‐
530 tion(F, S1, S2)).
531
532 empty_set() -> Set
533
534 Types:
535
536 Set = a_set()
537
538 Returns the untyped empty set. empty_set() is equivalent to
539 from_term([], ['_']).
540
541 extension(BinRel1, Set, AnySet) -> BinRel2
542
543 Types:
544
545 AnySet = anyset()
546 BinRel1 = BinRel2 = binary_relation()
547 Set = a_set()
548
549 Returns the extension of BinRel1 such that for each element E in
550 Set that does not belong to the domain of BinRel1, BinRel2 con‐
551 tains the pair (E, AnySet).
552
553 1> S = sofs:set([b,c]),
554 A = sofs:empty_set(),
555 R = sofs:family([{a,[1,2]},{b,[3]}]),
556 X = sofs:extension(R, S, A),
557 sofs:to_external(X).
558 [{a,[1,2]},{b,[3]},{c,[]}]
559
560 family(Tuples) -> Family
561
562 family(Tuples, Type) -> Family
563
564 Types:
565
566 Family = family()
567 Tuples = [tuple()]
568 Type = type()
569
570 Creates a family of subsets. family(F, T) is equivalent to
571 from_term(F, T) if the result is a family. If no type is explic‐
572 itly specified, [{atom, [atom]}] is used as the family type.
573
574 family_difference(Family1, Family2) -> Family3
575
576 Types:
577
578 Family1 = Family2 = Family3 = family()
579
580 If Family1 and Family2 are families, then Family3 is the family
581 such that the index set is equal to the index set of Family1,
582 and Family3[i] is the difference between Family1[i] and Fam‐
583 ily2[i] if Family2 maps i, otherwise Family1[i].
584
585 1> F1 = sofs:family([{a,[1,2]},{b,[3,4]}]),
586 F2 = sofs:family([{b,[4,5]},{c,[6,7]}]),
587 F3 = sofs:family_difference(F1, F2),
588 sofs:to_external(F3).
589 [{a,[1,2]},{b,[3]}]
590
591 family_domain(Family1) -> Family2
592
593 Types:
594
595 Family1 = Family2 = family()
596
597 If Family1 is a family and Family1[i] is a binary relation for
598 every i in the index set of Family1, then Family2 is the family
599 with the same index set as Family1 such that Family2[i] is the
600 domain of Family1[i].
601
602 1> FR = sofs:from_term([{a,[{1,a},{2,b},{3,c}]},{b,[]},{c,[{4,d},{5,e}]}]),
603 F = sofs:family_domain(FR),
604 sofs:to_external(F).
605 [{a,[1,2,3]},{b,[]},{c,[4,5]}]
606
607 family_field(Family1) -> Family2
608
609 Types:
610
611 Family1 = Family2 = family()
612
613 If Family1 is a family and Family1[i] is a binary relation for
614 every i in the index set of Family1, then Family2 is the family
615 with the same index set as Family1 such that Family2[i] is the
616 field of Family1[i].
617
618 1> FR = sofs:from_term([{a,[{1,a},{2,b},{3,c}]},{b,[]},{c,[{4,d},{5,e}]}]),
619 F = sofs:family_field(FR),
620 sofs:to_external(F).
621 [{a,[1,2,3,a,b,c]},{b,[]},{c,[4,5,d,e]}]
622
623 family_field(Family1) is equivalent to family_union(family_do‐
624 main(Family1), family_range(Family1)).
625
626 family_intersection(Family1) -> Family2
627
628 Types:
629
630 Family1 = Family2 = family()
631
632 If Family1 is a family and Family1[i] is a set of sets for every
633 i in the index set of Family1, then Family2 is the family with
634 the same index set as Family1 such that Family2[i] is the inter‐
635 section of Family1[i].
636
637 If Family1[i] is an empty set for some i, the process exits with
638 a badarg message.
639
640 1> F1 = sofs:from_term([{a,[[1,2,3],[2,3,4]]},{b,[[x,y,z],[x,y]]}]),
641 F2 = sofs:family_intersection(F1),
642 sofs:to_external(F2).
643 [{a,[2,3]},{b,[x,y]}]
644
645 family_intersection(Family1, Family2) -> Family3
646
647 Types:
648
649 Family1 = Family2 = Family3 = family()
650
651 If Family1 and Family2 are families, then Family3 is the family
652 such that the index set is the intersection of Family1:s and
653 Family2:s index sets, and Family3[i] is the intersection of Fam‐
654 ily1[i] and Family2[i].
655
656 1> F1 = sofs:family([{a,[1,2]},{b,[3,4]},{c,[5,6]}]),
657 F2 = sofs:family([{b,[4,5]},{c,[7,8]},{d,[9,10]}]),
658 F3 = sofs:family_intersection(F1, F2),
659 sofs:to_external(F3).
660 [{b,[4]},{c,[]}]
661
662 family_projection(SetFun, Family1) -> Family2
663
664 Types:
665
666 SetFun = set_fun()
667 Family1 = Family2 = family()
668
669 If Family1 is a family, then Family2 is the family with the same
670 index set as Family1 such that Family2[i] is the result of call‐
671 ing SetFun with Family1[i] as argument.
672
673 1> F1 = sofs:from_term([{a,[[1,2],[2,3]]},{b,[[]]}]),
674 F2 = sofs:family_projection(fun sofs:union/1, F1),
675 sofs:to_external(F2).
676 [{a,[1,2,3]},{b,[]}]
677
678 family_range(Family1) -> Family2
679
680 Types:
681
682 Family1 = Family2 = family()
683
684 If Family1 is a family and Family1[i] is a binary relation for
685 every i in the index set of Family1, then Family2 is the family
686 with the same index set as Family1 such that Family2[i] is the
687 range of Family1[i].
688
689 1> FR = sofs:from_term([{a,[{1,a},{2,b},{3,c}]},{b,[]},{c,[{4,d},{5,e}]}]),
690 F = sofs:family_range(FR),
691 sofs:to_external(F).
692 [{a,[a,b,c]},{b,[]},{c,[d,e]}]
693
694 family_specification(Fun, Family1) -> Family2
695
696 Types:
697
698 Fun = spec_fun()
699 Family1 = Family2 = family()
700
701 If Family1 is a family, then Family2 is the restriction of Fam‐
702 ily1 to those elements i of the index set for which Fun applied
703 to Family1[i] returns true. If Fun is a tuple {external, Fun2},
704 then Fun2 is applied to the external set of Family1[i], other‐
705 wise Fun is applied to Family1[i].
706
707 1> F1 = sofs:family([{a,[1,2,3]},{b,[1,2]},{c,[1]}]),
708 SpecFun = fun(S) -> sofs:no_elements(S) =:= 2 end,
709 F2 = sofs:family_specification(SpecFun, F1),
710 sofs:to_external(F2).
711 [{b,[1,2]}]
712
713 family_to_digraph(Family) -> Graph
714
715 family_to_digraph(Family, GraphType) -> Graph
716
717 Types:
718
719 Graph = digraph:graph()
720 Family = family()
721 GraphType = [digraph:d_type()]
722
723 Creates a directed graph from family Family. For each pair (a,
724 {b[1], ..., b[n]}) of Family, vertex a and the edges (a, b[i])
725 for 1 <= i <= n are added to a newly created directed graph.
726
727 If no graph type is specified, digraph:new/0 is used for creat‐
728 ing the directed graph, otherwise argument GraphType is passed
729 on as second argument to digraph:new/1.
730
731 It F is a family, it holds that F is a subset of digraph_to_fam‐
732 ily(family_to_digraph(F), type(F)). Equality holds if
733 union_of_family(F) is a subset of domain(F).
734
735 Creating a cycle in an acyclic graph exits the process with a
736 cyclic message.
737
738 family_to_relation(Family) -> BinRel
739
740 Types:
741
742 Family = family()
743 BinRel = binary_relation()
744
745 If Family is a family, then BinRel is the binary relation con‐
746 taining all pairs (i, x) such that i belongs to the index set of
747 Family and x belongs to Family[i].
748
749 1> F = sofs:family([{a,[]}, {b,[1]}, {c,[2,3]}]),
750 R = sofs:family_to_relation(F),
751 sofs:to_external(R).
752 [{b,1},{c,2},{c,3}]
753
754 family_union(Family1) -> Family2
755
756 Types:
757
758 Family1 = Family2 = family()
759
760 If Family1 is a family and Family1[i] is a set of sets for each
761 i in the index set of Family1, then Family2 is the family with
762 the same index set as Family1 such that Family2[i] is the union
763 of Family1[i].
764
765 1> F1 = sofs:from_term([{a,[[1,2],[2,3]]},{b,[[]]}]),
766 F2 = sofs:family_union(F1),
767 sofs:to_external(F2).
768 [{a,[1,2,3]},{b,[]}]
769
770 family_union(F) is equivalent to family_projection(fun
771 sofs:union/1, F).
772
773 family_union(Family1, Family2) -> Family3
774
775 Types:
776
777 Family1 = Family2 = Family3 = family()
778
779 If Family1 and Family2 are families, then Family3 is the family
780 such that the index set is the union of Family1:s and Family2:s
781 index sets, and Family3[i] is the union of Family1[i] and Fam‐
782 ily2[i] if both map i, otherwise Family1[i] or Family2[i].
783
784 1> F1 = sofs:family([{a,[1,2]},{b,[3,4]},{c,[5,6]}]),
785 F2 = sofs:family([{b,[4,5]},{c,[7,8]},{d,[9,10]}]),
786 F3 = sofs:family_union(F1, F2),
787 sofs:to_external(F3).
788 [{a,[1,2]},{b,[3,4,5]},{c,[5,6,7,8]},{d,[9,10]}]
789
790 field(BinRel) -> Set
791
792 Types:
793
794 BinRel = binary_relation()
795 Set = a_set()
796
797 Returns the field of the binary relation BinRel.
798
799 1> R = sofs:relation([{1,a},{1,b},{2,b},{2,c}]),
800 S = sofs:field(R),
801 sofs:to_external(S).
802 [1,2,a,b,c]
803
804 field(R) is equivalent to union(domain(R), range(R)).
805
806 from_external(ExternalSet, Type) -> AnySet
807
808 Types:
809
810 ExternalSet = external_set()
811 AnySet = anyset()
812 Type = type()
813
814 Creates a set from the external set ExternalSet and the type
815 Type. It is assumed that Type is a valid type of ExternalSet.
816
817 from_sets(ListOfSets) -> Set
818
819 Types:
820
821 Set = a_set()
822 ListOfSets = [anyset()]
823
824 Returns the unordered set containing the sets of list ListOf‐
825 Sets.
826
827 1> S1 = sofs:relation([{a,1},{b,2}]),
828 S2 = sofs:relation([{x,3},{y,4}]),
829 S = sofs:from_sets([S1,S2]),
830 sofs:to_external(S).
831 [[{a,1},{b,2}],[{x,3},{y,4}]]
832
833 from_sets(TupleOfSets) -> Ordset
834
835 Types:
836
837 Ordset = ordset()
838 TupleOfSets = tuple_of(anyset())
839
840 Returns the ordered set containing the sets of the non-empty tu‐
841 ple TupleOfSets.
842
843 from_term(Term) -> AnySet
844
845 from_term(Term, Type) -> AnySet
846
847 Types:
848
849 AnySet = anyset()
850 Term = term()
851 Type = type()
852
853 Creates an element of Sets by traversing term Term, sorting
854 lists, removing duplicates, and deriving or verifying a valid
855 type for the so obtained external set. An explicitly specified
856 type Type can be used to limit the depth of the traversal; an
857 atomic type stops the traversal, as shown by the following exam‐
858 ple where "foo" and {"foo"} are left unmodified:
859
860 1> S = sofs:from_term([{{"foo"},[1,1]},{"foo",[2,2]}], [{atom,[atom]}]),
861 sofs:to_external(S).
862 [{{"foo"},[1]},{"foo",[2]}]
863
864 from_term can be used for creating atomic or ordered sets. The
865 only purpose of such a set is that of later building unordered
866 sets, as all functions in this module that do anything operate
867 on unordered sets. Creating unordered sets from a collection of
868 ordered sets can be the way to go if the ordered sets are big
869 and one does not want to waste heap by rebuilding the elements
870 of the unordered set. The following example shows that a set can
871 be built "layer by layer":
872
873 1> A = sofs:from_term(a),
874 S = sofs:set([1,2,3]),
875 P1 = sofs:from_sets({A,S}),
876 P2 = sofs:from_term({b,[6,5,4]}),
877 Ss = sofs:from_sets([P1,P2]),
878 sofs:to_external(Ss).
879 [{a,[1,2,3]},{b,[4,5,6]}]
880
881 Other functions that create sets are from_external/2 and
882 from_sets/1. Special cases of from_term/2 are a_function/1,2,
883 empty_set/0, family/1,2, relation/1,2, and set/1,2.
884
885 image(BinRel, Set1) -> Set2
886
887 Types:
888
889 BinRel = binary_relation()
890 Set1 = Set2 = a_set()
891
892 Returns the image of set Set1 under the binary relation BinRel.
893
894 1> R = sofs:relation([{1,a},{2,b},{2,c},{3,d}]),
895 S1 = sofs:set([1,2]),
896 S2 = sofs:image(R, S1),
897 sofs:to_external(S2).
898 [a,b,c]
899
900 intersection(SetOfSets) -> Set
901
902 Types:
903
904 Set = a_set()
905 SetOfSets = set_of_sets()
906
907 Returns the intersection of the set of sets SetOfSets.
908
909 Intersecting an empty set of sets exits the process with a
910 badarg message.
911
912 intersection(Set1, Set2) -> Set3
913
914 Types:
915
916 Set1 = Set2 = Set3 = a_set()
917
918 Returns the intersection of Set1 and Set2.
919
920 intersection_of_family(Family) -> Set
921
922 Types:
923
924 Family = family()
925 Set = a_set()
926
927 Returns the intersection of family Family.
928
929 Intersecting an empty family exits the process with a badarg
930 message.
931
932 1> F = sofs:family([{a,[0,2,4]},{b,[0,1,2]},{c,[2,3]}]),
933 S = sofs:intersection_of_family(F),
934 sofs:to_external(S).
935 [2]
936
937 inverse(Function1) -> Function2
938
939 Types:
940
941 Function1 = Function2 = a_function()
942
943 Returns the inverse of function Function1.
944
945 1> R1 = sofs:relation([{1,a},{2,b},{3,c}]),
946 R2 = sofs:inverse(R1),
947 sofs:to_external(R2).
948 [{a,1},{b,2},{c,3}]
949
950 inverse_image(BinRel, Set1) -> Set2
951
952 Types:
953
954 BinRel = binary_relation()
955 Set1 = Set2 = a_set()
956
957 Returns the inverse image of Set1 under the binary relation Bin‐
958 Rel.
959
960 1> R = sofs:relation([{1,a},{2,b},{2,c},{3,d}]),
961 S1 = sofs:set([c,d,e]),
962 S2 = sofs:inverse_image(R, S1),
963 sofs:to_external(S2).
964 [2,3]
965
966 is_a_function(BinRel) -> Bool
967
968 Types:
969
970 Bool = boolean()
971 BinRel = binary_relation()
972
973 Returns true if the binary relation BinRel is a function or the
974 untyped empty set, otherwise false.
975
976 is_disjoint(Set1, Set2) -> Bool
977
978 Types:
979
980 Bool = boolean()
981 Set1 = Set2 = a_set()
982
983 Returns true if Set1 and Set2 are disjoint, otherwise false.
984
985 is_empty_set(AnySet) -> Bool
986
987 Types:
988
989 AnySet = anyset()
990 Bool = boolean()
991
992 Returns true if AnySet is an empty unordered set, otherwise
993 false.
994
995 is_equal(AnySet1, AnySet2) -> Bool
996
997 Types:
998
999 AnySet1 = AnySet2 = anyset()
1000 Bool = boolean()
1001
1002 Returns true if AnySet1 and AnySet2 are equal, otherwise false.
1003 The following example shows that ==/2 is used when comparing
1004 sets for equality:
1005
1006 1> S1 = sofs:set([1.0]),
1007 S2 = sofs:set([1]),
1008 sofs:is_equal(S1, S2).
1009 true
1010
1011 is_set(AnySet) -> Bool
1012
1013 Types:
1014
1015 AnySet = anyset()
1016 Bool = boolean()
1017
1018 Returns true if AnySet appears to be an unordered set, and false
1019 if AnySet is an ordered set or an atomic set or any other term.
1020 Note that the test is shallow and this function will return true
1021 for any term that coincides with the representation of an un‐
1022 ordered set. See also note on data types.
1023
1024 is_sofs_set(Term) -> Bool
1025
1026 Types:
1027
1028 Bool = boolean()
1029 Term = term()
1030
1031 Returns true if Term appears to be an unordered set, an ordered
1032 set, or an atomic set, otherwise false. Note that this function
1033 will return true for any term that coincides with the represen‐
1034 tation of a sofs set. See also note on data types.
1035
1036 is_subset(Set1, Set2) -> Bool
1037
1038 Types:
1039
1040 Bool = boolean()
1041 Set1 = Set2 = a_set()
1042
1043 Returns true if Set1 is a subset of Set2, otherwise false.
1044
1045 is_type(Term) -> Bool
1046
1047 Types:
1048
1049 Bool = boolean()
1050 Term = term()
1051
1052 Returns true if term Term is a type.
1053
1054 join(Relation1, I, Relation2, J) -> Relation3
1055
1056 Types:
1057
1058 Relation1 = Relation2 = Relation3 = relation()
1059 I = J = integer() >= 1
1060
1061 Returns the natural join of the relations Relation1 and Rela‐
1062 tion2 on coordinates I and J.
1063
1064 1> R1 = sofs:relation([{a,x,1},{b,y,2}]),
1065 R2 = sofs:relation([{1,f,g},{1,h,i},{2,3,4}]),
1066 J = sofs:join(R1, 3, R2, 1),
1067 sofs:to_external(J).
1068 [{a,x,1,f,g},{a,x,1,h,i},{b,y,2,3,4}]
1069
1070 multiple_relative_product(TupleOfBinRels, BinRel1) -> BinRel2
1071
1072 Types:
1073
1074 TupleOfBinRels = tuple_of(BinRel)
1075 BinRel = BinRel1 = BinRel2 = binary_relation()
1076
1077 If TupleOfBinRels is a non-empty tuple {R[1], ..., R[n]} of bi‐
1078 nary relations and BinRel1 is a binary relation, then BinRel2 is
1079 the multiple relative product of the ordered set (R[i], ...,
1080 R[n]) and BinRel1.
1081
1082 1> Ri = sofs:relation([{a,1},{b,2},{c,3}]),
1083 R = sofs:relation([{a,b},{b,c},{c,a}]),
1084 MP = sofs:multiple_relative_product({Ri, Ri}, R),
1085 sofs:to_external(sofs:range(MP)).
1086 [{1,2},{2,3},{3,1}]
1087
1088 no_elements(ASet) -> NoElements
1089
1090 Types:
1091
1092 ASet = a_set() | ordset()
1093 NoElements = integer() >= 0
1094
1095 Returns the number of elements of the ordered or unordered set
1096 ASet.
1097
1098 partition(SetOfSets) -> Partition
1099
1100 Types:
1101
1102 SetOfSets = set_of_sets()
1103 Partition = a_set()
1104
1105 Returns the partition of the union of the set of sets SetOfSets
1106 such that two elements are considered equal if they belong to
1107 the same elements of SetOfSets.
1108
1109 1> Sets1 = sofs:from_term([[a,b,c],[d,e,f],[g,h,i]]),
1110 Sets2 = sofs:from_term([[b,c,d],[e,f,g],[h,i,j]]),
1111 P = sofs:partition(sofs:union(Sets1, Sets2)),
1112 sofs:to_external(P).
1113 [[a],[b,c],[d],[e,f],[g],[h,i],[j]]
1114
1115 partition(SetFun, Set) -> Partition
1116
1117 Types:
1118
1119 SetFun = set_fun()
1120 Partition = Set = a_set()
1121
1122 Returns the partition of Set such that two elements are consid‐
1123 ered equal if the results of applying SetFun are equal.
1124
1125 1> Ss = sofs:from_term([[a],[b],[c,d],[e,f]]),
1126 SetFun = fun(S) -> sofs:from_term(sofs:no_elements(S)) end,
1127 P = sofs:partition(SetFun, Ss),
1128 sofs:to_external(P).
1129 [[[a],[b]],[[c,d],[e,f]]]
1130
1131 partition(SetFun, Set1, Set2) -> {Set3, Set4}
1132
1133 Types:
1134
1135 SetFun = set_fun()
1136 Set1 = Set2 = Set3 = Set4 = a_set()
1137
1138 Returns a pair of sets that, regarded as constituting a set,
1139 forms a partition of Set1. If the result of applying SetFun to
1140 an element of Set1 gives an element in Set2, the element belongs
1141 to Set3, otherwise the element belongs to Set4.
1142
1143 1> R1 = sofs:relation([{1,a},{2,b},{3,c}]),
1144 S = sofs:set([2,4,6]),
1145 {R2,R3} = sofs:partition(1, R1, S),
1146 {sofs:to_external(R2),sofs:to_external(R3)}.
1147 {[{2,b}],[{1,a},{3,c}]}
1148
1149 partition(F, S1, S2) is equivalent to {restriction(F, S1, S2),
1150 drestriction(F, S1, S2)}.
1151
1152 partition_family(SetFun, Set) -> Family
1153
1154 Types:
1155
1156 Family = family()
1157 SetFun = set_fun()
1158 Set = a_set()
1159
1160 Returns family Family where the indexed set is a partition of
1161 Set such that two elements are considered equal if the results
1162 of applying SetFun are the same value i. This i is the index
1163 that Family maps onto the equivalence class.
1164
1165 1> S = sofs:relation([{a,a,a,a},{a,a,b,b},{a,b,b,b}]),
1166 SetFun = {external, fun({A,_,C,_}) -> {A,C} end},
1167 F = sofs:partition_family(SetFun, S),
1168 sofs:to_external(F).
1169 [{{a,a},[{a,a,a,a}]},{{a,b},[{a,a,b,b},{a,b,b,b}]}]
1170
1171 product(TupleOfSets) -> Relation
1172
1173 Types:
1174
1175 Relation = relation()
1176 TupleOfSets = tuple_of(a_set())
1177
1178 Returns the Cartesian product of the non-empty tuple of sets Tu‐
1179 pleOfSets. If (x[1], ..., x[n]) is an element of the n-ary rela‐
1180 tion Relation, then x[i] is drawn from element i of TupleOfSets.
1181
1182 1> S1 = sofs:set([a,b]),
1183 S2 = sofs:set([1,2]),
1184 S3 = sofs:set([x,y]),
1185 P3 = sofs:product({S1,S2,S3}),
1186 sofs:to_external(P3).
1187 [{a,1,x},{a,1,y},{a,2,x},{a,2,y},{b,1,x},{b,1,y},{b,2,x},{b,2,y}]
1188
1189 product(Set1, Set2) -> BinRel
1190
1191 Types:
1192
1193 BinRel = binary_relation()
1194 Set1 = Set2 = a_set()
1195
1196 Returns the Cartesian product of Set1 and Set2.
1197
1198 1> S1 = sofs:set([1,2]),
1199 S2 = sofs:set([a,b]),
1200 R = sofs:product(S1, S2),
1201 sofs:to_external(R).
1202 [{1,a},{1,b},{2,a},{2,b}]
1203
1204 product(S1, S2) is equivalent to product({S1, S2}).
1205
1206 projection(SetFun, Set1) -> Set2
1207
1208 Types:
1209
1210 SetFun = set_fun()
1211 Set1 = Set2 = a_set()
1212
1213 Returns the set created by substituting each element of Set1 by
1214 the result of applying SetFun to the element.
1215
1216 If SetFun is a number i >= 1 and Set1 is a relation, then the
1217 returned set is the projection of Set1 onto coordinate i.
1218
1219 1> S1 = sofs:from_term([{1,a},{2,b},{3,a}]),
1220 S2 = sofs:projection(2, S1),
1221 sofs:to_external(S2).
1222 [a,b]
1223
1224 range(BinRel) -> Set
1225
1226 Types:
1227
1228 BinRel = binary_relation()
1229 Set = a_set()
1230
1231 Returns the range of the binary relation BinRel.
1232
1233 1> R = sofs:relation([{1,a},{1,b},{2,b},{2,c}]),
1234 S = sofs:range(R),
1235 sofs:to_external(S).
1236 [a,b,c]
1237
1238 relation(Tuples) -> Relation
1239
1240 relation(Tuples, Type) -> Relation
1241
1242 Types:
1243
1244 N = integer()
1245 Type = N | type()
1246 Relation = relation()
1247 Tuples = [tuple()]
1248
1249 Creates a relation. relation(R, T) is equivalent to from_term(R,
1250 T), if T is a type and the result is a relation. If Type is an
1251 integer N, then [{atom, ..., atom}]), where the tuple size is N,
1252 is used as type of the relation. If no type is explicitly speci‐
1253 fied, the size of the first tuple of Tuples is used if there is
1254 such a tuple. relation([]) is equivalent to relation([], 2).
1255
1256 relation_to_family(BinRel) -> Family
1257
1258 Types:
1259
1260 Family = family()
1261 BinRel = binary_relation()
1262
1263 Returns family Family such that the index set is equal to the
1264 domain of the binary relation BinRel, and Family[i] is the image
1265 of the set of i under BinRel.
1266
1267 1> R = sofs:relation([{b,1},{c,2},{c,3}]),
1268 F = sofs:relation_to_family(R),
1269 sofs:to_external(F).
1270 [{b,[1]},{c,[2,3]}]
1271
1272 relative_product(ListOfBinRels) -> BinRel2
1273
1274 relative_product(ListOfBinRels, BinRel1) -> BinRel2
1275
1276 Types:
1277
1278 ListOfBinRels = [BinRel, ...]
1279 BinRel = BinRel1 = BinRel2 = binary_relation()
1280
1281 If ListOfBinRels is a non-empty list [R[1], ..., R[n]] of binary
1282 relations and BinRel1 is a binary relation, then BinRel2 is the
1283 relative product of the ordered set (R[i], ..., R[n]) and Bin‐
1284 Rel1.
1285
1286 If BinRel1 is omitted, the relation of equality between the ele‐
1287 ments of the Cartesian product of the ranges of R[i], range R[1]
1288 x ... x range R[n], is used instead (intuitively, nothing is
1289 "lost").
1290
1291 1> TR = sofs:relation([{1,a},{1,aa},{2,b}]),
1292 R1 = sofs:relation([{1,u},{2,v},{3,c}]),
1293 R2 = sofs:relative_product([TR, R1]),
1294 sofs:to_external(R2).
1295 [{1,{a,u}},{1,{aa,u}},{2,{b,v}}]
1296
1297 Notice that relative_product([R1], R2) is different from rela‐
1298 tive_product(R1, R2); the list of one element is not identified
1299 with the element itself.
1300
1301 relative_product(BinRel1, BinRel2) -> BinRel3
1302
1303 Types:
1304
1305 BinRel1 = BinRel2 = BinRel3 = binary_relation()
1306
1307 Returns the relative product of the binary relations BinRel1 and
1308 BinRel2.
1309
1310 relative_product1(BinRel1, BinRel2) -> BinRel3
1311
1312 Types:
1313
1314 BinRel1 = BinRel2 = BinRel3 = binary_relation()
1315
1316 Returns the relative product of the converse of the binary rela‐
1317 tion BinRel1 and the binary relation BinRel2.
1318
1319 1> R1 = sofs:relation([{1,a},{1,aa},{2,b}]),
1320 R2 = sofs:relation([{1,u},{2,v},{3,c}]),
1321 R3 = sofs:relative_product1(R1, R2),
1322 sofs:to_external(R3).
1323 [{a,u},{aa,u},{b,v}]
1324
1325 relative_product1(R1, R2) is equivalent to relative_product(con‐
1326 verse(R1), R2).
1327
1328 restriction(BinRel1, Set) -> BinRel2
1329
1330 Types:
1331
1332 BinRel1 = BinRel2 = binary_relation()
1333 Set = a_set()
1334
1335 Returns the restriction of the binary relation BinRel1 to Set.
1336
1337 1> R1 = sofs:relation([{1,a},{2,b},{3,c}]),
1338 S = sofs:set([1,2,4]),
1339 R2 = sofs:restriction(R1, S),
1340 sofs:to_external(R2).
1341 [{1,a},{2,b}]
1342
1343 restriction(SetFun, Set1, Set2) -> Set3
1344
1345 Types:
1346
1347 SetFun = set_fun()
1348 Set1 = Set2 = Set3 = a_set()
1349
1350 Returns a subset of Set1 containing those elements that gives an
1351 element in Set2 as the result of applying SetFun.
1352
1353 1> S1 = sofs:relation([{1,a},{2,b},{3,c}]),
1354 S2 = sofs:set([b,c,d]),
1355 S3 = sofs:restriction(2, S1, S2),
1356 sofs:to_external(S3).
1357 [{2,b},{3,c}]
1358
1359 set(Terms) -> Set
1360
1361 set(Terms, Type) -> Set
1362
1363 Types:
1364
1365 Set = a_set()
1366 Terms = [term()]
1367 Type = type()
1368
1369 Creates an unordered set. set(L, T) is equivalent to
1370 from_term(L, T), if the result is an unordered set. If no type
1371 is explicitly specified, [atom] is used as the set type.
1372
1373 specification(Fun, Set1) -> Set2
1374
1375 Types:
1376
1377 Fun = spec_fun()
1378 Set1 = Set2 = a_set()
1379
1380 Returns the set containing every element of Set1 for which Fun
1381 returns true. If Fun is a tuple {external, Fun2}, Fun2 is ap‐
1382 plied to the external set of each element, otherwise Fun is ap‐
1383 plied to each element.
1384
1385 1> R1 = sofs:relation([{a,1},{b,2}]),
1386 R2 = sofs:relation([{x,1},{x,2},{y,3}]),
1387 S1 = sofs:from_sets([R1,R2]),
1388 S2 = sofs:specification(fun sofs:is_a_function/1, S1),
1389 sofs:to_external(S2).
1390 [[{a,1},{b,2}]]
1391
1392 strict_relation(BinRel1) -> BinRel2
1393
1394 Types:
1395
1396 BinRel1 = BinRel2 = binary_relation()
1397
1398 Returns the strict relation corresponding to the binary relation
1399 BinRel1.
1400
1401 1> R1 = sofs:relation([{1,1},{1,2},{2,1},{2,2}]),
1402 R2 = sofs:strict_relation(R1),
1403 sofs:to_external(R2).
1404 [{1,2},{2,1}]
1405
1406 substitution(SetFun, Set1) -> Set2
1407
1408 Types:
1409
1410 SetFun = set_fun()
1411 Set1 = Set2 = a_set()
1412
1413 Returns a function, the domain of which is Set1. The value of an
1414 element of the domain is the result of applying SetFun to the
1415 element.
1416
1417 1> L = [{a,1},{b,2}].
1418 [{a,1},{b,2}]
1419 2> sofs:to_external(sofs:projection(1,sofs:relation(L))).
1420 [a,b]
1421 3> sofs:to_external(sofs:substitution(1,sofs:relation(L))).
1422 [{{a,1},a},{{b,2},b}]
1423 4> SetFun = {external, fun({A,_}=E) -> {E,A} end},
1424 sofs:to_external(sofs:projection(SetFun,sofs:relation(L))).
1425 [{{a,1},a},{{b,2},b}]
1426
1427 The relation of equality between the elements of {a,b,c}:
1428
1429 1> I = sofs:substitution(fun(A) -> A end, sofs:set([a,b,c])),
1430 sofs:to_external(I).
1431 [{a,a},{b,b},{c,c}]
1432
1433 Let SetOfSets be a set of sets and BinRel a binary relation. The
1434 function that maps each element Set of SetOfSets onto the image
1435 of Set under BinRel is returned by the following function:
1436
1437 images(SetOfSets, BinRel) ->
1438 Fun = fun(Set) -> sofs:image(BinRel, Set) end,
1439 sofs:substitution(Fun, SetOfSets).
1440
1441 External unordered sets are represented as sorted lists. So,
1442 creating the image of a set under a relation R can traverse all
1443 elements of R (to that comes the sorting of results, the image).
1444 In image/2, BinRel is traversed once for each element of SetOf‐
1445 Sets, which can take too long. The following efficient function
1446 can be used instead under the assumption that the image of each
1447 element of SetOfSets under BinRel is non-empty:
1448
1449 images2(SetOfSets, BinRel) ->
1450 CR = sofs:canonical_relation(SetOfSets),
1451 R = sofs:relative_product1(CR, BinRel),
1452 sofs:relation_to_family(R).
1453
1454 symdiff(Set1, Set2) -> Set3
1455
1456 Types:
1457
1458 Set1 = Set2 = Set3 = a_set()
1459
1460 Returns the symmetric difference (or the Boolean sum) of Set1
1461 and Set2.
1462
1463 1> S1 = sofs:set([1,2,3]),
1464 S2 = sofs:set([2,3,4]),
1465 P = sofs:symdiff(S1, S2),
1466 sofs:to_external(P).
1467 [1,4]
1468
1469 symmetric_partition(Set1, Set2) -> {Set3, Set4, Set5}
1470
1471 Types:
1472
1473 Set1 = Set2 = Set3 = Set4 = Set5 = a_set()
1474
1475 Returns a triple of sets:
1476
1477 * Set3 contains the elements of Set1 that do not belong to
1478 Set2.
1479
1480 * Set4 contains the elements of Set1 that belong to Set2.
1481
1482 * Set5 contains the elements of Set2 that do not belong to
1483 Set1.
1484
1485 to_external(AnySet) -> ExternalSet
1486
1487 Types:
1488
1489 ExternalSet = external_set()
1490 AnySet = anyset()
1491
1492 Returns the external set of an atomic, ordered, or unordered
1493 set.
1494
1495 to_sets(ASet) -> Sets
1496
1497 Types:
1498
1499 ASet = a_set() | ordset()
1500 Sets = tuple_of(AnySet) | [AnySet]
1501 AnySet = anyset()
1502
1503 Returns the elements of the ordered set ASet as a tuple of sets,
1504 and the elements of the unordered set ASet as a sorted list of
1505 sets without duplicates.
1506
1507 type(AnySet) -> Type
1508
1509 Types:
1510
1511 AnySet = anyset()
1512 Type = type()
1513
1514 Returns the type of an atomic, ordered, or unordered set.
1515
1516 union(SetOfSets) -> Set
1517
1518 Types:
1519
1520 Set = a_set()
1521 SetOfSets = set_of_sets()
1522
1523 Returns the union of the set of sets SetOfSets.
1524
1525 union(Set1, Set2) -> Set3
1526
1527 Types:
1528
1529 Set1 = Set2 = Set3 = a_set()
1530
1531 Returns the union of Set1 and Set2.
1532
1533 union_of_family(Family) -> Set
1534
1535 Types:
1536
1537 Family = family()
1538 Set = a_set()
1539
1540 Returns the union of family Family.
1541
1542 1> F = sofs:family([{a,[0,2,4]},{b,[0,1,2]},{c,[2,3]}]),
1543 S = sofs:union_of_family(F),
1544 sofs:to_external(S).
1545 [0,1,2,3,4]
1546
1547 weak_relation(BinRel1) -> BinRel2
1548
1549 Types:
1550
1551 BinRel1 = BinRel2 = binary_relation()
1552
1553 Returns a subset S of the weak relation W corresponding to the
1554 binary relation BinRel1. Let F be the field of BinRel1. The sub‐
1555 set S is defined so that x S y if x W y for some x in F and for
1556 some y in F.
1557
1558 1> R1 = sofs:relation([{1,1},{1,2},{3,1}]),
1559 R2 = sofs:weak_relation(R1),
1560 sofs:to_external(R2).
1561 [{1,1},{1,2},{2,2},{3,1},{3,3}]
1562
1564 dict(3), digraph(3), orddict(3), ordsets(3), sets(3)
1565
1566
1567
1568Ericsson AB stdlib 4.2 sofs(3)