HW 1: Lambda Calculus (and Haskell)

Overview

In this assignment, we are going to (continue to) do something that may seem very strange to us: We are going to encode data structures as functions. In other words, using only lambda-calculus, we will implement ways to store and operate on boolean values, values called maybes (that represent the presence or absence of other values), lists, and trees. We will also write iterative and recursive functions in lambda calculus. The goal of our work is to become comfortable with higher-order functions, with lambda calculus, and with thinking about familiar things (e.g., lists and trees) in new and unfamiliar ways.

Similar to last week, the second part of the homework will ask you to do some background learning online before Monday’s class; it should take about an hour.

Tips for working on the assignment

  • Read the assignment carefully. In general, CS 131 assignments require more careful reading than you might be familiar with from CS courses.
  • It can help to code the problems in a language you know (e.g., Python), then translate the code into lambda calculus.
  • It can help to think about which part of a lambda-calculus expression describes the input to the expression and which part corresponds to the implementation / encoding. For example, to represent true, we use the lambda-calculus expression (λ x . (λ y . x)). It is helpful to see this expression as a function that takes two inputs and returns one of them (rather than as a function that takes an argument and returns a function that takes an argument…).

Getting Started

Reminder: Pair Programming

You may work on this assignment by yourself or with a partner. If you work with a partner, you must follow pair programming rules at all times (even when writing text or math) and share the driver/navigator roles equally. Both members of the pair must contribute to and understand all parts of jointly submitted work. You are not required to work with your partner from lab.

Getting the materials

Use the GitHub classroom link on Piazza and the assignment workflow to get the materials for this assignment.

Be sure to regularly commit and push your changes. Remember that you should always start your work session with a pull to the computer you are working on, and end your session with a push back to GitHub.

Part 1: Coding in the Lambda Calculus

This part involves using lc on Knuth, as you did in lab. For all questions, you can (and should) use helper definitions when it makes your code more readable.

Your answers go into the files hw1.lc as instructed. You’ll want to test your code with lc. Remember you have to :reload the definitions every time you make changes.

Leq [10%]

In the hw1.lc file, define a new macro Leq that takes two church numerals as arguments, such that ((Leq n) m) reduces to True if $n \leq m$, and to False otherwise. (If you make good use of the existing definitions for numeric operations, this function can be defined in one line!)

Reload hw1.lc into lc and check that your definition works on specific inputs like 3 and 4, or 5 and 4, or 5 and 5.

Equal [10%]

In the hw1.lc file, define a new macro Equal that takes two Church numerals as arguments, and returns True if they are equal and False otherwise. Test your definition to confirm it works. (This function can also be done in one line if you use Leq.)

Maybes [20%]

A pair is a container for two values (the first component and the second component). We’ve seen one way to encode pairs as functions in lambda calculus.

Similarly, a maybe is a container that can hold only one value, but it’s allowed to be empty: a maybe either contains zero values or one value.

Every maybe is built either with the constant Nothing (an empty container) or a function call (Just x) (which creates a container holding the value x).

We could imagine using booleans and pairs to encode maybes, the way we encoded lists in the lab: Every maybe is a pair; the first component of the pair contains a boolean saying whether the container is empty or not (i.e., whether the maybe is a Nothing or a Just). If the container is not empty, the second component of the pair contains the value.

But a more elegant encoding is inspired by the encoding of booleans. The most important operation on booleans is to make a choice (compute $e_1$ if the boolean is true, and compute $e_2$ if the boolean is false); as long as we can make choices, we can compute all the “usual” boolean operations like Not, And, and Or. This choice-making is so fundamental that we defined the boolean values True and False to be functions that make choices, so that the function application ((b e1) e2) produces e1 if b turns out to be the boolean True, and produces e2 if b turns out to be the boolean False.

Similarly for maybes, the critical operation is to determine whether the container is empty or not and if not, get access to the value inside. The idea is to make every maybe value be the function that chooses the correct one of two alternatives: “what to do if the container is empty,” and “what to do if the container has a value x”.

Thus we want the following behavior: in the same way that we pass to a boolean two expressions, a “when true” expression and a “when false” expression, we pass to a maybe two expressions, a “when nothing” expression for when the nothing is there, and a “when just” expression for when the expression contains something (and this “when just” expression will be passed the value being held). Thus, the rules are:

        ((Nothing       whenNothing) whenJust)  →*   whenNothing
        (((Just value)  whenNothing) whenJust)  →*   (whenJust value)

