Programming Language Principles Solution to Homework for Week 04. 1. Identify the free variable occurrences in the following AE's: (a) fn x. x y - (b) (fn y. fn x. x+y) x 1 - (c) (fn x. fn y. x y) x - (d) (fn x. ((fn y. fn x. x+x) (x+1) (y+1)) +1) 1 - Reduce the above AE's. (a) fn x. x y (already reduced) (b) (fn y. fn x. x+y) x 1 ( fn x'. x'+x) 1 1+x (c) (fn x. fn y. x y) x fn y. x y (d) (fn x. ((fn y. fn x. x+x) (x+1) (y+1)) +1) 1 (fn x. (( fn x. x+x) (y+1)) +1) 1 (fn x. (y+1+y+1) +1) 1 y+1+y+1+1 2. (a) (fn x.x+1) 3 3+1 (b) (fn x.1+(fn y.y+1) 3) 2 1+(fn y.y+1) 3 1+ 3+1 (c) (fn x.1+(fn x.x+1) 3) 2 1+(fn x.x+1) 3 1+ 3+1 (d) (fn x. fn y. x+y) 3 4 ( fn y. 3+y) 4 3+4 (e) (fn x. fn y. x+y) 3 fn y. 3+y (f) (fn x.x) 3 3 (g) (fn x. fn y. y x) 1 fn y. y 1 (h) (fn x. fn y. x y) (fn z. z+2) 1 ( fn y. (fn z.z+2) y ) 1 (fn z.z+2) 1 1+2 (i) (fn x. fn y. x y) (fn y. y+2) 1 ( fn y. (fn y.y+2) y ) 1 (fn y.y+2) 1 1+2 (j) (fn x. fn y. x y) (fn x. fn y. x y) (fn z. z+1) 1 ( fn y. (fn x. fn y. x y) y) (fn z. z+1) 1 ( (fn x. fn y. x y) (fn z. z+1)) 1 ( fn y. (fn z.z+1) y) 1 (fn z.z+1) 1 1+1 (k) (fn x. fn y. x) 1 3 ( fn y. 1) 3 1 (l) (fn x. fn y. y) 1 3 ( fn y. y) 3 3 (m) (fn x. x+2) ((fn y. y+1) 3) ((fn y.y+1) 3) + 2 3+1 + 2 (n) (fn x. x+2) (fn y. y+1) 3 ( (fn y.y+1) + 2 ) 3 (o) (fn x. x x) 1 1 1 (p) (fn x. x x) (fn y. y 1) (fn y. y 1) (fn y. y 1) (fn y. y 1) 1 1 1 (q) (fn x. x x) (fn y. fn z. y z) (fn z. z+1) 1 ( (fn y.fn z.y z) (fn y.fn z.y z) ) (fn z. z+1) 1 ( fn z. (fn y.fn z.y z) z ) (fn z. z+1) 1 ( (fn y.fn z.y z) (fn z.z+1) ) 1 ( fn z. (fn z.z+1) z ) 1 (fn z.z+1) 1 1+1 3. In the following, even the most trivial steps are shown. (fn x. fn y. -xy) y x { [y/x] (fn y.-xy) } x by axiom beta. { fn y`. [y/x] ([y`/y] (-xy)) } x by case 3.2.3. { fn y`. [y/x] ([y`/y](-x) [y`/y]y) } x by case 2. { fn y`. [y/x] (([y`/y](-) [y`/y]x) [y`/y]y) } x by case 2. { fn y`. [y/x] (( (-) [y`/y]x) [y`/y]y) } x by case 1.2. { fn y`. [y/x] (( (-) x) [y`/y]y) } x by case 1.2. { fn y`. [y/x] (( (-) x) y`) } x by case 1.1. { fn y`. [y/x] (-x) ([y/x] y`) } x by case 2. { fn y`. ([y/x] (-) [y/x] x) ([y/x] y`) } x by case 2. { fn y`. ( - [y/x] x) ([y/x] y`) } x by case 1.2. { fn y`. ( - y) ([y/x] y`) } x by case 1.1. { fn y`. ( - y) y` } x by case 1.2. [x/y`] ((-y)y`) by axiom beta. ([x/y`] (-y)) ([x/y`]y`) by case 2. ([x/y`] (-) ([x/y`]y)) ([x/y`]y`) by case 2. - ([x/y`]y)) ([x/y`]y`) by case 1.2. - y ([x/y`]y`) by case 1.2. - y x by case 1.1. 4. a) Draw the AST. let ____/ \____________________ / \ and G _______/ \_______ / \___ / \ G \ fcn_form within / \ G / | | \ / \________ f nil / \ f x v aug = \ p tau / \ / \___ fcn_form / \ x v , \ / | \_____ 1 2 / \ tau p , \ x y / \ / \ -> 1 1 r s ___/|\___ / | \ eq + + / \ / \ / \ s 1 r x r y b) Transform the AST to the standardized tree. G _________/ \_________ / \ L tau / \ ________/ \_______ T G / \ __/ \ L G / G / \ / \___________ L / \ x L L \ / \ T 1 / \ / \ tau f G v G T G / \ __/ \ / \ / \_______ 1 1 / G G v L \ L / \ / \ / \ G / \ T 2 aug x x G / \ p G / \____ T 1 / \___ L G G \ / \ / \ / \ G y L T 2 f nil / \ / \ p tau T G / \ / \_______ 1 2 L \ / \ G r G / \ / \____ T 1 L \ / \ G s G / \ / \ T 2 G nil / \__________ G \ / \___ L G \ / \ / \ L () G Cond G / \ / \ / \ () G G y G 1 / \ / \ / \ G x + r eq s / \ + r c) Transform the standardized tree to a lambda expression. Lambda expression: (fn T. (fn f. (fn p. (f nil) (p (1,2)) ) (T 2) ) (T 1) ) ( (fn x. fn y. x aug y) , (fn T. (fn x. (fn y. (fn T. ( fn r. ( fn s. Cond (s eq 1) (fn ().r+x) (fn ().r+y) nil) (T 2) ) (T 1) ) ) (T 2) ) (T 1) ) (1,1) ) => (fn T. (fn f. (fn p. (f nil) (p (1,2)) ) (T 2) ) (T 1) ) ( (fn x. fn y. x aug y) , (fn x. (fn y. (fn T. ( fn r. ( fn s. Cond (s eq 1) (fn ().r+x) (fn ().r+y) nil) (T 2) ) (T 1) ) ) ((1,1) 2) ) ((1,1) 1) ) 5. (a) (fn x. x+1) 2 2+1 (b) (fn x. x+3) [(fn y. 2*y) 7] (fn x. x+3) [ 2*7 ] 2*7+3 (c) {fn y. (fn x. y) [(fn x. x x) (fn y. y y)]} 1 (fn x. 1) [(fn x. x x) (fn y. y y)] 1 (d) (fn z. (fn x. x+1) [(fn x. x+z) 1]) fn z. (fn x. x+1) [ 1+z ] fn z. 1+z+1 (e) (fn x. (fn x. (fn x. x+1) (x+2)) (x+3)) x (fn x. (fn x. x+2+1 ) (x+3)) x (fn x. x+3+2+1 ) x x+3+2+1 (f) (fn y. [fn x. (fn y. y+x+a) (y+2)] [(fn t. fn s. t) y x]) 5 (fn y. [fn x. y+2+x+a ] [ (fn s. y) x]) 5 (fn y. [fn x. y+2+x+a ] [ y ]) 5 [fn x. 5+2+x+a ] 5 5+2+5+a (g) [fn f. fn x. f(f x)] [(fn g. fn y. g y) (fn x. x*2)] 3 [fn f. fn x. f(f x)] [ fn y. (fn x.x*2) y ] 3 [fn f. fn x. f(f x)] [ fn y. y*2 ] 3 [ fn x. (fn y.y*2) ((fn y.y*2) x) ] 3 (fn y.y*2) ((fn y.y*2) 3) (fn y.y*2) ( 3*2 ) 3*2*2 (h) (fn x. (fn y. y x 4) (fn x. fn y. x+y)) ((fn x. x*2) 3) (fn x. (fn x. fn y. x+y) x 4 ) ( 3*2 ) (fn x. fn y. x+y) 3*2 4 (fn y. 3*2+y) 4 3*2+4 6. (fn x.x+x) [(fn y.y+y) {(fn z.z+z) [(fn v.v+v) 2]}] => (fn x.x+x) [(fn y.y+y) {(fn z.z+z) [ 2+2 ]}] => (fn x.x+x) [(fn y.y+y) { 2+2+2+2 }] => (fn x.x+x) [2+2+2+2 +2+2+2+2 ] => 2+2+2+2 +2+2+2+2 +2+2+2+2 +2+2+2+2 (==delta==> 32) In programming language order, 4 beta reductions are necessary. In normal order, # beta reductions[(fn x.x+x) E] = 1+2*(# beta reductions[E]) (fn x.x+x) [(fn y.y+y) {(fn z.z+z) [(fn v.v+v) 2]}] Thus: 1+2* ( 1+2* ( 1+2* ( 1+2* 0))) = 15 beta-reductions in normal order.