[CST-2] Types

[M.Y.W.Y. Becker]

Hi Matthew,

--On 02 June 2001 08:29 +0100 Matthew Richards <mwr22@cam.ac.uk> wrote:
[...]
> 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'))
                 ^^^
               A \ missing here.



>   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''))
>                      )))

A better solution would be
Compose_g_d_e = \f:gamma->Opt_d, g:d->Opt_e (\x:gamma (f x Opt_e None_e g)).


> 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!

I'm not sure whether your formula is correct but it's too complicated 
anyway.


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

Even if PLC was Turing powerful not all functions N->N could be 
represented, since there are also uncomputable (total) functions N->N. But 
since PLC is not even Turing powerful it can of course not represent all 
total functions.

Mo