[CST-2] 2 x Types

[Matthew Richards]

[...]
> Types 2000/7/11
> Last 1 mark question:
> I would say that there always exists a principal typing if there is any 
> typing. Reason: if mgu() is used to find the substitutions in the typing 
> algorithm then the resulting typing (S,t) is a principal typing 
> since mgu() 
> can always find the most general unifier if it exists.
> 
> Is that convincing?

It convinces me :-)

> Types 2000/9/13
> Third part (Prove PHI(G,M,t)):
> Proof by rule induction (on structure of M):
[...]
> Is that the right way to do it? 

They both look right to me, and I can't see any better way of doing it.

> I found it quite hard for a 30min question...

I always find questions hard to fit into 30 minutes :-)

Matthew