# Ordinals and Programs

One can model specifications of "batch" programs by a set `S` of `states' and a function `f : S -> Fam(Fam(S))` from states to families of families of states. By a batch program I mean what might variously be called a transformational program (in the terminology of Harel and Pnueli), and input output program, or a transaction. The essential thing is that the execution of the program is externally visible only to the extent that either it hasn't begun, or it has terminated. There are only `before' states and `after' states, and the latter supplants the former instantaneously, "in a trice".

I asserted that such a structure can serve as a model. To see this, ask yourself what we really want to know about something that meets the specification of a batch program. What can we use such a thing for? All we can do is run it to produce a new state, and presumably our purpose in running the program can be expressed by a predicate that expresses our goal, holding of states that we like. We need to know what predicate to establish in the `before' state so as to guarantee a given goal predicate. In other words, we need to know a predicate transformer `F`. The predicate transformer should be monotone. The more we know about the start state (the stronger the argument predicate `P`), the more we know about the `after' state (the stronger `F(P)`. Each function `f = { n(s,i,j) | j : J(s,i) | i : I(s) }` provides a representation of a monotone predicate transformer in sum-of-products form

```
F(P) = { s : S | exists i : I(s) . all j : J(s,i) . P(n(s,i,j)) }  .
```
Of course, there can be many representations of the same predicate transformer, with different `I, J`, and `n`.

# Ordinals

What are ordinals for? They are for indexing iterations of a function, and the levels of hierarchies of well-founded objects.

There are two key properties of the von-Neumann ordinals: transitivity, and well-foundedness.

By wellfounded I mean a suitable argument for definitions by recursion on the membership relation. One could also say, obedient to the foundation axiom of ZF set-theory, which is classically equivalent to the schema of induction on the membership structure. More precisely, a well-founded set is one in the intersection of all progressive classes, where a progressive class is one which holds of a set provided that it holds of all elements of that set.

Note the following equivalences:

```
UNION(c) subset c
=                              {definition subset}
a in UNION(c)     => a in c
=                              {definition UNION}
a in b /\ b in c  => a in c  --<<<<<<<<<<<<<<<< Start here
=                              {swap conjuncts}
b in c /\ a in b  => a in c
=                              {definition subset}
b in c => b subset c
=                              {definition SUBSET (powerset)}
b in c => b in SUBSET(c)
=                              {definition subset}
c subset SUBSET(c)
```
It follows that the relation `in` is transitive on `a` provided `UNION(c) subset c` or equivalently `c subset SUBSET(c)` holds for any element `c` of the set. By transitivity (I am not sure that this is quite the standard notion) of a set `a` I mean that the membership relation on the von-Neumann successor of `a`, ie. `a cup {a}` is transitive. Seo we have `UNION(a) subset a`, as well as `UNION(_) subset _` throughout `a`

# A construction

It seems to me that one might give an inductive definition of the finite ordinals (with an eye to revision and generalisation) somewhat along the following lines:

```Omega : Set,
Seg : Omega -> Set,
pd : (a : Omega)-> Seg a -> Omega  -- can be defined separately

Omega = { 0
| a+        WHERE a : Omega
| sup(a,f)  WHERE a : Omega
f : Seg a -> Omega
}
Seg a = CASE a OF
0         |->  {}
b+        |->  1 + Seg(b)
sup(b,f)  |->  Sigma t : Seg(b). Seg(f(t))
pd(a) = CASE a OF
0         |->  ex falso quolibet
b+        |->  \t-> CASE t OF INL(_) |-> b
INR(t) |-> pd(b,t)
sup(b,f)  |->  \(t,t')-> pd(f(t),t')
```
A slight variant, which gets rid of the successor case: instead of the constructor
`sup`
, use a constructor whose interpretation is the least strict upper bound.

But what do we do about transitivity? It seems that we have to consider something else at suprema, perhaps an ordered sum, and/or use a transitive closure construction somewhere.

The transitive closure `phi+` of a transition structure `phi : S -> Fam(S)`

```    S : Set
T : S -> Set
n : (s : S) -> T(s) -> S
```
is the `least' (in some sense) solution for ```psi : S -> Fam(S)``` of (either or both) of the following equations
```      psi = phi ; (SKIP union psi)
psi = phi union (phi ; psi)
```
where `SKIP` is the identity transition system and union and sequential composition of transition structures is defined in the obvious way.

Perhaps we can put a transition structure on `Seg(a)` above, and try for an ordered sum (which preserves transitivity).

Peter Hancock