                           premise.demon.co.uk
        peter 37622 Nov 9 22:47
       /home/peter/half/ts.half

November 9, 1997

¡code¿ Time-stamp: ”1997-11-09 22:47:13 peter” ¡/code¿

This is a script for the type-checker CHalf. Here is a hastily written explanation of CHalf’s syntax in ¡a href=”half.html”¿ html ¡/a¿.

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.

Contents

1 Motivation 1 1.1 themes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

2 Transition Systems 6

3 ABc form – ‘Triples’ 17

4 Arithmetic of transition systems 18

1 Motivation

One strand in the notion of set is ‘set 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 P(A) in a strong way and a weak way.

• In the strong interpretation, P(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 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.

• In the weak interpretation, P(A) is the type of families of A’s, i.e. functions into A defined on some index set. A family is specified parametrically, with an expression containing a parameter which varies over the index set: that is, parametrically. (C.f. giving a parabola in parametric form (x = at^{2}, y = 2at)).

Along with the weak and the strong forms of P(A), 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 P(A), is that t he argument occurs negatively in the definition of Pow(A), (the type of predicates on a set A), and positively in the definition of Fam(A) (the type of families of elements of A. So one can think about the fixed points of 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’.

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

#include "./standard.half"
#include "./Boole.half"
#include "./world.half"

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 P(A), and the set of functions from the set A into P(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 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

2 Transition Systems

Explanation needed here.

Hypo-relations? Semi-relations? If one interprets P(A) as ‘set of subsets of’, and ‘subset of’ as ‘indexed family

of’, then it is far from clear that P(A) is much like the set of functions from the set A into P(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 state. The value of the function for a given state a is the set of states 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 first a transition relation, 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 Δ-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 transition, to c. I shall call the values {c(a, b) | b : B(a)} derivatives, or ( 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 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 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 ⊆→; R; ←,

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    : Pow A
, cstar = th.end3   : ( 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

3 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

4 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 α+β, α.β, (1+α)^{β} from a pair well-orderings with order types α and β.

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:

• nil ≺ cons h tl
• cons h1 tl1 ≺ cons h2 tl2 ⟸ h1 < h2
• cons h tl1 ≺ cons h tl2 ⟸ tl1 ≺ tl2

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 inductivelyrecursively. 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 α, the dictionary has order type 2^{α}, and if the mountaineer is allowed to bounce finitely often where he is before hopping somewhere strictly beneath, the order type is ω^{α}.) 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^{α})), or non-increasing (ω^{α}). How are these facts proved?