- Enumeration Types
- : Why
- : What
- : Exercise 1
- : Example
- : Notation
- : Example 2
- : Exercise 2
- : Cyclic Enumerations
- : Example 3
- : See Also
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS
- Glossary

- 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".
- (above)|- (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),
- (above)|- (e3): For all s,s', s<=s' or s'<=s.
- (above)|- (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 ).
- (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- weekday:$ ENUMERATION where following,
- 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.

(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): - Set::Sets,
- 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 [click here if you can fill this hole]
- 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

- |-ENUMERATION(Set=img(v), succ=map[a:Set~v(length(v))](v(/v(a)+1)) ).
- Answer::=enum(no, yes).
- Answer.no:Answer,
- Answer.yes:Answer,
- Answer.no=Answer.first,
- Answer.yes=Answer.last,
- ...

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|.
- (above)|-for all s, s = s.succ^cycle.
- (above)|-succ^cycle=Id.
- (above)|-for all c, if succ^c = Id then for some n:0..*( c = n*cycle ).
- initialed::@.
- if initialed then initial::Set.

(End of Net CYCLIC_ENUMERATION)

## Example 3

Net- week = cycle(mon,tue,wed,thur,fri,sat,sun).
- week.set={mon,tue,wed,thur,fri,sat,sun},
- week.succ= mon+>tue|tue+>wed|...|sat+>sun|sun+>mon.
- week.cycle = 7.
- ...

(End of Net Example 3)

## See Also

- |-UNARY_ALGEBRA(Set, f=>succ, finite=true).
- PARTIAL_UNARY_ALGEBRA::= See http://www.csci.csusb.edu/dick/maths/math_15_Unary_Algebra.html#PARTIAL_UNARY_ALGEBRA
- UNARY_ALGEBRA::= See http://www.csci.csusb.edu/dick/maths/math_15_Unary_Algebra.html#UNARY_ALGEBRA
- Linearly_ordered_sets::= See http://www.csci.csusb.edu/dick/maths/math_21_Order.html#Linearly_ordered_sets
- Complete::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html#Complete.
- STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
# Glossary

- 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).
- given::reason="I've been told that...", used to describe a problem.
- given::variable="I'll be given a value or object like this...", used to describe a problem.
- goal::theorem="The result I'm trying to prove right now".
- goal::variable="The value or object I'm trying to find or construct".
- 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.
- hyp::reason="I assumed this in my last Let/Case/Po/...".
- QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
- QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
- RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last
assumption (let) that you introduced.

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++.

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:

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

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 ]

For a more rigorous description of the standard notations see