.Open Sets
This introduces set theory from the point of view of a computer
professional using ASCII.
For the traditional notation see
.See http://www.math.csusb.edu/notes/sets/sets.html
There is a less formal introduction to this theory in
.See http://www.csci.csusb.edu/dick/maths/intro_sets.html
. Rapid History
Sets are implicit in much of Aristotelian logic (Ancient Greece... Medieval).
George Cantor (1800's) developed the theory as part of his research into
the mathematics of infinity. Sets rapidly became the language of modern
mathematics. Russell (1990's) uncovered paradoxes in the Cantor theory.
This lead to the Zermelo-Frankel axiomatic theory($THEORY below), Halmos's
Naive set theory, and Whitehead and Russell's Theory of Types.
. Introduction
These notes are about a language that lets talk both naturally and
rigorously at the same time. Everyday language is full of references to
sets of objects, classes, types of things, and on. The simple notation
proposed here makes much of this rigorous. Sets also form a foundation for
several more complex ideas which together form a simple yet effective way
of talking about complex systems and so software - such IBM's CICS(Customer
Information C?? Systems), elevators, or Hotel Bookings for example.
The classic argument looks like this in the language of sets:
.Let
Socrates is_a Human,
Human are Mortal.
()|- Socrates is_a Mortal.
.Close.Let
Here is another example, using the language of sets we can say:
birds ==> fly,
all birds fly.
penguins ==> birds,
penguins are birds.
And so conclude (in the face of the evidence):
penguins ==> fly.
So we might rethink our assumptions:
birds = flightless | flying.
Birds are flying or flightless.
This might lead us to think about how big the various sets are
and conclude that most birds are not flightless...
. Types
Every object belongs to a type T -- where the type describes the kind of
things that can be done to the object or could produce objects of the type.
For any type T there is an another type symbolized by @T with objects that
are sets of objects of type T.
.Note
THEORY::=Net{
The use of sets is only distantly related to the theories of sets developed
my mathematicians and logicians between 1850 through about 1940:
.See http://www/dick/maths/logic_32_Set_Theory.html
}=::THEORY.
A key point is that in theory one can re-express statements in MATHS
that use sets into expressions that use predicates instead.
Some sets are not types - A type by definition is a universal set or
domain of discourse, but a set is determined by the type of element
plus some
rule(predicate) indicating what is in the set.
We assume that whenever we have a set of some kind or other than it is a
set of objects of the same type. However a subset (or a `set` for short)
does belong to a type and so determines the types of the elements in it.
It is therefore safe to use a subset of a type in a declaration of a
variable of the right type, and with values/properties limited to those of
the set(compare type and subtype in Ada).
The restriction that each set has elements all of the same type is not a
particularly restrictive rule given the freedom with which we can construct
types as we need them.
The main expressions involving sets in MATHS are:
.Open Set Expressions
. Constructors
.Table Form Meaning Type (Notes)
.Row {} $() null set Ambiguous type.
.Row T universal set @T
.Row {e1} $(e1) set(e1) singleton @T (e1:T)
.Row e1 {e1} @type(e1) (only if context requires a set)
.Row {e1,e2,e3,...} set(e1,e2,e3,...) $(e1,e2,e3,...) set of enumerated items @T (extension)
.Row {x:T || W(x)} {x:T. W(x)} $[x:T](W(x)) set(x:T WHERE W(x)) set of things satisfying a property W @T (intension)
.Row {e(x) || x:S, W(x)} {e(x). x:S, W(x)} set of vales of e(x) for som x satisfying W(x) @T (comprehension)
.Row $ Net{...} structured set type(Net{...})
.Row $ Name set of elements with structure Name type(Name)
.Close.Table
There is also a more readable format that is suitable for large sets made up of
complex objects --
.See Long Format
below.
. Long Format Representation
For example
my_pets::@Animals=following,
.Set
stranger, AKA "Megan"
shadow
ginger
.Close.Set
The raw source code is:
.As_is .Set
.As_is element
.As_is element, comment.
.As_is ...
.As_is .Close.Set
An element in a long set can be several lines long. It starts with an
indentation. Each element is an expression and may
be terminated by a comma and a comment. Comments are ignored.
Long sets are normally used with a definition like this:
.As_is Name::@Type = following,
When rendered for display or printing a long set
should shown as an unordered list with
each element marked with a bullet or similar marker.
. Enumerating Finite Sets
In computing and software engineering we often need to introduce
and then describe
a finite set of distinct named elements. One way to this is:
.Box
Instead of
.As_is T::Sets,
.As_is e1::T,
.As_is e2::T,
.As_is ...
.As_is e[n]::T,
.As_is |- T = {e1,e2,...e[n]}.
.Close.Box
If the elements e1,e2,...,e[n] are distinct and free identifiers
then
the following syntax is natural short hand:
.As_is T::={e1,e2,...,e[n]}
It defines T and declares the elements in T.
For example:
.As_is Direction::={down, up}.
means
.Box
.As_is Direction::Sets.
.As_is down::Direction.
.As_is up::Direction.
.As_is |- Direction={down, up}.
.Close.Box
Note, that the above does not guarantee that the elements
have to be different -- even if we use different identifiers for the
elements. As written, it is possible for some else to take our document
and reuse it with a substitution which makes two variables the same.
To stop this, and to be very clear about what we want we must add
extra assumptions like this:
.As_is Direction::={down, up}.
.As_is |- down <> up.
or
.As_is Lights::={Green, Amber, Red}.
.As_is |- 3 Lights.
See $Cardinality below.
This is a little clumsy and counter-intuitive, and so I may
add a new notation that handles this.
If you want the elements to be in order then see
.See http://www/dick/maths/math_77_Enumerations.html
. Summary of Set Operators
.Table Symbols Example Meaning Type
.Row & \cap AND S1 & S2 Intersection @T><@T->@T
.Row & \cap AND & \beta Intersection @@T->@T
.Row | \cup OR S1|S2 union @T><@T->@T
.Row | \cup OR |\beta union @@T->@T
.Row ~ NOT S1 ~ S2 Complement @T><@T->@T
.Row @ \powset SetOf @S1 powerset,set_of_subsets @T->@@T
.Row >< Product S1><@T->@(T><@T->@
.Row <> S1 <> S2 inequality @T><@T->@
.Row != S1 != S2 inequality @T><@T->@
.Row == S1 == S2 equality @T><@T->@
.Row ==> ARE S1 ==> S2 subset or equal, \subseteq @T><@T->@
.Row =>> S1 =>> S2 proper subset, \subset @T><@T->@
.Row some some S1 S1<>{} @T->@
.Row - S1 some S1 @T->@
.Row no no S1 S1={} @T->@
.Row all all S1 S1=T @T->@
.Row and S1 and S2 some(S1&S2) @T->@
.Close.Table
.Close
. Syntax of Set Expressions
propositional_expression::= set_theoretical_proposition |...,
set_theoretical_proposition::= |[T:Types] (expression(T) "in"
expression(@T) | expression(@T) "=" expression(@T) | expression(@T)),
For T:Types, expression(@T) ::= simple_set_expression | union |
intersection,
union::= SERIAL($intersection,"|"),
.As_is Dog | Cat
intersection::= SERIAL($complementary_set_expression,"&"),
.As_is Shot_haired & Barkless & Dog
complementary_set_expression::= $Cartesian_product | complementary_set_expression $complement $Cartesian_product.
complement::="but_not" | "~", The text form is used in EBCDIC.
.As_is Animal~Dog
.As_is Animal~Dog~Cat
Note. The above definition is expressed recursively to express the associativity of
complements:
A~B~C = (A~B)~C.
$complementary_set_expression = $Cartesian_Product #($complement $Cartesian_product).
Cartesian_product::= SERIAL($possible_prefix_set_expression, "><").
Note: Cartesian products are sets of pairs of elements and are actually
a subset of a different type.
.As_is Point = Real >< Real.
possible_prefixed_set_expression::= #( "|" | "&") $simple_set_expression.
Note: in fact the simple expression must return a set of sets for a prefix
to be OK. If there are 2 prefixes then it must be a set of set of sets.
.As_is |{ {1,2}, {2,3} }
= {1, 2, 3}.
.As_is &{ {1,2}, {2,3} }
= {2}.
simple_set_expression::=set_name | elementary_set |"("$set_expression")" |
set_of_sets | set_of_maps | set_of_relations |
simple_set_expression"."relational_expression | relational_expression
"("set_expression")".
.As_is Animal
.As_is { shadow, ginger }
.As_is ( A \cup B ~ C )
.As_is @Animal
.As_is A<>->B
.As_is shadow.breeds
.As_is breeds(shadow)
set_of_sets::= "@" simple_set_expression | simple_set_expression "@" expression(Nat0).
.As_is @Animals
.As_is Animals@2
@A = { B | B==>A }.
A@n = { B:@A | Card(B) = n }.
.Box
A@n was new and tentative on Thu Aug 19 at 11:20:05 PDT 1999
but became standard notation
2008-06-27 Fri Jun 27 08:06 .
.Close.Box
elementary_set::= intention | extension |comprehension | singleton | empty_set |type_name
| "$"structure_description,
empty_set::="{}"|"$()",
Note "{}" is ambiguous as to type.... is a setof no animals, or a set of no real numbers.
The type of "{}" needs to be worked out from the context. To remove the ambiguity use
.As_is {}.@Animal
intention::= "{" loose_binding #(","loose_binding ) "||" proposition "}" | "$" loose_bindings "(" proposition ")",
comprehension::= "{" expression $where_lexeme loose_binding #(","loose_binding ) "." proposition "}",
where_lexeme::="||" | "." .
extension::= finite_extension |informal_extension,
finite_extension::="{" list_of_elements "}"| "$(" list_of_elements ")"
informal_extension::= "{" list_of_elements "..." "}"|"$(" list_of_elements
"..." ")",
An informal extension will stop most automatic proof checkers from
validating results.
list_of_elements ::= element #(punctuation element),
singleton::= "{"element"}" | "$(" element ")".
For Type T, e:T, e::@T={e}.
element::= expression,
MATHS has a special way to define a set - by describing it as a collection
of tuples under some constraint. Any piece of documentation contains
declarations and axioms that can be interpreted this way. Examples might
be:
my_circle::=$ Net{x,y:Real, x^2+y^2=y^2 },
CIRCLE::=Net{x,y:Real, r:Real, x0,y0:Real, (x-x0)^2+(y-y0)^2=r^2 },
(CIRCLE)|- my_circle=$ $CIRCLE(r=>1, (x0,y0)=>(0,0)}
structure_description::= "$" documentation,
.See http://www/dick/maths/notn_13_Docn_Syntax.html
and
.See http://www/dick/maths/notn_14_Docn_Semantics.html
structure_expression::=R(expression),
.See http://www/dick/maths/notn_12_Expressions.html
|- structure_expression= "(" identifier "=>" expression #( (|",")
identifier "=>" expression) ")",
.Open Semantics of Set Expressions
. Definitions
(intension_semantics): For Type T, W:predicate, x:variable(T), {x:T||W(x)}::@T= `set of all x in T
that satisfy W(x)`.
(in): For Type T, A:@T, t:T, t in A ::@=`it is true that t is a member of
set A`.
|- (set0): t in {x:T||W(x)} iff W(t).
.Key null set or empty set
{}::@T= {x:T||false},
Note "{}" the type of "{}" above is @T and not determined by the symbol itself.
It is determined by the context of the symbol. To remove all ambiguity use the standard
MATHS technique of using ".type" to define the type.
|- (unambiguous_null_set): {}.@T = {x:T||false}.
.Key Universal set
T::@T= {x:T||true},
(singleton_semantics): For a,b,c,...: T, {a}::@T={x:T||x=a}.
(coerced_singleton): For a,b,c,...: T, a::@T={a}.
(extension_semantics): For a,b,c,...: T, {a,b,c,...} ::@T= {a} | {b} | {c}|... .
(projection_semantics): For f,x,W, {f(x) || for some x:T (W)}::= {y || for some x:T(y=f(x) and (W))}.
For f,x,X,W, {f(x) || x:X}::= {y || for some x:X(y=f(x))}.
(Comprehension semantics): an expression like {e || x:X, y:Y, ..., W} should be interpreted as a generalisation of the above whenever e is an expression and W a proposition:
{z || for some x:X, y:Y, ... (z=e and (W))}
If the W is missing it should be taken to be true.
For example
even = { 2*n || n:Nat0 }.
Note. This is one place where variables are declared after they are used.
(Set Operators)|- (union_semantics): For A,B: @T, A | B = {x:T || x in A or x in B }.
(Set Operators)|- (intersection_semantics): For A,B: @T, A & B = {x:T || x in A and x in B }.
(Set Operators)|- (complement_semantics): For A,B: @T, A ~ B = {x:T || x in A and not x in B }.
. Unary Complement Operator
Expression like this
~Cat
are best thought of as abbreviations when the type of the set is known. If for example
Cat is a subset of a type called Animal then
~Cat = Animal ~ Cat.
However, the null set symbol `{}` has no defined type and so it's complement is undefined.
Here is an attempt to catch this
For Type T, A:@T, ~A::= T~A.
. Equality of sets
|-(eqsets):for A,B:@T, if for all x:T(x in A iff x in B) then A=B.
An object is a set when and only when membership solely determines
equality. "Bags" have the same abstract operators as "Sets" but two bags
are equal only when their members occur the same number of times in both
Bags. Formally a "Bag of X's" is an object of type Nat^X. The most general
form of this model will be found under
.See http://www/dick/maths/math_41_Two_Operators.html#semiring
For A,B:@T, A<>B iff not(A=B).
. Conveniences
For x,y:T1, x is y::=(x = y),
For x:T1,X:@T1, x is_a X::=(x in X).
For Type T, A:@T, ~A ::= T~A.
Note, if the type of the elements of a set A is undefined then the complement
of A is also undefined.
. Cardinality
`How many elements are in this set?`
For X:@T, n:Nat0, |X| = n iff for n x:T (x:X).
For Type T, Card[T]::@T->Nat0= map[X:@T](|X|).
For Type T, X:@T, Card(X) ::Nat0= Card[T](X).
For Type T, A:@T, n:Nat0, A@n = { X:@T || Card[T](X) = n }.
Note: avoid using /Card(n) or /|_|(n)
as it does not define the types of objects
being counted. Instead the expression `T@n` defines the type and the number of elements.
. Finite Sets
A finite set can be formally defined as a set that can not be put into a one-one
correspondence to a proper subset of itself. We can describe:
For Type T, Finite_sets(T)::@T=`the subsets S of T that are finite`.
.See ./types.html#Finite_sets
For Type T, S:@T. Finite_sets(S)::@T={F:@S. F in Finite_sets(T) }.
Notice that
|-(fin1):For Type T, A,B:@T, if A==>B in Finite_sets(T) then A in Finite_sets(T).
|-(fin2):For Type T, A,B:@T, if A in Finite_sets(T) then A&B in Finite_sets(T).
|-(fin3):For Type T, A,B:@T, if A,B in Finite_sets(T) then A|B in Finite_sets(T).
|-(fin4):For Type T, A,B:@T, if A in Finite_sets(T) then A~B in Finite_sets(T).
|-(cardinality_of_union): for Type T, \alpha, \beta:Finite_sets(T) ( Card(\alpha | \beta ) = | \alpha | + | \beta | - |\alpha & \beta| ).
We can define a property of sets:
For Type T, S:@T, finite(S)::bool= (S in Finite_sets(T)).
However me must avoid expressions that contain "/finite(P)".
. Quantifiers expressed using sets
For all X:@T, X=T iff for all x:T(x in X),
A set in a context that demands a proposition is true iff there exists at
least one member.
For X:@T, X::@= for some x:T(x in X),
For X:@T, for some x:T(x in X) = Card(X)>0.
For X:@T, if |X|=1 then the(A) ::= the(x:T||x in A).
There are short hand ways of stating properties of sets so that
they can be used easily:
some(X)::= (X<>{}).
no(X)::= (X={}).
all(X)::= (X=T).
A and B::= some (A & B).
Here is a readable distfix expression:
no A and B::= no (A & B).
. Set Operators
For T:Types, A,B:@T, A & B::= {x:T || x in A and x in B} ,
\cap::= "&".
& :: @@T -> @T,
|- For \beta:@@T, &\beta={x:T || for all B:\beta(x in B)}.
(above)|- A & B = &{A,B}.
For T:Types, A,B:@T,A | B::= {x:T || x in A or x in B},
\cup::= "|".
| :: @@T -> @T,
|- For \beta:@@T, |\beta={x:T || for some B:\beta (x in B)},
(above)|- A | B = |{A,B}.
For T:Types, A,B:@T,A ~ B::= {x:T || x in A and not x in B},
"but_not"::="~".
(above)|- (@T,|,{},&,T,~) in Boolean_algebra.
.Box
A&B = B&A.
A|B = B|A.
A&(B&C) = (A&B)&C.
A|(B|C) = (A|B)|C.
A | A = A.
A & A = A.
A~A={}.
...
Note. `~A` is a well defined set expression as long as A is a subset of a known type T.
Instead in MATHS if `A` is a subset of a Type `T` then `~A`= `T~A`.
A~B = A & (T~B).
~(A&B) = T~(A&B) = (T~A)|(T~B) = ~A | ~B.
...
.Close.Box
(Cartesian products): these look like set expressions but are
really part of the MATHS theory of types.
For T:Types, A,B:@T, A>B::= for all a in A(a in B),
\subseteq::= "==>".
.As_is \subseteq::="==>"
A<==B ::= B==>A.
all A are B::= (A==>B).
For T:Types, A,B:@T,A=>>B::= A ==>B and A<>B,
\subset::= "=>>".
.As_is \subset::="=>>"
A<<=B ::= B=>>A.
There are many useful theorems for subsets:
.Box
()|- (subseteq_reflexive): For all Types T, A:@T, A ==> A.
()|- (subset_irreflexive): For all Types T, A:@T, not (A =>> A).
()|-(subseteq_transitive): For all Types T, A,B,C:@T, if A ==> B ==> C then A ==> C.
()|-(subset_transitive): For all Types T, A,B,C:@T, if A =>> B =>> C then A =>> C.
()|-(subset_subseteq): For all Types T, A,B,C:@T, if A =>> B ==> C then A =>> C.
()|-(subseteq_subset): For all Types T, A,B,C:@T, if A ==> B =>> C then A =>> C.
Note: these are easier to write using the relational product:
(subseteq_transitive)|- (==>; ==>) = ==>.
(subset_transitive)|- (=>>; ==>>) = =>>.
(subset_subseteq)|- (=>>; ==>) = =>>.
(subseteq_subset)|- (==>; =>>) = =>>.
()|- (subset_complement): For all Types T, A,B:@T, if A ==> B then T~B ==> T~A.
()|-(intersection_is_subset): for all Types T, A,B:@T, A & B ==> B and A & B ==>A.
()|-(union_is_superset): for all Types T, A,B:@T, A ==> A | B and B ==> A | B.
()|-(subset_union_form): for all Types T, A,B:@T, A==>B iff A | B = B.
()|-(subset_intersection): for all Types T, A,B:@T, A==>B iff A = A&B.
We could use the above two eqivalences to reason algebraically about subsets.
They are both inspired by lattice theory.
Some of these theorems are also stated below... $TBA?
()|-(Product_of_subsets): for all Types T, A,B,C,D:@T, if A==>C and B==>D then A>** C>A, all B:\pi
( choice(B) in B).
Notice that this assumption is `obviously` true for finite cases.... it
is some the weirder infinite sets that make it doubtful.
The following formally asserts that the axiom of choice is part of the
$MATHS system:
|- (axiom_of_choice): $Choice.
This appears in other forms as part of the theory of relations and
functions,
.See http://www/dick/maths/logic_5_Maps.html#Choice
The axiom of choice was used long before Zermelo made it an
explicit axiom in 1904.
It appears as the
.Key axiom of selection
in `Principia Mathematica`. It was discussed for a long time but is
used by practicing mathematicians without qulams. For more history,
see
.See http://http://en.wikipedia.org/wiki/Axiom_of_Choice
in the Wikipedia.
Also see Skolem functions in
.See http://www/dick/maths/logic_5_Maps.html
.Close
.Open Proofs involving Sets
The following proof patterns are common:
.Table To prove Assume Derive Notes
.Row A==>B a:A b:B
.Row no(A) a:A $RAA
.Row A=B a:A a:B And also
.Row - b:B b:A
.Close.Table
There are a large number of provable facts about sets
()|-(glb): A<==A&B==>B.
()|-(lub): A==>B|A<==B.
There are also some easily proved derivation rules
()|-(seteq): A=B iff A==>B and B==>A.
()|-(converse): A==>B iff ~B==>~A.
()|-(barbara): If A==>B==>C then A==>C.
()|-(celarent): If no A are B and all C are B then no C is B.
()|-(darii): If all M is P and some S are M then some S are P.
()|-(ferio): If no M is P and some S are M then some S are ~P.
And so on thru most of the medieval catagorical syllogisms
.See http://ftp.csci.csusb.edu/dick/samples/syllogisms.html
.Close
. Epithets and term logic -- Use Sets instead
This is a the idea designed to handle natural expressions like
`flightless bird`. An `epithet` is a word or phrase written in front of
the name of a set (not an expression). It is always a subset of the named
set.
There is a risk of confusion when talking about sets of strings.
What would be very handy would be able to have positive and negative
epithets. The effect would be like including term logic into MATHS.
Use '&' and '~' to construct terms
penguin \subset aquatic & flightless & bird.
ostriche \subset bird & flightless ~ aquatic.
Representing complex families of sets -- ontologies or domains of
discourse -- in this form make many consequence transparent. For example
No penguin and ostriche,
one is aquatic and the other is not.
penguin | ostriche \subset flightless & bird \subset bird.
For more on this see
.See ./logic_8_Natural_Language.html
(Semantics)
and
.See ./notn_16_Classification.html
(Notation).
Caveats when
.Key translating natural language into sets.
First, these classifications in natural language
are often based on defining arbitrary boundaries. Sometimes you
need to attach attributes to the elements of a set to get a consistent and
realistic logic. The classic example would be the adjective `bearded` when
applied to the set of `men`. Here is the
.Key argument of the beard`.
Where do you draw the boundary between `bearded` and
`beardless`? What happens when you take a `bearded` person and start removing
hairs from the face... when do they become `beardless`. If we reverse the process and let
one hair grow at a time... when has the person become `bearded`.
Second, one needs to be careful of adjectives that define subsets relative to
the superset. For example: `large` and `small` are not absolutes. A 'small elephant`
is larger (I guess) than a `large dog`. So `large & dog` does not encode the
semantics of `large` correctly. It can not be a separate set. Instead it
should be defined as a map from a set into a subset:
large::@object->@object.
Possibly with this definition in terms of an attribute `size`:object->Real&Positive.
For S:@object, large(S) = {x:S. size(x) > 75 * mean(size o S)},
perhaps, or
large(S) = top_quartile[size](S),
(if you define top_quartile)...
By the way, as a final warning -- what about `bearded dog`? One must be
careful to defines sets as subsets and not translate the terms that
move the subsets outside of their sets -- except for humorous, poetic, or other
creative processes.
Perhaps a traditional Philosophy 101 course would be wise...
. Families of sets
.See http://www.csci.csusb.edu/dick/maths/logic_31_Families_of_Sets.html
. Principia Mathematica Chapter 42 -- Partly Baked Idea
This comes from rereading section 42 of Principia Mathematica and noticing
a couple of odd theorems about the union and intersection of sets
of sets of set.
I doubt if they will be useful.
They force the use of a nonstandard notation for the set extension
of a function, so I'm enclosing them in a Net.
Chapter_14::PBI=following
.Net
|- NONSTANDARD.
T::Types.
|- Set Operators
// :: infix( T^T, @T, @T).
For all f:T->T, A:@T, f//A = { f(x) || x:A }.
For A,B,C:@T.
(-1)|- | //{ {A,B}, {C} } = { |{A,B}, |{C} } = {A|B, C}.
(-1)|- | | //{ {A,B}, {C} } = | {A|B, C } = A | B | C.
(Set Operators)|- |{{A,B}, {C}} = {A,B,C }.
(Set Operators)|- ||{{A,B}, {C}} = |{A,B,C } = A | B | C.
(above)|- | | //{ {A,B}, {C} } = ||{{A,B}, {C}} .
Whiehead and Russell (PM *42) prove that
(above)|- (infinite_union_associative): For all \kappa: @@@T, | |// \kappa = | | \kappa.
(above)|- (infinite_intersection_associative):For all \kappa: @@@T, & &// \kappa = & | \kappa.
.Close.Net
. MinTerms
MINTERM::={
A:Sets, B:@A, p::=map[ a:A] (map b:B(a in b)).
For each a in A there is an array of true/false values, one for each set in
B, named p(a). We can partition A into cells of elements with the same
array of values:
P::=A/p
Thus, given for a1,a2:A, a1 =/p a2, for all b:B, a1 in b iff a2 in b.
}=::MINTERM.
.Open Tree by Knuth
.Source Knuth 69, Vol 1, Section 2.3 Trees p305
A typical tree is `T` where
.Box
T::=(nodes=>{1,1.1,1.2,1.2.3}, root=>1, m=>2, subtree=>(T1,T2)),
T1:=(nodes=>{1.1}, root=>1.1, m=>0, subtree=>()),
T2:=(nodes=>{1.2,1.2.3}, root=>1.2, m=>1, subtree=>(T3)),
T3:=(nodes=>{1.2.3}, root=>1.2.3, m=>0, subtree=>()).
.Close.Box
. Definition of a tree
TREE::=Net{
|-numbers.
nodes::Finite(Sets),
root::nodes,
fan_out::Nat0,
subtree::1..fan_out->@nodes, -- These are ordered trees
|-nodes~{root}>== {subtree(i) || i:1..m},
|-For all i:1..m, subtree(i) in $ $TREE.
}=::TREE.
|-For T:$ $TREE, i:Nat0, T[i]::=T.subtree[i].
??{convergence because lim |nodes|=0}??
forest::={F:@TREES||for T1,T2:F(no T1&T2)}
()|- if T:$ $TREE then T~{root} in forest.
.Close
.Close Sets
**