[CST-2] 1 x General Question + 2 x Types

[M.Y.W.Y. Becker]

General question: I was a bit confused to see that all past papers only had 
13 questions. This year's papers will have 15 questions, is that correct?


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?



Types 2000/9/13
Third part (Prove PHI(G,M,t)):
Proof by rule induction (on structure of M):
(var),(fn),(app) are straight forward, but I would like to check (gen) and 
(spec):

(gen):
Assume G |- /\a(M): forall a.(t), and rho(forall a.(t))=false.

Then a,G |- M:t, and rho[a->true](t) & rho[a->false](t) = false.
So either rho[a->true](t)=false or rho[a->false](t)=false.
W.l.o.g. suppose rho[a->true](t)=false.

By induction hypothesis there exists a
(x_i:t_i) in G_ta such that rho[a->true](t_i)=false.
But "a" cannot be free in t_i since G ok.
Using the given lemma, rho(t_i)=false. q.e.d.

(spec)
Assume G |- M t: t'[t/a], and rho(t'[t/a])=false.

Then G |- M: forall a.(t'), and rho[a->rho(t)](t')=false, using the given 
lemma.
Either rho(t)=true or rho(t)=false, so in any case
So rho(forall a.(t'))
 = rho[a->true](t') & rho[a->false](t')
 = false.
By induction hypo, G has the required property.

Is that the right way to do it? I found it quite hard for a 30min 
question...


Mo