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

# 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 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

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)

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.