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
.
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
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) -> Sis 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).