Posted by Kevin Chang on February 16, 2004 at 22:27:34:
In Reply to: missing lecture notes posted by Kevin Chang on February 16, 2004 at 20:09:44:
I found the rest in "A Simple Algorithm and Proof for Type Inference", thanks,
Kevin
: I'm missing a little bit of lecture notes on 2/9/04 (Monday). I have the following example from lecture, where I use ^ to mean lambda to save typing:
: (empty,^x.^y.^z.(xz)(yz),t0) t0=t1->t2
: ((x:t1),^y.^z.(xz)(yz),t2) t2=t3->t4
: ((x:t1,y:t3),^z.(xz)(yz),t4) t4=t5->t6
: ((x:t1,y:t3,z:t5),(xz)(yz),t6) uh...?
: Here I stopped taking notes. I know that (xz) is t7->t6, and (yz) is t7. However can someone please post the complete solution as I'm not so sure how to derive the rest? Thanks!
: Kevin