[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / math_77_Enumerations
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Sun Oct 2 14:39:41 PDT 2011

Contents


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

      (End of Net ENUMERATION)

      Exercise 1

      Sketch out proofs of the theorems in ENUMERATION above. [click here [socket symbol] 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 [socket symbol] 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

    Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

    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 might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

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

    Notes on the Underlying Logic of MATHS

    The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

    For a more rigorous description of the standard notations see

  1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

    Glossary

  2. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
  3. given::reason="I've been told that...", used to describe a problem.
  4. given::variable="I'll be given a value or object like this...", used to describe a problem.
  5. goal::theorem="The result I'm trying to prove right now".
  6. goal::variable="The value or object I'm trying to find or construct".
  7. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  8. hyp::reason="I assumed this in my last Let/Case/Po/...".
  9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

End