For example, if we have a maybe value, b, that might contain an integer or might be empty, the following expression means “if b is empty then give me 0; if it contains an integer $m$ then give me $m{+}1$”:

        ((b 0) (\m. (Succ m)))

Note that we are applying the maybe value b to the two possible actions; depending on whether the b was created from Nothing or from (Just a), it chooses the correct one of the two options.

Give definitions of Nothing and Just that behave as specified as above. Verify that ((Nothing x) y) reduces to x, and (((Just a) x) y) reduces to (y a).

Lists, revisited [10%]

In lab, we mentioned that there were other ways to define lists. Using what you have learned from encoding maybe values, encode lists, by defining Nil and Cons such that:

        ((Nil          whenNil) whenCons)  →*   whenNil
        ((((Cons h) t) whenNil) whenCons)  →*   ((whenCons h) t)

Also write IsEmpty, Head, and Tail. (What Head and Tail should do when used erroneously on an empty list is up to you, return anything you like or just assume such inputs won’t happen.)

Binary trees [10%]

Using what you have learned from encoding maybe types and lists, encode binary trees, such that:

        ((Leaf               whenLeaf) whenBranch)  →*   whenLeaf            
        (((((Branch v) l) r) whenLeaf) whenBranch)  →*   (((whenBranch v) l) r)

Non-recursive Fibonacci [10%]

We were very careful to define macros Plus, IsZero, Fst, and so on as simple abbreviations, so that one could replace them all by their definitions, obtaining a (much longer) term in the official $\lambda$-calculus syntax with just variables, functions, and applications.

Recursive definitions for functions to compute factorials or Fibonacci numbers would lead to illegal (circular) definitions that cannot be expanded away. The simplest way to handle this is by using fixed points and the Y combinator (as described in Wednesday’s class), but in many cases this is unnecessary.

Give a non-circular definition for a function Fib written without using Y or fixed points such that Fib n reduces to $F_n$ for all $n \geq 0$, where $F_n$ is the (Church numeral representing) the $n^{\mbox{th}}$ Fibonacci number. For reference, $F_0 = 0$; $F_1 = 1$, and $F_n = F_{n-1} + F_{n-2}$ for all $n \geq 2$.)

Hint: Use Pred from lab as your model. What sequence of pairs would be useful?

Recursion

Finally, let’s consider code that uses recursion in a more interesting way (i.e., where the number of iterations is not known ahead of time, so the Pred trick doesn’t work), namely the so-called “3n + 1” function. The idea is to start with a number and repeatedly: divide by 2 (if we have an even number) or multiply by 3 and add 1 (if we have an odd number). Empirically, it seems that if we start at any positive integer and repeatedly apply this procedure we will eventually reach 1 (e.g., 6, 3, 10, 5, 16, 8, 4, 2, 1) but no one has yet proved that it always happens.

  1. [20%] Give a definition for Step, a function that takes one step in the 3n+1 computation. That is, Step $n$ calculates $n/2$ if $n$ is even, and calculates $3n+1$ if $n$ is odd.

  2. [10%] Give a definition for Tnpo, the function that takes a number as input and returns how many times Step must be applied to it before we reach the answer 1. Thus, for example: Tnpo 1 should return 0, Tnpo 2 should return 1, and Tnpo 5 should return 5, and Tnpo 3 should return 7.

Note:

  • You should define and test some helper functions first before jumping into the definition of Step.

  • All correct and readable definitions get full credit. It is likely that your code will take many steps to run Tnpo on small inputs (like 5). Execution speed often depends on exactly how you wrote your code; the simplest definitions end up taking exponential time to run, due to order in which lc chooses to do $\beta$-reductions when it has a choice. Pred-style definitions tend be much more efficient than Y-style definitions, e.g., to compute the quotient and remainder when dividing by 2, but again, you’re not being graded on efficiency.

  • You will likely want to turn tracing off when testing any nontrivial input, unless you have specific debugging purposes in mind.

Part 2: Haskell

In preparation for Monday’s class, we will need to learn some basics about the Haskell programming language. Go through the on-line Haskell tutorial. It should take about an hour to watch the videos and do a few Haskell coding exercises. There’s nothing to turn in for this part, but when you finish you’ll get the secret code word. Bring it to Monday’s class.