1sofs(3)                    Erlang Module Definition                    sofs(3)
2
3
4

NAME

6       sofs - Functions for manipulating sets of sets.
7

DESCRIPTION

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

DATA TYPES

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

EXPORTS

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

SEE ALSO

1564       dict(3), digraph(3), orddict(3), ordsets(3), sets(3)
1565
1566
1567
1568Ericsson AB                       stdlib 4.2                           sofs(3)
Impressum