CIS 425 Fall 2019 Assignment 2Lambda Calculus October 2019
Submission of assignments is optional. Submitted assignments will not be graded. If your solution differs from the posted solution, please submit it and indicate clearly why you think your solution is correct.
1 Multiple Choice Select the right answer:
x. y z and x. y z are equivalent 1. True
2. False
The term x.x a b is equivalent to which of the following?
1. x.x a b 2. x.x a b 3. x.x a b 4. x.x a b
x.yz can be betareduced to
1. y
2. y z
3. z
4. Cannot be reduced
Which of the following reduces to z.z
1. y.z.x z
2. z.x.z y
3. y.y x.z.z w 4. y.x.z z z.z
Which of the following expressions is equivalent to converts from x.y.x yy
1. y.y y 2. z.y z
1
CIS 425 Fall 2019 Assignment 2Lambda Calculus October 2019
3. x.z.x z y 4. x.y.x y z
reducing the following term produces what result? x.x y.y x y
1. y z.z y 2. z y.y z 3. y y.y y 4. y y
reducing the following term produces what result? x.y.y y w z
1. x.w w z
2. x.w z
3. w z
4. Does not reduce
2 Problems
1. Make all parentheses explicit in the following expressions
a x.x z y.x y
b x.x z y.w w.w y z x
c x.x y x.y x
2. Find all free unbound variables in the following expressions
a x.x z y.x y
b x.x z y.w x.w y z x
c x.x y x.y x
3. Give the result of performing the following substitutions:
a y.x yxx x.y x b x.x yxy.x x.x
2
CIS 425 Fall 2019 Assignment 2Lambda Calculus October 2019
4. Apply reduction to the following expressions as much as possible
a z.z y.y y x.x a b z.z z.z z z.z y
c x.y.x y y a.a b d x.y.x y y y.y y
e x.x x y.y x z f x. y. x y y z
g x.x x y.y y.y h x.y.x y y.y w
5. Show that the following expression has multiple reduction sequences x.y y.y y y x.x x x
6. Verify the following by applying the axiom:
a S K I I I, where S is x.y.z.x zy z, K is x.y.x, and I is x.x
b x.xxI I I
Note that, by convention, the lefthand side of part b reads as x.x x I I
3
3.1 Numbers
Lambda Calculus Encodings
Part of understanding a computational model is knowing its expressiveness: what range of programs can be written in the model? For example, in the language of arithmetic, we know that every program must evaluate to a value, i.e. it can never loop. While most normal programming languages permit partial functions functions that could return a result or loop forever, arithmetic is a language of total functions they always return a result.
Intuitively, this means that arithmetic is a less expressive than a more general programming language. the set of programs expressible in arithmetic is a strict subset of those expressible in, say Python or Java. What about the lambda calculus? It seems like such a simple language, but can we formally reason about its expressiveness? It turns out that the lambda calculus is equivalent in expressiveness to a Turing machine this result is called the Church Turing thesis. Both of these computational models can express computable functions. Informally, a computable function is a function on the natural numbers computable by a human being following an algorithm, ignoring resource limitations.
3
CIS 425 Fall 2019 Assignment 2Lambda Calculus October 2019
In the context of the lambda calculus, this idea will seem strange. If we only have variables and functions, how are we supposed to express something as simple as 2 2? The key idea is that we have to provide a mapping from constructs in the lambda calculus to natural numbers, which allows us to interpret the result of a lambda calculus program as a number. This is called a Church encoding after Alonzo Church, one of the founders of computer science and the inventor of the lambda calculus. In the remainder of this section, well work through a few exercises to understand how this works.
1. We will abbreviate Churchencoded natural numbers as n. For example, We can represent the first n numbers as follows:
0 x.y.y
1 x.y.x y
2 x.y.x x y
.
n x.y.xn y
Read xny as an abbreviation for xxxx x y , where x appears n times. With the above representation, we can define the successor function Succ as:
Succ u.x.y.x u x y. Show, by applying the axiom, that Succ n n 1, that is,
Succ x.y.xny x.y.xn1y.
2. Observe that for any Church numeral n, the lambda expression n f v corresponds to applyingf exactlyntimestov. So1f vf v,2f vf f vandsoon. Withthis in mind:
a Define a calculus term plus that adds Church numerals. That is, plus should have the property that:
plusm n mn
where denotes equivalence of calculus terms. You may want to use the
Succ function in your answer.
b Show that 2 1 3
c Define a calculus term mul that multiplies Church numerals.
4
CIS 425 Fall 2019 Assignment 2Lambda Calculus October 2019
3.2 Church Booleans
To introduce conditional logic, i.e ifsthenscomparisons, we need to use the Church encoding for booleans. Here, the idea is that true and false are functions which select a particular branch of two possibilities.
4
true a.b.a false a.b.b
not true false not false true
2. Define if such that
returns b if a true and returns c otherwise.
Coding Exercises
1. Translate the following code snippet written in Javascript to their equivalent in the calculus:
let x 1;
function gz return x z;
function fy
let x y 1;
return gy x;
f3; in other words what would calling f on 3 look like?
2. A programmer is having difficulty debugging the following C program. In theory, on an ideal machine with infinite memory, this program would run forever. In practice, this program crashes because it runs out of memory, since extra space is required every time a function call is made.
int fint g… g points to a function that returns an int
return gg;
int main
1. Define not such that
if a b c
5
Fall 2019
Assignment 2Lambda Calculus
int x;
x ff;
printfValue of x dn, x;
return 0;
CIS 425 October 2019
Explain the behavior of the program by translating the definition of f into lambda calculus and then reducing the application ff. This program assumes that the type checker does not check the types of arguments to functions.
3. Functions map and reduce are standard functions from traditional functional program ming that achieved broader recognition as a result of Googles MapReduce method for processing and generating large data sets. While map, reduce, and a number of related functions are provided in many JavaScript implementations, map and reduce can also be defined relatively simply in JavaScript as follows:
function map f, inarray
var out ;
forvar i 0; i inarray.length; i
out.push finarrayi
return out;
function reduce f, inarray
ifinarray.length 1 return;
ifinarray.length 2 return finarray0,inarray1;
r inarray0;
forvar li 1;li inarray.length;li
r fr, inarrayli;
return r;
Function mapf, inarray returns an array constructed by applying f to every element of inarray. Function reducef, inarray applies the function f of two arguments to elements in the list, from left to right, until it reduces the list to a single element. For example:
js map functionxreturn x1, 1,2,3,4,5
2,3,4,5,6
6
Fall 2019
Assignment 2Lambda Calculus
js reducefunctionx,yreturn xy, 1,2,3,4,5
15
js reducefunctionx,yreturn xy, 1,2,3,4,5
120
CIS 425 October 2019
These functions can be combined in various ways. For each of the following questions, you may use a JavaScript implementation to test your answer yourself, but turn your solution in as part of a written description for manual grading.
a Explain how to use map and reduce to compute the sum of the first five squares, in one line. The sum of the first three squares is 1 4 9
b Explain how to use map and reduce to count the number of positive numbers in an array of numbers.
c Explain how to use map andor reduce to flatten an array of arrays of numbers, such as 1, 2, 3, 4, 5, 6, 7, 8, 9, to an array of numbers. Hint: Look for builtin JavaScript concatenation functions.
7