CIS505/705 Worksheet Oct. 27    SAMPLE SOLUTIONS

1.    ( lam y. (lam z. z)((lam x. x) y) ) 5 

One legal reduction sequence:
bind 5 to y:                  =>  (lam z. z)((lam x. x) 5)
bind ((lam x. x) 5) to z:     =>  (lam x. x) 5
bind 5 to x:                  =>   5

Another:
=>  (lam z. z)((lam x. x) 5)
=>  (lam z. z)(5)
=>  5

There are others.  All produce  5.


2.  The Python code:

x = 2
def f(y): global x
          return y + x
x = x + 1
print f(99)

looks like this in lambda notation:

(lam x.
   (lam f.
      (lam x. (f 99 x) 
      ) (x + 1)
   )(lam y. lam x. y + x)
)(2)

An outside-in reduction, which matches Python's execution steps:
=>    
(lam f.
      (lam x. (f 99 x)   // notice that  2  is not pasted here!
      ) (2 + 1)
)(lam y. lam x. y + x)   // notice that  2  is not pasted here!

=>
     (lam x. ((lam y. lam x. y + x) 99 x)
     ) (2 + 1)

=>  (lam y. lam x. y + x) 99 (2+1)   // notice that the inner x is not changed!
  
=>  (lam x. 99 + x) (2+1)

=>  99 + (2+1)
    


3.  Let  F  be a "global variable" that we don't have just yet.

(lam s. F(s s))(lam s. F(s s))

=> F ( (lam s. F(s s)) (lam s. F(s s)) )

=> F (F ((lam s. F(s s)) (lam s. F(s s))))

=> F (F (F (lam s. F(s s)) (lam s. F(s s))))

=> ... and so on, forever ...



4. 
[0] == lam s. lam z. z
[1] == lam s. lam z. s z
[2] == lam s. lam z. s (s z)
[SUCC] == lam n. lam s. lam z. s (n s z) 


[2] [SUCC] [0]

== (lam s. lam z. s (s z)) [SUCC] [0]                 // defn of [2]

=> (lam z. [SUCC] ([SUCC] z) [0]

=> [SUCC] ([SUCC] [0])                               // "do [SUCC] twice" to [0]

== [SUCC] ((lam n. lam s. lam z. s (n s z)) [0]      // defn of [SUCC]

=> [SUCC] (lam s. lam z. s ([0] s z))

== [SUCC] (lam s. lam z. s ((lam s. lam z. z) s z))  // defn of [0]

=>=> [SUCC] (lam s. lam z. s (z))                    // this is  [SUCC][1]

=> ... => lam s. lam z. s (s z)                      // this is [2]