Posted by Kevin Chang on February 16, 2004 at 20:09:44:
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