[ -rw-r--r-- 1 peter other 4394 Oct 13
11:59 /home/peter/half/on.half ]

November 9, 1997

Time-stamp: "1997-10-13 11:59:16 peter"
#include "./standard.half"
#include "./Boole.half"

N3 = {-Codes for the first 3 ‘number-classes’ -}

data { $0, $1, $omega }
: Set

, T3 = {-decoding an element of N3 -}

\ n3 ->
case n3 of

{ $0 -> N0 {-the empty set -} , $1 -> N1 {-‘the’ singleton -} , $omega -> Nat {-the natural numbers -}

}
: Pow N3

, O = {-trees with 3 kinds of node - nillary, unary, countably branching. -}

data { $0 {-nillary -} , $S ( p : O ) {-unary -} , $L ( os : ( n : Nat )-> O ) } {-countably branching -}

: Set

I call the elements of the type O countable tree ordinals.

{-There is something unresolved below: debris -}

, O' = {- might these work?! -}

  data { $0 ( os : ( n : N0 )-> O' )
       , $S ( os : ( n : N1 )-> O' )
       , $L ( os : ( n : Nat )-> O' ) }
: Set

, ON {-ordinal notations for countable tree-ordinals -}

= sig
{ T : Set
, cf : ( t : T )-> N3
, pd : ( t : T
       , i : T3 (cf t)
       )-> T
}
: Type
, Example1

= {-notations for ϵ_{0}. -}

let { T = data
          { $0, $W ( a : T, b : T ) }
        : Set
    , f = \ a b n
          -> case n of
             { $0  -> a
             , $S p -> $W (f a b p) b
             }
        : ( a : T, b : T, n : Nat )-> T
    , g = \ a b c
          -> case c of
             { $0  -> f a b
             , $W a1 b1 -> \ n -> $W a (g b a1 b1 n)
             }
        : ( a : T, b : T, c : T, n : Nat )-> T
    } in
    struct
    { T = T
    , cf = \ t
           -> case t of
              { $0  -> $0
              , $W a b
                -> case b of
                   { $0  -> $1
                   , $W a1 b1 -> $omega
                   }
              }

, pd = \ t
 -> case t of
    { $0  -> \ i -> case i of {}
    , $W a b
      -> case b of
         { $0  -> \ i -> a
         , $W a1 b1 -> g a a1 b1
         }
    }
}
: ON
, Example2

= {-cheating ordinal notations: the ordinals themselves -}

struct
{ T  = O
, cf = \ t
-> case t of
{ $0 -> $0
, $S junk -> $1
, $L junk -> $omega
}
, pd = \ t
-> case t of
{ $0  -> \ i -> case i of {}
, $S p -> \ i -> p
, $L os -> os
}
}
: ON
, Acc (X : ON, a : X.T )
= data { $0 ( phi : ( i : T3 (X.cf a) )-> Acc X (X.pd a i) ) }
: Set

{-Now some definitions that do not work .. -}

, ON2O ( X : ON, a : X.T, a' : Acc X a )

= {-the interpretation of the accessible element a as an ordinal -}

let { t = X.cf a : N3 } in
case a' of {
$0 phi -> case t of {
   $0  -> $0,
   $1  -> $S (ON2O X (X.pd a [$0]) (phi [$0])),
   $omega  -> $L (\n->ON2O X (X.pd a [n]) (phi [n]))}}
: O

{-try to reverse the approach -}

, ON2O ( X : ON, a : X.T, a' : Acc X a )

= {-the interpretation of the accessible element a as an ordinal -}

case X.cf a of
{ $0  -> $0
, $1  -> case a' of
         { $0 phi -> $S (ON2O X (X.pd a [$0]) (phi [$0]))}
, $omega
      -> case a' of
         { $0 phi -> $L (\n->ON2O X (X.pd a [n]) (phi [n])) }
}
: O
, Acc' ( X : ON, a : X.T )
= case X.cf a of
{ $0  -> N1
, $1  -> Acc' X (X.pd a [$0])
, $omega  -> ( n : Nat )-> Acc' X (X.pd a [n])
}
: Set
, th ( A : Set, B : ( a : A )-> Set, c : ( a : A, b : B a )-> A )
= theory
{ W
  = data { $0 ( a : A, phi : ( b : B a )-> W ) }
  : Set
, t ( w : W )
  = case w of { $0 a phi -> a }
  : A
, Acc ( a : A )
  = data { $0 ( phi : ( b : B a )-> Acc (c a b) ) }
  : Set
, Acc2W ( a : A, a' : Acc a )
  = case a' of
    { $0 phi -> $0 a ( \ b -> Acc2W (c a b) (phi b) ) }
  : W
}
: Theory

5