                           premise.demon.co.uk
         peter 8452 Jan 9 13:29
      /home/peter/half/Expr.half

January 9, 1998

Towards a categorical treatment of variable binding.

The problem is to find a category with an endo-functor having an initial algebra which is recognisably the untyped lambda-calculus. A necessary criterion of recognisability is a definition of substitution using only structural recursion, meaning the universal properties of the initial algebra.

We start with the following Haskell code.

data M x = Old x | New
aM :: (x -> y) -> M x -> M y
aM f m = case m of New -> New
                   Old x -> Old (f x)
data E x = Var x | App (E x) (E x) | Abs (E (M x))
aE ::  (x -> y) -> E x -> E y
aE f e = case e of Var x -> Var (f x)
                   App e1 e2 -> App (aE f e1) (aE f e2)
                   Abs e -> Abs (aE (aM f) e)
lift :: (x -> E y) -> M x -> E (M y)
lift phi m = case m of New -> Var New
                       Old x -> aE Old (phi x)
sub :: E x -> (x -> E y) -> E y
sub e phi  = case e of Var x -> phi x
                       App e1 e2 -> App (sub e1 phi) (sub e2 phi)
                       Abs e -> Abs (sub e (lift phi))
subme :: E x -> M x -> E x
subme e m  = case m of { New -> e ; Old x -> Var x }
sub1 :: E (M x) -> E x -> E x
sub1 e e' = sub e (subme e')

Anyone who has ever written functional programs to deal with lambdacalculus expressions in ‘de-Bruijn form’, will have written something very like this code. If they wrote it in ML, they will shortly after have encountered a major brutality of ML’s type system, that recursively defined names must be monomorphically typed. (See: Polymorphic Type Schemes and Recursive Definitions, Alan Mycroft, 1984 LNCS 167.) Haskell is slightly more accomodating. It allows polymorphic typing of such names, so long as you declare the types yourself. (If the type-declarations are commented out, the Haskell type-checker will reject the definitions.)

The program above can be written in constructive type-theory. The following, which needs revision and explanation, sketches one way to go about this, using the typechecker half. There is probably a theorem or two to prove that I’ve actually defined substitution correctly. (I believe that Hilbert, Ackermann, Gödel, and numerous brilliant logicians actually had bugs in their definitions; and that the first logician to give a correct definition was Church, in his book ‘Mathematical Logic’. So maybe I shouldn’t assume that my definition is correct!

Maybe ( X : Set ) The ‘successor’ of a set

  = data { $new, $old ( x : X ) }
  : Set
,
  MaybeA ( X : Set, Y : Set, f : ( x : X )-> Y )
  = \ mx -> case mx of { $new  -> $new, $old x -> $old (f x) }
  : ( x : Maybe X )-> Maybe Y
,
  MaybeUnit ( X : Set )
  = \ x -> $old x
  : ( x : X )-> Maybe X
,
  MaybeBind ( X : Set, Y : Set, f : ( x : X )-> Maybe Y )
  = \ mx -> case mx of { $new  -> $new, $old x -> f x }
  : ( x : Maybe X )-> Maybe Y

,

FamSet A set-indexed family of sets

= sig { U : Set, T : Pow U }
: Type

, The successor of a FamSet (not used)

SUCC ( UT : FamSet )
= struct {
    U = Maybe UT.U
  , T = \ u -> case u of { $new  -> UT.U, $old x -> UT.T x }
  }
: FamSet

, Closure of a family under Maybe

Closure ( UT : FamSet )
= let {
    U   = UT.U : Set
  , T   = UT.T : Pow U
  , U'  = data { $0 ( u : U ), $S ( p : U' ) } : Set
  , T'  = \ u' -> case u' of { $0 u -> T u
                             , $S p -> Maybe (T' p) }
        : Pow U'
  } in
  struct { U = U', T = T' }
: FamSet

