[CST-2] Types

[Matthew Richards]

> Has anyone attempted 99 Paper 9 Q13 ?
> I cannot do the last part.  Presumably, we do not have to show how to
> compose f and g?  Is the Lift function from the previous section
> being used
> at all?

My answer for this is rather long and horrid, but...

[Using \ for little lambda and /\ for big lambda]
Assuming
  Opt_a  = all a'(a' -> (a->a') -> a')
  None_a = /\a (x':a', f:a->a'(x'))
  Some_a = \x:a (/\a' (\x':a', f:a->a'(f x)))

Then I think:

Compose_g_d_e = \f:g->Opt_d, g:d->Opt_e ( \v:g (
                     /\a' (\x':a', f':e->a' (
                     (f v) a' x' (\v':d (
                     (g v') a' x' (\v'':e (f' v''))
                     )))

Sorry, that looks even worse in ASCII than on paper! As usual with Types
questions, it took far too long to do for 5 marks :-(  I just hope we
wouldn't be expected to prove it's right too!  Looking at it now, I'm not
entirely sure about whether the \v:g is in the right place, but I'll leave
it as it is and see if anyone corrects it!

> Also, 1998 P7 Q10, I think every function N -> N is PLC representable, but
> cannot justify it  :-(

I think that not all functions N -> N are representable, since PLC is not
Turing powerful (due to the Strong Normalisation property).

Matthew