```
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'. (Another
way to put that: they're \emph{all} 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' was already taken by the category theorists. But perhaps
they have abandoned it for `monad'? In any case, it doesn't seem like
a good word to steal. It's like calling some random crazy data
structure a `pair'.
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
have a theory of transitive systems, by speaking instead about the
transitive closure of an arbitrary system. As with transitivity,
so with any other property that can be defined
inductively-recursively. The definitional equalities that you need
are assured, because they follow from definitions. (Of course!)
Simulation is a strange concept. One is interested in the `largest
bisimulation', 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
mountaineer, who abseils down on a rope, hopping from state down to
state. His trajectory is a descending chain, and to say that the
initial state is accessible, is to say that the mountaineer 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 the order
of the alphabet is well-founded. (In fact, if the alphabet has
order type $\alpha$, the dictionary has order type $2^\alpha$, and
if the mountaineer is allowed to bounce finitely often where he is
before hopping somewhere strictly beneath, the order type is
$\omega^\alpha$.) All this speaking loosely of course.
Now 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?
-}