bunch set string list
unpackaged
packaged
unpackaged
packaged
unindexed
unindexed
indexed
indexed
1/25
Bunch Theory
Bunches can be used to represent collections.
1, 3, 7 ⊤, ⊥, 5, “a” 2
Any number, character, binary, or set is an elementary bunch, or element.
A , B A ‘ B ¢A A: B
union
intersection
size, cardinality (number) inclusion (binary)
2/25
1, 3, 7 = 3, 1, 7, 1
¢2 = 1
¢(1, 3, 7) = 3 =
2: 0, 2, 5, 9 2: 2
2, 9: 0, 2, 5, 9
¢(3, 1, 7, 1)
Bunch Theory
3/25
axioms
x: y = x: A,B
x=y
elementary axiom
compound axiom idempotence
symmetry associativity idempotence symmetry associativity
antidistributivity
distributivity generalization
specialization
=
x: A
∨
x: B
A,A = A
A,B = B,A
A,(B,C) = (A,B),C A‘A = A
A‘B = B‘A A‘(B‘C) = (A‘B)‘C
A,B: C = A: C ∧ B: C A: B‘C = A: B ∧ A: C
A: A,B A‘B: A
Bunch Theory
4/25
axioms
Bunch Theory
A: A reflexivity
A: B ∧ B: A = A=B antisymmetry
A:B ∧ B:C ⇒ A:C transitivity ¢x = 1 size ¢(A,B) + ¢(A‘B) = ¢A + ¢B size
¬ x: A ⇒ ¢(A‘x) = 0 size
A:B ⇒ ¢A≤¢B size
5/25
laws
A,(A‘B) = A A‘(A,B) = A
A: B ⇒ C,A: C,B A: B ⇒ C‘A: C‘B
A:B = A,B=B = A=A‘B A,(B,C) = (A,B),(A,C)
A,(B‘C) = (A,B)‘(A,C) A‘(B,C) = (A‘B), (A‘C) A‘(B‘C) = (A‘B)‘(A‘C)
A: B ∧ C: D ⇒ A,C: B,D A: B ∧ C: D ⇒ A‘C: B‘D
absorption absorption monotonicity monotonicity
inclusion distributivity
distributivity distributivity distributivity conflation conflation
Bunch Theory
6/25
null
bin = nat = int = rat = real = xnat = xint = xrat = xreal = char =
⊤,⊥
0, 1, 2, …
…, –2, –1, 0, 1, 2, …
…, –1, 0, 2/3, …
…, 21/2, …
0, 1, 2, …, ∞
–∞, …, –2, –1, 0, 1, 2, …, ∞ –∞, …, –1, 0, 2/3, …, ∞
–∞, …, ∞
…, “a”, “A”, …
the empty bunch
the binary values the natural numbers the integer numbers the rational numbers the real numbers
the extended natural numbers the extended integer numbers the extended rational numbers the extended real numbers
the character values
Bunch Theory
7/25
i: x,..y = ¢(x,..y) =
0,..3 = 0,..2 = 0,..1 = 0,..0 =
0,..∞ =
x≤i