Programming Languages, Fall 2013
HW5 - Lambda Calculus II
Due electronically on Blackboard on Tuesday October 8, 11:59pm.
Those who submit by Monday Oct 7 will receive extra credit.

Typesetting via LaTeX is recommended but not required.

Expected Amount of Work for an average student: 6-8 hours.

Textbooks for References:
[1] TAPL, Chap. 5
[2] Wikipedia article http://en.wikipedia.org/wiki/Fixed-point_combinator
[3] Wikipedia article http://en.wikipedia.org/wiki/Lambda_calculus


1. Use prd to define subtract, equal, and gt ("greater-than").
   Work out (subtract c5 c2) and (gt c2 c3).

2. A quick-n-dirty way to simulate lambda calculus on Haskell is as follows 
   (suggested by Cong, Dezhong, and Eric):
   
   c0 = \s z -> z
   c1 = \s z -> s z
   plus = \m n s z -> m s (n s z)

   Now you can "sort-of" test them in ghci:

   > c0 (+1) 0
   0
   > plus c1 c1 (+1) 0
   2

   Note we have to supply (+1) for s and 0 for z, otherwise the return values
   are functions which Haskell cannot display, i.e., equivalently:

   > let f = plus c1 c1
   > f (+1) 0
   2
   
   (f is a function that is "behaviorally equivalent" to c2.) 

   Write and test 
   1) tru, fls, not, and, or, pair, fst, snd
   2) scc, scc2, times, times2, times3, power1, power2, prd, subtract, equal, gt
   
   In Chap. 7 we will see a real implementation of lambda calculus on Haskell.  

3. Define the operational semantics of lambda calculus for 
   "full (non-deterministic) beta reduction". 
   
   Note that in HW4, many calculations involving Church numerals rely on full 
   beta reduction otherwise you'll only get "behaviorally equivalent" terms.

4. Assuming strict call-by-value evaluation:
   (1) is there a normal form that is not a value?
   (2) is there a value that is not a normal form?
   (3) does every term evaluate to a normal form?

5. Convert the factorial function to pure lambda calculus:
   f = \fct. \n. if n=0 then 1 else n*(fct (pred n))

6. The call-by-name Y-combinator is simpler than the call-by-value one
   we studied in the slides and the book (this is intuitive because it's harder
   to diverge in a call-by-name setting):

   Y = \f. (\x. f (x x)) (\x. f (x x))

   Let 
       fact2 = Y f 
   where f is the function in the above question. Work out (fact2 3).

   Hint: [2].

7. Exercise 5.2.8 (list).

8. Exercise 5.2.11 (list sum).

Solutions can be found at the end of the book.

Debriefing (required!): --------------------------

1. Approximately how many hours did you spend on this assignment?
2. Would you rate it as easy, moderate, or difficult?
3. Did you work on it mostly alone, or mostly with other people?
4. How deeply do you feel you understand the material it covers (0%–100%)? 
5. Any other comments?

This section is intended to help us calibrate the homework assignments. 
Your answers to this section will *not* affect your grade; however, skipping it
will certainly do.