.Open Enumeration Types
. Why
Enumerations where introduced into Pascal. They are
really to trivial to have a formal mathematical theory and
so were not "discovered" until this time.
They proved to be very useful for making programs
more readable, less error prone, and easier to maintain,
as a result they appeared in C, Ada, and C++.
. What
An enumeration type has a finite set of values in a fixed
sequence:
.As_is enum(bad, indifferent, good)
.As_is enum(green, amber, red)
.As_is enum(off, on)
.As_is enum(Yes, No)
Thes are best used by giving them names and using the name as a type in
later definitions:
.As_is weekday::=enum(mon,tue,wed,thur,fri,sat,sun).
.As_is month::=enum(jan,feb,mar,apr,may,jun,jul,aug,sep,oct,nov,dec).
The term "enum" is borrowed from C++. In what follows the terms "pred",
"succ" and "ord" come from Pascal and Ada:
ENUMERATION::=following,
.Net
Set::Sets,
|- finite Set.
succ::gloss="Successor",
succ::Set<->Set, partial one-to-one mapping/funtion/operator.
pred::= /succ.
pred::gloss="predescessor".
()|-(e1): $PARTIAL_UNARY_ALGEBRA(Set, op=>succ, finite=>true, terminal).
<=::@(Set,Set),
|- For s,s':Set, s<=s' = for some n:0..*(s' = s.succ^n)
|- (e2):(<=) in $Complete(Set),
()|- (e3):For all s,s', s<=s' or s'<=s.
()|- (e4):$linear_order(Set).
first::=min(Set).
last::=max(Set).
(Set,last)|- (e5):last in terminal.
(succ,e5)|- (e6):terminal = {last}.
(e3)|- (e7):for all s:Set, some n:0..* ( s = first.pred^n ).
(e7,succ)|- (e8):for all s:Set, one n:0..* ( s = first.succ^n ).
ord::=gloss="order".
For s:Set, ord(s) ::=the n:0..* ( s = first.succ^n ).
()|- (e9):ord(last) = |Set| - 1.
.Close.Net ENUMERATION
. Exercise 1
Sketch out proofs of the theorems in $ENUMERATION above.
.Hole
. Example
.Net
weekday:$ $ENUMERATION where following,
.Box
weekday.Set={mon,tue,wed,thur,fri,sat,sun},
mon:weekday.Set,
tue:weekday.Set,
...
sun:weekday.Set,
weekday.succ= mon+>tue|tue+>wed|wed+>thu|thu+>fri|fri+>sat|sat+>sun,
weekday.first=mon,
weekday.last=sun,
weekday.ord= /(mon,tue,wed,thur,fri,sat,sun) -1.
= mon+>0 | tue+>1 | wed+>2 |thu+>3 | fri+>4 | sat+>5 | sun+>6.
.Close.Box
.Close.Net Example
. Notation
When we have a list of unique identifiers v then we can create
a new type T=enum v.
(enum):
For n:Nat, v:1..n-->identifier, T:identifier, (T=enum v) ::=following,
.Net
|- $ENUMERATION(Set=img(v), succ=map[a:Set~v(length(v))](v(/v(a)+1)) ).
|- T=Set.
v(1) : T.
v(2) : T.
... -- informal here
.Hole
v(length(v)) : T.
.Close.Net
Notice that this allows you to refer to an identifier i in v as T.v
but not generate a new type by substituting a new identifier for T.
Using 'i' without T may also be ambiguous. However, we can write
definitions because they imply a declaration and a equality:
. Example 2
Answer::=enum(no, yes).
.Box
Answer.no:Answer,
Answer.yes:Answer,
Answer.no=Answer.first,
Answer.yes=Answer.last,
...
.Close.Box
However, `Bad=enum(no,no)` and `Bad2=enum(12, 42)` are not correct
and do not define Bad and Bad2. Notice also that if `Answer(yes=>no)` was
allowed then this would generate `Bad`.
. Exercise 2
Prove that there is no complete UNARY_ALGEBRA that is finite
and is a linearly order set.
. Cyclic Enumerations
These would be useful if only they were implemented.
The key difference is that the values form a ring
rather than a line. Each value has a successor. Repeated
successors lead back to the initial one again. All elements
have a unique predesessor.
CYCLIC_ENUMERATION::=following,
.Net
|- $UNARY_ALGEBRA(Set, f=>succ, finite=true).
|- succ in Set --- Set.
pred ::= /succ.
|- For s,s':Set, some n:0..*, s' = s.succ^n.
cycle ::= |Set|.
()|- for all s, s = s.succ^cycle.
()|- succ^cycle=Id.
()|- for all c, if succ^c = Id then for some n:0..*( c = n*cycle ).
initialed::@.
if initialed then initial::Set.
.Close.Net CYCLIC_ENUMERATION
. Example 3
.Net
week = cycle(mon,tue,wed,thur,fri,sat,sun).
.Box
week.set={mon,tue,wed,thur,fri,sat,sun},
week.succ= mon+>tue|tue+>wed|...|sat+>sun|sun+>mon.
week.cycle = 7.
...
.Close.Box
.Close.Net Example 3
. See Also
PARTIAL_UNARY_ALGEBRA::=http://www.csci.csusb.edu/dick/maths/math_15_Unary_Algebra.html#PARTIAL_UNARY_ALGEBRA
UNARY_ALGEBRA::=http://www.csci.csusb.edu/dick/maths/math_15_Unary_Algebra.html#UNARY_ALGEBRA
Linearly_ordered_sets::=http://www.csci.csusb.edu/dick/maths/math_21_Order.html#Linearly_ordered_sets
Complete::=http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html#Complete.
.Close Enumeration Types