,
Experiment1 ( UT : FamSet )
= let
{

We want to assume we have a FamSet which is closed under ‘maybe’. One way to do this is to assume we have an arbitrary FamSet, and then work with its closure under ‘maybe’.

UT' = Closure UT : FamSet
,
I = UT'.U : Set
,
T = UT'.T : Pow I
,

We can make I into a category

I_Arrow ( i : I, j : I )
= ( x : T i )-> T j
: Set

Some properties of ‘maybe’ re-expressed using the T-predicate ‘Maybe’ is a kind of successor operator, hence letter ‘S’.

,
S_Arrows( i : I, j : I )
= MaybeA (T i) (T j)
: ( f : I_Arrow i j )-> I_Arrow ($S i) ($S j)
,
S_Unit( i : I )
= MaybeUnit (T i)
: I_Arrow i ($S i)
,
S_Bind( i : I, j : I )
= MaybeBind (T i) (T j)
: ( f : I_Arrow i ($S j) )-> I_Arrow ($S i) ($S j)
,

The category we are looking for Since I is a category, we have some kind of pre-sheaves over I

Obj = Pow I : Type
,
Arr = \ X Y ->
      ( i : I )->
      ( x : X i )-> Y i
    : (X : Obj, Y : Obj )-> Set

The endo-functor we are looking for

, On objects

Phi = \ X i ->
      data { $Var' ( x : T i )
           , $App' ( f : X i, a : X i )
           , $Abs' ( b : X ($S i) )
           }
    : ( X : Obj )-> Obj

, On arrows

PhiA = \ X Y f ->
       \ i x' ->
       case x' of
       { $Var' x    -> $Var' x
       , $App' f1 a -> $App' (f i f1) (f i a)
       , $Abs' b    -> $Abs' (f ($S i) b)
       }
     : ( X : Obj, Y : Obj, f : Arr X Y )->
       Arr (Phi X) (Phi Y)
,

Phi_Init This causes technical problems with half

= let { X = Phi X : Obj } in X
: Obj
,

E A work-around. The object of the initial algebra for Phi.

= \ i ->
  data { $Var ( v : T i )
       , $App ( f : E i, a : E i)
       , $Abs ( b : E ($S i))
       }
: Obj
,

E2PhiE ( i : I ) Another part of the work around.

= \ x -> case x of { $Var v   -> $Var' v
                   , $App f a -> $App' f a
                   , $Abs b   -> $Abs' b }
: ( x : E i ) -> Phi E i
,

The initial algebra’s structure map, if that’s the right jargon

Phi_InitA
= \ E' e' ->
  \ i x ->
  e' i
  (PhiA E E' (Phi_InitA E' e') i (E2PhiE i x))

: ( E' : Obj, e' : Arr (Phi E') E' )->
  Arr E E'
,

A functorial property of E. Should use structure map

lift ( i : I, e : E i )
= \ j m ->
  case e of
  { $Var v   -> $Var (m v)
  , $App f a -> $App (lift i f j m) (lift i a j m)
  , $Abs b   -> $Abs (lift ($S i) b ($S j) (S_Arrows i j m))
  }
: ( j : I, m : I_Arrow i j )-> E j
,
up
= \ i x ->
  lift i x ($S i) (S_Unit i)
: ( i : I, x : E i )-> E ($S i)
,
up1 ( i : I, j : I, m : ( x : T i )-> E j )
= \ x ->
  case x of { $new    -> $Var $new, $old x1 -> up j (m x1) }
: ( x : T ($S i) )-> E ($S j)

The substitution function. Should use structure map

,
sub ( i : I, e : E i )
= \ j phi->
  case e of
  { $Var v   -> phi v
  , $App f a -> $App (sub i f j phi) (sub i a j phi)
  , $Abs b   -> $Abs (sub ($S i) b ($S j) (up1 i j phi))
  }
: ( j : I, phi : ( t : T i )-> E j )-> E j
,
E' ( i : I )
= ( j : I, phi : ( t : T i )-> E j )-> E j
: Set
,
E'A ( i : I, i' : I, m : I_Arrow i i', e' : E' i)
= \ j phi -> e' j ( \ t -> phi (m t) )
: E' i'

} in

some debris from testing the above

theory
{ I_term ( i : I )
= $Abs ($Var $new)
: E i
, K_term ( i : I )
= $Abs ($Abs ($Var ($old $new)))
: E i
, S_term ( i : I )
= $Abs ($Abs ($Abs
       ($App ($App ($Var ($old ($old $new)))
                   ($Var $new))
             ($App ($Var ($old $new))
                   ($Var $new)))))
: E i
, M_term ( i : I )
= $Abs ($App ($Var ($old $new)) ($Var ($old $new)))
: E ($S i)
, test   ( i : I )
= sub ($S i) (M_term i)  i
  ( \ t -> case t of { $new  -> I_term i
                     , $old x -> $Var x
                     } )
: E i
}
: Theory