Programming Languages, Fall 2014
HW5 - Lambda Calculus II
Due electronically on Blackboard on Tuesday October 14, 2pm.

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. Work out (plus c3 c2). Explain the intuition behind plus.

2. Work out (times c3 c2). Explain the intuition behind times.

3. Redefine times without using plus. Explain the new intuition.

4. Define two versions of the power function, one with and one without times.
    Work out (power c3 c2). Explain the intuitions behind each definition.

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

6. 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.  

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

8. 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?

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

10. Consider the call-by-name Y-combinator:

   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].

11. Exercise 5.2.8 (list).

12. 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.