{-
Time-stamp: "1997-11-09 22:47:13 peter"
This is a script for the type-checker CHalf. Here is a hastily written explanation of CHalf's syntax in html .
The script explores various things to do with binary relations on a given set.
One plan is to make use of some of this material in a file that deals with lenses; also to make some corresponding explorations around `interactive transition systems', basically a very rich data structure invented by Kent Peterson and Dan Synek.
\tableofcontents
\section{Motivation}
One strand in the notion of set is `set \emph{of} (something: reals, integers, elephants, ..)', and makes sense even if a `set of', or subcollection is something essentially different (in type) from a `set', or collection. However we can interpret the powerset operator \newcommand{\defocc}[1]{\mbox{\textit #1}} \newcommand{\power}[1]{\cal{P}(A)} $\power{}$ in a strong way and a weak way.
\begin{itemize}
\item In the strong interpretation, $\power{A}$ is the type of predicates over $A$, or (by the Curry-Howard isomorphism) set-valued functions with domain $A$. (One might also say `sets depending on an element of $A$'.)
A \defocc{predicate} is a (unary) propositional function defined on the underlying set $A$ - i.e. a function that maps an element of $A$ to a `truth-value', i.e. a proposition. To say the predicate holds somewhere is to say that there is an element of the corresponding set.
\item In the weak interpretation, $\power{A}$ is the type of families of $A$'s, i.e. functions into $A$ defined on some \defocc{index} set. A family is specified parametrically, with an expression containing a \defocc{parameter} which varies over the index set: that is, parametrically. (C.f. giving a parabola in parametric form $(x = a t^2, y = 2 a t )$).
\end{itemize}
Along with the weak and the strong forms of $\power{}$, there is a weak and a strong form of binary relation. The strong form is the familiar one, and but in the weak form a relation is a function which assigns to an element the family of elements that are related to it.
One reason to be interested by the weak form of $\power{}$, is that t he argument occurs \emph{negatively} in the definition of \texttt{Pow(A)}, (the type of predicates on a set \texttt{A}), and \emph{positively} in the definition of \texttt{Fam(A)} (the type of families of elements of \texttt{A}. So one can think about the fixed points of \texttt{Fam}, and versions of it that are relativised to a family of sets acting as a universe. This seems to lead towards the so-called `W' types, and Peter Aczel's constructive models of the cumulative hierarchy of sets.
One reason to be interested in the weak form of relation is that it allows you to talk, to some extent, about relations on a set without mentioning `the' genuine equality relation on the underlying set. Equality seems a troublesome notion in constructive mathematics, and the further you can get along without it, the better. Another reason is that many interesting notions like composition, or simulation seem related to how the two notions `mix'.
\subsection{themes}
Certainly these definitions are not well-structured, in part because of my clumsiness with the `theory' construct in half. There is some experimentation with theory structure, meaning that sometimes the same material is repeated in different arrangements. There are also sometimes different formulations of essentially the same definition.
There are definitions pertaining to transitive closure of genuine relations and reflexive and transitive closure for transition systems. (There seem to be 3 natural ways to define the transitive closure, one with problems.)
There are definitions pertaining to how transition systems and general relations `mix'. (Their composition. Predicate transformers of various kinds. Simulation.)
Then well foundedness, in the sense of the accessible (normalising, or terminating) states of a transition system.
Then some definitions connected with addition, multiplication and exponention of transition systems, essentially mimicing the classical definitions (by Cantor, I believe).
I should like to prove that exponentiation preserves well-foundedness by the method of lenses, but certain problems arise.
-}
{-
Make the checker load certain scripts in other files.
\begin{verbatim} #include "./standard.half" #include "./Boole.half" #include "./world.half" \end{verbatim}
-}
RTSSept97 = {- Some junk name for the whole file -}
theory
{
Pow2Fam {- family of a pow -}
( A : Set, P : Pow A )
= struct { I = Sigma A P, g = \i->i.p}
: Fam A
,
Rel( A : Set ) {- Genuine relations -}
= ( a : A )-> Pow A
: Type
{-
In the framework of classical set theory, there isn't any real difference between $\power{A \times A}$, and the set of functions from the set $A$ into $\power{A}$. The same seems to be true constructively, interpreting `subset of' as `propositional function on'.
-}
{- definitions and constructions for genuine relations -}
,
Rel_Properties( A : Set, R : Rel A )
= theory
{ Reflexive = ( a : A )-> R a a : Set
, Symmetric = ( a : A, a' : A, hyp : R a a' )-> R a' a : Set
, Transitive
= ( a1 : A, a2 : A, a3 : A )->
( hyp1 : R a1 a2, hyp2 : R a2 a3 )->
R a1 a3
: Set
, LE = \ S ->
( a : A, a' : A )->
( hyp : R a a' )->
S a a'
: Pow (Rel A)
, Converse = \ a1 a2 -> R a2 a1
: Rel A
, Domain = \a -> Sigma A (R a)
: Pow A
, Compose = \S a1 a3 ->
Sigma A (\ a2 -> and (R a1 a2) (S a2 a3))
: OP (Rel A)
, SC = {- symmetric closure -}
\ a a' ->
data
{ $0 ( x : R a a' )
, $1 ( x : R a' a )
}
: Rel A
{- three reasonable definitions of transitive closure -}
{- there is \emph{no way} to define general reflexive closure -}
, TC1 = \a a' ->
data { $sing ( x : R a a' )
, $ext_start
( a1 : A
, x : R a a1
, xs : TC1 a1 a'
)
}
: Rel A
, TC2 = \a a' ->
data { $sing ( x : R a a' )
, $ext_end
( a1 : A
, xs : TC2 a a1
, x : R a1 a'
)
}
: Rel A
, TC3 = \a a' ->
data { $sing ( x : R a a' )
, $compose
( a1 : A
, xsl : TC3 a a1
, xsr : TC3 a1 a'
)
}
: Rel A
, TC13 = {- The first is included in the third -}
\ a a' x ->
case x of
{ $sing x1 -> $sing x1
, $ext_start a1 x1 xs
-> $compose a1 ($sing x1) (TC13 a1 a' xs)
}
: ( a : A, a' : A, x : TC1 a a' )-> TC3 a a'
, TC23 = {- The second is included in the third -}
\ a a' x ->
case x of
{ $sing x1 -> $sing x1
, $ext_end a1 xs x
-> $compose a1 (TC23 a a1 xs) ($sing x)
}
: ( a : A, a' : A, x : TC2 a a' )-> TC3 a a'
, TC31 = {- The third is included in the first -}
let
{ conc ( a1 : A, a2 : A, a3 : A
, x : TC1 a1 a2 , y : TC1 a2 a3 )
= case x of {
$sing x1 -> $ext_start a2 x1 y,
$ext_start a4 x1 xs
-> $ext_start a4 x1 (conc a4 a2 a3 xs y)}
: TC1 a1 a3
}
in
\ a a' tc3 ->
case tc3 of
{ $sing x -> $sing x
, $compose a1 xsl xsr ->
conc a a1 a' (TC31 a a1 xsl)
(TC31 a1 a' xsr)
}
: ( a : A, a' : A, tc3 : TC3 a a' )-> TC1 a a'
, TC32 = {- The third is included in the second -}
let
{ conc ( a1 : A, a2 : A, a3 : A
, x : TC2 a1 a2 , y : TC2 a2 a3 )
= case y of {
$sing y1 -> $ext_end a2 x y1,
$ext_end a4 ys y1
-> $ext_end a4 (conc a1 a2 a4 x ys) y1}
: TC2 a1 a3
}
in
\ a a' tc3 ->
case tc3 of
{ $sing x -> $sing x
, $compose a1 xsl xsr ->
conc a a1 a' (TC32 a a1 xsl)
(TC32 a1 a' xsr)
}
: ( a : A, a' : A, tc3 : TC3 a a' )-> TC2 a a'
}
: Theory
{-
\section{Transition Systems}
Explanation needed here.
Hypo-relations? Semi-relations?
If one interprets \power{} as `set of subsets of', and `subset of' as `indexed family of', then it is far from clear that $\power{A \times A}$ is much like the set of functions from the set $A$ into $\power{A}$.
-}
,
TS ( A : Set ) {- Transition system, relative to a set -}
= ( a : A )-> Fam A
: Type
{-
I call an elements of the underlying set $A$ a \defocc{state}.
The value of the function for a given state $a$ is the set of
states \defocc{after} $a$, this set of states being given in the form
of an indexed family.
-}
,
{- Get a transition system from a genuine relation -}
Rel2TS( A : Set, R : Rel A )
= \ a -> Pow2Fam A (R a)
: TS A
,
{-
Get an operator on genuine relations from a transition system.
This is really composition of \emph{first} a transition relation,
\empty{then} a genuine relation. The other way round seems
problematic.
-}
Rel_TS( A : Set, t : TS A )
= let { B ( a : A ) = (t a).I : Set
, c ( a : A, b : B a ) = (t a).g b : A
} in
\ R a1 a2 ->
Sigma (B a1) (\b->R (c a1 b) a2)
: OP (Rel A)
,
TS_Properties ( A : Set, F : TS A )
= theory
{ B
= \ a -> (F a).I
: Pow A {- As a predicate, `is related to something' -}
, c ( a : A, b : B a )
= (F a).g b
: A {- what it's related to -}
{- We cannot really state transitivity or reflexivity. -}
{- For that we would need a genuine relation. -}
{- However, for certain constructions, the properties hold -}
{- at the level of definitional equality. -}
{- Another way to say a relation is transitive is to say that -}
{- it is isomorphic to its transitive closure. -}
{- Or if you want a relation to be transitive, use any relation -}
{- and work with its closure. -}
, Transitive
= ( a : A )->
( b : B a , b' : B (c a b) )->
B a
: Set
, Reflexive
= ( a : A )-> B a
: Set
{- two predicate transformers -}
, wlp
= {- The PT: X goes to `can lead to X' : wlp. -}
\ X a -> Sigma (B a) ( \ b -> X (c a b) )
: OP (Pow A)
, wlp_dual {- X goes to `must lead to X, if anywhere' -}
= \ X a -> Pi (B a) ( \ b -> X (c a b) )
: OP (Pow A)
, wp
= {- The PT: X goes to `can and must lead to X'. -}
\ X a -> and (Sigma (B a) ( \ b -> X (c a b) ))
(Pi (B a) ( \ b -> X (c a b) ))
{- This is kinda a $\Delta$-mumble-mumble shape... -}
: OP (Pow A)
{- This definition maps a TS to a relation transformer. -}
, RelT_TS
= \ R a1 a2 -> Sigma (B a1) ( \ b -> R (c a1 b) a2 )
: OP (Rel A)
{- how to deal with definitional equality? -}
, Leibnitz ( f : Fam (Pow A) ) {- Leibnitz wrt family -}
= \ a a' ->
( x : f.I )->
( h : f.g x a ) -> f.g x a'
: Rel A {- If we had used `real' X, have to be REL -}
}
: Theory
{- Package together the transition structure with the underlying set -}
, TS_s = sig { Base : Set, t : TS Base } : Type
{- Some examples of transition systems -}
,
TS_s0 = struct { Base = empty.set , t = \a->case a of {} } : TS_s
,
TS_s1 = struct
{ Base = data { $0 }
, t = \ z ->
struct { I = empty.set
, g = \i->case i of {} }
}
: TS_s
,
TS_s2 = struct
{ Base = data { $0, $1 }
, t = \z -> case z of
{ $0 -> struct { I = empty.set, g = \ i -> case i of {} }
, $1 -> struct { I = data { $0 }, g = \ i -> $0 }
}
}
: TS_s
,
{- An operation on transition systems that changes the base set. -}
{- (There are other examples below in `arithmetic') -}
{- Effectively, we throw out the first transition. -}
step1 ( s : TS_s )
= let { A = s.Base : Set
, B = \a ->(s.t a).I : Pow A
, c = \a ->(s.t a).g : ( a : A, b : B a )-> A
}
in struct { Base = Sigma A B
, t = \ ab ->
struct { I = B (c ab.p ab.q)
, g = \ i ->
struct { p = c ab.p ab.q
, q = i
}
}
}
: TS_s
,
TS_t
{-
The following is a theory about binary relations
presented in the `weak' fam form:
-}
( A : Set {- underlying set -}
, F : TS A )
= theory
{-
The relation $F$ can be put into another form,
that is much more convenient: it is
basically the same as a function which assigns a
set $B(a)$ to each state $a$ of the underlying set,
together with a function $c(a,b)$ of states $a$ and elements of $B(a)$,
which yields states. I shall call an element $b$ of some set $B(a)$
a \defocc{transition}, \defocc{to} $c$. I shall call the values
$\{ c(a,b) \; | \; b : B(a) \} $ \defocc{derivatives}, or
\defocc{(immediate) descendants } of $a$.
-}
{ B
= \ a -> (F a).I
: Pow A {- As a predicate of states, `is related to something' -}
, c ( a : A, b : B a )
= (F a).g b
: A
{- Transitive-reflexive closure, in 3 forms. -}
{- The first definition is perhaps the most straight-forward. -}
, TC1 {- chains from at a given element, growing at the head. Stalagmites? -}
= \ a ->
data
{ $nil {- possibly empty -}
, $cons ( b : B a, bs : TC1 (c a b) )
}
: Pow A
, end1 {- element a chain leads to -}
= \ a b ->
case b of
{ $nil -> a
, $cons b1 bs -> end1 (c a b1) bs }
: ( a : A, b : TC1 a )-> A
, TC1end1 {- chains from an element, growing at the tail. (Stalactites?) -}
= \ a ->
struct
{ I = TC1 a
, g = end1 a }
: TS A
, star = TC1end1 : TS A
, concat1 {- proof that TC1end1 is transitive. -}
( a : A, b : TC1 a, b' : TC1 (end1 a b ) )
= case b of
{ $nil -> b'
, $cons b1 bs -> $cons b1 (concat1 (c a b1) bs b')}
: TC1 a
{-
The next definition is simultaneously an inductive definition of a
set, and a definition by recursion on the construction of an element
of that set (of the `end' function).
-}
, j ( a : A )
= theory
{ TC2end2
= let
{ x = struct
{ I = data
{ $lin , $snoc ( bs : x.I, b : B (x.g bs) ) }
, g = \ i ->
case i of
{ $lin -> a
, $snoc bs b -> c (x.g bs) b
}
}
: Fam A
} in x
: Fam A
, Bs = TC2end2.I : Set
, cs = TC2end2.g : ( bs : Bs )-> A
}
: Theory
, TC2end2 = \ a -> (j a).TC2end2 : TS A
, TC2end2' {- another formulation -}
= \ a ->
let
{ x = struct
{ I = data
{ $lin
, $snoc ( bs : x.I, b : B (x.g bs) ) }
, g = \ i ->
case i of
{ $lin -> a
, $snoc bs b -> c (x.g bs) b }
}
: Fam A
} in x
: TS A
, TC2
= \ a -> (TC2end2 a).I
: Pow A
, end2
= \ a -> (TC2end2 a).g
: ( a : A , b : TC2 a )-> A
, concat2
( a : A , bs : TC2 a )
= let
{ f ( bs' : TC2 (end2 a bs) )
= case bs' of
{ $lin -> bs
, $snoc bs1 b -> $snoc (f bs1) {- problem -} [b]
}
: TC2 a
}
in
\ bs' ->
case bs' of
{ $lin -> bs
, $snoc bs'' b -> $snoc (concat2 a bs bs'') {- problem -} [b]
}
:
( bs' : TC2 (end2 a bs)
) -> TC2 a
{-
In this definition, which is simultaneously inductive
and recursive, chains grow by concatenation. (We really
have a set of binary trees. They are not unlike lisp
S-expressions, with atoms and nil.)
-}
, TC3end3
= let
{ I' ( a : A ) = (TC3end3 a).I : Set
, g' ( a : A ) = (TC3end3 a).g : ( i : I' a )-> A
} in \ a ->
struct
{ I = data
{ $nil
, $sing ( b : B a )
, $conc ( bs : I' a, bs' : I' (g' a bs) ) }
, g = \ i ->
case i of
{ $nil -> a
, $sing b -> c a b
, $conc bs bs' -> g' (g' a bs) bs' } }
: TS A
, TC3 = \ a -> (TC3end3 a).I : Pow A
, end3 = \ a bs -> (TC3end3 a).g bs : ( a : A, bs : TC3 a )-> A
, concat3
( a : A
, b : TC3 a
, b' : TC3 (end3 a b) )
= $conc b b'
: TC3 a
{-
Thinking of closure operations, another one of some
interest is the reflexive closure:
-}
, RCend
= \a->struct {
I = data
{ $nil
, $sing ( b : B a ) },
g = \ i ->
case i of
{ $nil -> a
, $sing b -> c a b } }
: TS A
{-
This raises the question of whether one can express
the symmetric closure. I do not have an answer it,
but I don't have a formulation either.
-}
, compose ( G : TS A ) {- compose two transition systems -}
= \a->
let { f = F a : Fam A
, B = f.I : Set
, c = f.g : ( b : B )-> A
} in
struct { I = Sigma B (\b->(G (c b)).I)
, g = \i->(G (c i.p)).g i.q
}
: TS A
{- Accessibility -}
, Acc
= \ a ->
data { $sup ( phi : ( b : B a )-> Acc ( c a b ) ) }
: Pow A
{-
Note that the following all create predicate transformers.
-}
, AccR {- Accessibility relative to a given predicate -}
= \ X a ->
data { $0 ( x : X a )
, $sup ( phi : ( b : B a )-> AccR X ( c a b ) ) }
: OP (Pow A)
, wlp {- weakest liberal precondition -}
{- ensuring all descendants have X -}
= \ X a -> Pi (B a)
(\b->X (c a b))
: OP (Pow A)
, dwp {- dual of wp. Better name? -}
= \ X a -> Sigma (B a)
(\b->X (c a b))
: OP (Pow A)
, wp {- weakest precondition - requires step enabled -}
= \ X a -> and (B a) {- equivalently, and (wlp X a) (dwp X a) -}
(wlp X a)
: OP (Pow A)
, wlp' {- AccR can be defined as a fixed point of wp'. -}
= \ X a -> maybe (wlp X a)
: OP (Pow A)
{-
Now a relation transformer. Composition `transition then genuine'. Can surely define with predicate transformer.
-}
, Rel_TS
= \ R a1 a2 -> Sigma (B a1) (\b->R (c a1 b) a2)
: OP (Rel A)
, Rel_TSD {- a dual. Something like a `diamond property'. -}
= \ R a1 a2 -> Pi (B a1) (\b->R (c a1 b) a2)
: OP (Rel A)
{-
A predicate of genuine relations: is a simulation.
Remember we do not require there to be a notion of equality between the states of a transition system. Without a notion of equality, we cannot actually \emph{say} that a pair of states is related - all we can do is run through the set of next states for a given state, parametrically.
It can happen that two states are `behaviourally' indistinguishable, meaning intuitively that any transition from one can be mimiced by a transition from the other, and vice versa. Of course it isn't obvious what mimicry means in connection with states, but for example a pair of states both of which have no derivatives is a pair of indistinguishable states -- they're both really `the dead state'. Furthermore, we don't care about the identity of transitions beyond that they come from here and they go to there, so these are really unlabelled transitions. (With labelled transitions, and an equality relation on transitions with the same origin, forming the reflexive and transitive closure looks exactly like forming the free category of paths in a labelled graph.)
We say that a genuine relation is a simulation, if when a pair of states is related, any derivative of the first is related to some derivative of the second. We simply don't care about whether the transition labels are `equal'.
Note that we manage to express this despite the fact that the idea seems to involve the composition `genuine followed by transition'. This is because it really involves `genuine followed by converse-transition'. In relational notation, it is $R \subseteq \rightarrow ; R ; \leftarrow$,
where the arrow stands for the transition relation, pointing `down'.
-}
, Simulation
= \ R ->
( a : A, a' : A )->
( hyp : R a a' )->
( b : B a )->
Sigma (B a') (\b' -> R (c a b) (c a' b'))
: Pow (Rel A )
{- reformulations -}
, Simulation1
= \ R ->
( a : A, a' : A )->
( hyp : R a a' )->
sig { f : ( b : B a )-> B a'
, s' : ( b : B a )-> R (c a b) (c a' (f b))
}
: Pow (Rel A )
, Simulation2
= \ R ->
( a : A, a' : A )->
( hyp : R a a' )->
Pi (B a) ( \ b ->
Sigma (B a') ( \ b' ->
R (c a b) (c a' b')))
: Pow (Rel A )
, SimulationOP {- pull a relation `back' -}
= \ R a a' ->
( hyp : R a a' )->
Pi (B a) ( \ b -> {- Anything you can do .. -}
Sigma (B a') ( \ b' -> {- .. I can do better. -}
R (c a b) (c a' b')))
: OP (Rel A )
, Simulation2' {- Can express as R LE (SimulationOP R) -}
= \ R ->
( a : A, a' : A )->
SimulationOP R a a'
: Pow (Rel A )
}
: Theory
{- proving that our definition of the `end' of a chain is correct -}
, th99 ( A : Set, F : TS A )
= theory
{ th = TS_t A F : Theory
, B = th.B : Pow A
, th' = TS_t A th.star : Theory
, Bstar = th.TC3 {- # th'.B -} : Pow A
, cstar = th.end3 {- # th'.c -} : ( a : A , arg : Bstar a )-> A
, unit ( a : A , b : B a )
= $sing b
: Bstar a
, DE ( a : A, a' : A ) {- Doesn't work if A is a type -}
= ( X : Pow A , hyp : X a )-> X a'
: Type
, refl ( a : A )
= $nil
: Bstar a
, c_refl ( a : A )
= \ X hyp -> hyp
: DE (cstar a (refl a)) a
, trans ( a : A, b : Bstar a, b' : Bstar (cstar a b) )
= th.concat3 a b b'
: Bstar a
, c_trans ( a : A, b : Bstar a, b' : Bstar (cstar a b) )
= \ X hyp -> hyp
: DE (cstar a (trans a b b'))
(cstar (cstar a b) b')
}
: Theory
{-
\section{ABc form -- `Triples'}
I used to call transition systems `triples'. I stopped because `triple' is already taken by the category theorists.
In any case, it is a particularly convenient, and intuitive form in which to have a transition system.
-}
, Triple
= sig { A : Set
, B : Pow A
, c : ( a : A, b : B a )-> A
}
: Type
{-
There is a general problem of mapping backwards and forwards between different representations of a transition system - as a triple, or as a set and a function on it into its (weak) powerset.
-}
, F2T ( F : TS_s )
= struct { A = F.Base
, B = \a ->(F.t a).I {- as a predicate, `has a predecessor' -}
, c = \a ->(F.t a).g
}
: Triple
, T2F ( F : Triple )
= struct { Base = F.A
, t = \a->struct { I = F.B a, g = F.c a }
}
: TS_s
{-
\section{Arithmetic of transition systems}
I want to define operations on transition systems corresponding to the three classic operations that produce well orderings with order-type $\alpha + \beta$, $\alpha . \beta$, $(1 + \alpha) ^ \beta$ from a pair well-orderings with order types $\alpha$ and $\beta$.
I use a theory so I can unpack the first argument just once.
-}
, arithmetic ( F : TS_s )
= theory
{ Ft = F2T F : Triple
, A = Ft.A : Set
, B = Ft.B : Pow A
, c = Ft.c : ( a : A, b : B a )-> A
{- Binary addition of two transition systems -}
{- There is another formulation below -}
, addition
= \G->
let { A' = G.Base : Set
, B' = (F2T G).B : Pow A'
, c' = (F2T G).c : ( a' : A', b' : B' a' )-> A'
}
in
T2F (struct
{ A = data { $first ( a : A ), $second ( a' : A' )}
, B = \a''->
case a'' of
{ $first a -> B a
, $second a'
-> data { $0 ( a : A )
, $1 ( b' : B' a' )
}
}
, c = \a'' b ->
case a'' of
{ $first a -> $first (c a b)
, $second a'
-> case b of
{ $0 a -> $first a
, $1 b' -> $second (c' a' b')
}
}
}
)
: OP TS_s
, addition' {- another formulation. Which way is better? -}
= \G->
let { A' = G.Base : Set
, B' = \ a' -> (G.t a').I : Pow A'
, c' = \ a' -> (G.t a').g : ( a' : A', b' : B' a' )-> A'
}
in
struct
{ Base = data { $first ( a : A ), $second ( a' : A' ) }
, t = \a''->
case a'' of
{ $first a -> struct
{ I = B a
, g = \ b -> $first (c a b)
}
, $second a' ->
struct
{ I = data
{ $0 ( a : A )
, $1 ( b' : B' a' )
}
, g = \ i ->
case i of
{ $0 a -> $first a
, $1 b' -> $second (c' a' b')
}
}
}
}
: OP TS_s
, {- In fact, we can define a `variadic' sum -}
{- indexed by a transition system -}
sum ( F : ( a : A )-> TS_s )
= struct
{ Base = Sigma A (\a->(F a).Base)
, t = \ab->
let
{ a = ab.p : A
, b = ab.q : (F a).Base
} {- ******************* -}
in struct
{ I = data
{
$0 ( pa : B a
, b : (F (c a pa)).Base
)
, $1 ( pb : ((F a).t b).I )
}
, g=\p ->
case p of
{ $0 pa b1 -> struct { p = c a pa, q = b1 }
, $1 pb -> struct { p = a, q = ((F a).t b).g pb }
}
}
}
: TS_s
{- binary multiplication of transition systemss -}
{- I suppose we should derive it from sum above. I doubt what follows is correct. -}
, multiplication
= \G->
let { A' = G.Base : Set
, B' = \ a' -> (G.t a').I : Pow A'
, c' = \ a' -> (G.t a').g : ( a' : A', b' : B' a' )-> A'
}
in
struct
{ Base = sig { first : A , second : A' }
, t = \z->
let { a = z.first : A, a' = z.second : A' }
in struct
{ I = data { $inner ( b : B a )
, $outer ( a : A, b' : B' a' )
}
, g = \ i ->
case i of
{ $inner b -> struct
{ first = c a b
, second=a'
}
, $outer a'' b'
-> struct
{ first = a''
, second = c' a' b'
}
}
}
}
: OP TS_s
, succ {- The successor of a transition system. -}
{- Note: preserves transitivity. -}
= let { A' = data {$top, $neath ( a : A ) } : Set
, B' ( a' : A' )
= case a' of { $top -> A
, $neath a -> B a
}
: Set
, c' ( a' : A', b' : B' a' )
= $neath ( case a' of { $top -> b'
, $neath a -> c a b'
}
)
: A'
}
in T2F ( struct { A=A', B=B', c=c' } )
: TS_s
,
{- base 2 exponentiation -}
{-
We want to mimic the structure of a proof that two `strings' are
related in the lexicographic order, as defined by the rules:
\begin{itemize}
\newcommand{\IF}{$\mbox{} \mathrel{\Longleftarrow} \makebox[1ex]{}$}
\item \texttt{nil} $\prec$ \texttt{cons h tl}
\item \texttt{cons h1 tl1} $\prec$ \texttt{cons h2 tl2}
\IF \texttt{h1} $<$ \texttt{h2}
\item \texttt{cons h tl1} $\prec$ \texttt{cons h tl2}
\IF \texttt{tl1} $\prec$ \texttt{tl2}
\end{itemize}
-}
two_to_the
= let { DC ( a : A )
= data { $nil, $cons ( b : B a, bs : DC (c a b)) }
: Set
, A2 {- Set of descending chains -}
= data { $empty, $nonempty ( a : A, d : DC a ) }
: Set
, B2 ( a2 : A2 )
= case a2 of
{ $empty -> data {}
, $nonempty a d ->
data { $0 {- to empty sequence -}
, $1 {- to sequence starting lower -}
( b : B a
, bs : DC (c a b)
)
}
}
: Set
, c2 ( a2 : A2, b2 : B2 a2 )
= case a2 of
{ $empty -> case b2 of {}
, $nonempty a d ->
case b2 of
{ $0 -> $empty
, $1 b bs -> $nonempty (c a b) bs
}
}
: A2
}
in T2F (struct { A = A2, B = B2, c = c2 } )
: TS_s
{- Styled on the definition above, we have product of a family -}
, product ( F : ( a : A )-> TS_s )
= let
{ Co ( a : A ) = (F a). Base : Set
, CoP ( a : A, c : Co a ) = ((F a).t c).I : Set
, Cop ( a : A, c : Co a, cp : CoP a c ) = ((F a).t c).g cp : Co a
, DC ( a : A )
= data { $nil
, $cons ( b : B a
, co : Co (c a b)
, bs : DC (c a b)
)
}
: Set
, A2 {- Set of descending chains -}
= data { $empty, $nonempty ( a : A, co : Co a, d : DC a ) }
: Set
, B2 ( a2 : A2 )
= case a2 of
{ $empty -> data {}
, $nonempty a co d ->
data { $0 {- to empty sequence -}
, $1 {- to sequence starting lower exponent -}
( b : B a
, co : Co (c a b)
, bs : DC (c a b)
)
, $2 {- to seq start with lower coeff -}
( cp : CoP a co
, b : B a
, co' : Co (c a b)
, bs : DC (c a b)
)
}
}
: Set
, c2 ( a2 : A2, b2 : B2 a2 )
= case a2 of
{ $empty -> case b2 of {}
, $nonempty a co d ->
case b2 of
{ $0 -> $empty
, $1 b co' bs -> $nonempty (c a b) co' bs
, $2 sp b co' bs
-> $nonempty a
(Cop a co sp)
($cons b co' bs)
}
}
: A2
}
in
T2F (struct { A = A2, B = B2, c = c2 })
: TS_s
}
: Theory
}
: Theory
{-
In conclusion:
It seems that despite being unable to say is a completely satisfactory way that a transition system is transitive, one can nevertheless quantify over transitive systems, by quantifying instead over arbitrary systems, and applying the predicate to their transitive transitive closure. (A generally applicable trick.)
Simulation is a problematic concept. One is interested in maximal fixpoints, but the usual definition involves impredicative existential second order quantification. But then, the usual definition of the `least (blah blah)' involves impredicative universal second order quantification, which seems even worse.
One can presumably define inductively the least discriminating bi-simulation between accessible states.
-}
{-
A comment I thought had something in it for salvage.
One can think of a chain in a transition system as traced out by a someone who abseils down on a rope, hopping from state down to state. Their trajectory is a descending chain, and to say that the initial state is accessible is to say that they will eventually reach the ground. The trajectory can be thought of as determining a word in the alphabet of states, and it happens that the lexicographic order of these words is well-founded if there's a well-founded order of the alphabet. (In fact, if the alphabet has order type $\alpha$, the dictionary has order type $2^\alpha$; moreover if the mountaineer is allowed to bounce finitely often where they are before hopping somewhere strictly beneath, the order type is $\omega^\alpha$.)
Can one express `lexicographic ' as an operator on transition systems? That is, we can attempt to define a binary relation on chains in a transition system, in analogy with the lexicographic order on descending chains in a given order. In fact, the definition of the lexicographic order works even for arbitrary sequences - as any dictionary shows. However the lexicographic construction on orders preserves well-foundedness for certain classes of sequences such as descending ($(2^\alpha)$), or non-increasing ($\omega^\alpha$). How are these facts proved?
-}