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:

 		enum(bad, indifferent, good)

 		enum(green, amber, red)

 		enum(off, on)

 		enum(Yes, No)

Thes are best used by giving them names and using the name as a type in later definitions:

 		weekday::=enum(mon,tue,wed,thur,fri,sat,sun).

 		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:
1. ENUMERATION::=following,
   Net
   1. Set::Finite(Sets),
   2. succ::gloss="Successor",
   3. succ::Set<->Set, partial one-to-one mapping/funtion/operator.
   4. pred::= /succ.
   5. pred::gloss="predescessor".
      
   6. (above)|- (e1): PARTIAL_UNARY_ALGEBRA(Set, op=>succ, finite=>true, terminal).
   7. <=::@(Set,Set),
      
   8. |-For s,s':Set, s<=s' = for some n:0..*(s' = s.succ^n)
      
   9. |- (e2): (<=) in Complete(Set),
      
   10. (above)|- (e3): For all s,s', s<=s' or s'<=s.
       
   11. (above)|- (e4): linear_order(Set).
   12. first::=min(Set).
   13. last::=max(Set).
       
   14. (Set, last)|- (e5): last in terminal.
       
   15. (succ, e5)|- (e6): terminal = {last}.
       
   16. (e3)|- (e7): for all s:Set, some n:0..* ( s = first.pred^n ).
       
   17. (e7, succ)|- (e8): for all s:Set, one n:0..* ( s = first.succ^n ).
   18. ord::=gloss="order".
   19. For s:Set, ord(s)::=the n:0..* ( s = first.succ^n ).
       
   20. (above)|- (e9): ord(last) = |Set| - 1.

   
   (End of Net ENUMERATION)
   
   

   Exercise 1

   Sketch out proofs of the theorems in ENUMERATION above. [click here if you can fill this hole]

   Example

   
   Net
   1. weekday:$ ENUMERATION where following,

      ---

      1. weekday.Set={mon,tue,wed,thur,fri,sat,sun},
      2. mon:weekday.Set,
      3. tue:weekday.Set,
      4. ...
      5. sun:weekday.Set,
      6. weekday.succ= mon+>tue|tue+>wed|wed+>thu|thu+>fri|fri+>sat|sat+>sun,
      7. weekday.first=mon,
      8. weekday.last=sun,
      9. weekday.ord= /(mon,tue,wed,thur,fri,sat,sun) -1.
      10. = mon+>0 | tue+>1 | wed+>2 |thu+>3 | fri+>4 | sat+>5 | sun+>6.

      ---

   
   (End of Net Example)
   
   

   Notation

   When we have a list of unique identifiers v then we can create a new type T=enum v.
   (enum):
2. For n:Nat, v:1..n-->identifier, T:identifier, (T=enum v) ::=following,
   Net
   
   
   1. |-ENUMERATION(Set=img(v), succ=map[a:Set~v(length(v))](v(/v(a)+1)) ).
      
   2. |-T=Set.
   3. v(1) : T.
   4. v(2) : T.
   5. ... -- informal here [click here if you can fill this hole]
   6. v(length(v)) : T.

   
   (End of 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

3. Answer::=enum(no, yes).

   ---

   1. Answer.no:Answer,
   2. Answer.yes:Answer,
   3. Answer.no=Answer.first,
   4. Answer.yes=Answer.last,
   5. ...

   ---

   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.

4. CYCLIC_ENUMERATION::=following,
   Net
   
   
   1. |-UNARY_ALGEBRA(Set, f=>succ, finite=true).
      
   2. |-succ in Set --- Set.
   3. pred::= /succ.
      
   4. |-For s,s':Set, some n:0..*, s' = s.succ^n.
   5. cycle::= |Set|.
      
   6. (above)|-for all s, s = s.succ^cycle.
      
   7. (above)|-succ^cycle=Id.
      
   8. (above)|-for all c, if succ^c = Id then for some n:0..*( c = n*cycle ).
   9. initialed::@.
   10. if initialed then initial::Set.

   
   (End of Net CYCLIC_ENUMERATION)
   
   

   Example 3

   
   Net
   1. week = cycle(mon,tue,wed,thur,fri,sat,sun).

      ---

      1. week.set={mon,tue,wed,thur,fri,sat,sun},
      2. week.succ= mon+>tue|tue+>wed|...|sat+>sun|sun+>mon.
      3. week.cycle = 7.
      4. ...

      ---

   
   (End of Net Example 3)
   
   

   See Also

5. PARTIAL_UNARY_ALGEBRA::= See http://www.csci.csusb.edu/dick/maths/math_15_Unary_Algebra.html#PARTIAL_UNARY_ALGEBRA
6. UNARY_ALGEBRA::= See http://www.csci.csusb.edu/dick/maths/math_15_Unary_Algebra.html#UNARY_ALGEBRA
7. Linearly_ordered_sets::= See http://www.csci.csusb.edu/dick/maths/math_21_Order.html#Linearly_ordered_sets

8. Complete::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html#Complete.

. . . . . . . . . ( end of section Enumeration Types) <<Contents | End>>

Notes on MATHS Notation

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle = Net{radius:Positive Real, center:Point}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

Notes on the Underlying Logic of MATHS

For a more rigorous description of the standard notations see