CMPSC 461: Programming Language Concepts Assignment 1 Solution
Problem 1 [9pt] Add parentheses to the following lambda terms so that the grouping of sub-terms becomes explicit. For example, the term λx. x λy. y with parentheses is λx. (x (λy. y)).
a) (3pt)λx.λy.xyλz.xz
Solution: λx.λy. (x y) (λz. (x z))
b) (3pt)λx.λy.xλx.xyy
Solution: λx.λy. x (λx. ((x y) y))
c) (3pt)λx.xλy.xxy
Solution: λx. x λy. ((x x) y)
Problem 2 [6pt] For each of following terms, connect all bound variables to their definitions with lines. For example, the answer for λx. x x y should be λx. x x y.
a) (3pt)λx.yxλx.xy Solution: λx. y x λx. x y
b) (3pt)λy.λz.zyλy.x Solution: λy. λz. z y λy. x
Problem 3 [10pt] Fully evaluate the following λ-term so that no further β-reduction is possible. a) (5pt)((λxy.xy)(λx.y))u
Solution:
((λx y. x y) (λx. y)) u
= ((λx. (λy. x y)) (λx. y)) u
= ((λx. (λz. x z)) (λx. y)) u
= (λz. (λx. y) z) u
= (λx. y) u = y
(desugar term λx y. x)) (α − reduction) (β − reduction) (β − reduction) (β − reduction)
(β − reduction) (desugar term λy z. y) (α − reduction) (β − reduction)
b) (5pt) ((λx. x) (λy z. y)) z Solution:
((λx. x) (λy z. y)) z = (λy z. y) z
= (λy. (λz. y)) z
= (λy. (λu. y)) z
= λu. z
1/2
Problem 4 [9pt] Recall that under Church encoding, we have the following definitions: IF λb t f. b t f TRUE λt f. t FALSE λt f. f
a) (4pt) Fully evaluate (λx. (x y TRUE)) FALSE so that no further β-reduction is possible.. Solution:
(λx. (x y TRUE)) FALSE = (FALSE y TRUE)
= (λt f. f) y TRUE
= TRUE
(β − reduction) (definition of FALSE) (β − reduction)
b) (5pt) Show that (IF FALSE TRUE FALSE) = FALSE under such encoding. Solution:
(IF FALSE TRUE FALSE)
= (λb t f. b t f) FALSE TRUE FALSE = FALSE TRUE FALSE
= (λt f. f) TRUE FALSE
= FALSE
(definition of IF) (β − reduction) (definition of TRUE) (β − reduction)
Problem 5 [16pt] In the lecture, we have used the pure λ-calculus to construct natural numbers and encoded some operations on them. In such encoding, a number n is encoded as a function λf z. fn z (denoted as n). In this problem, we will define more useful operations on numbers. If you get stuck in any question, try to proceed by assuming the previous function is properly defined. You can reuse any encoding given in lectures and previous questions.
a) (4pt) Define a function ISZERO in λ-calculus, so that given a number n, it returns TRUE (the encoding of true) if n = 0; FALSE (the encoding of false) if n ̸= 0. Hint: try to define two terms so that applying the second term multiple times to the first term returns FALSE; otherwise, the application returns TRUE. Solution:
ISZERO λn. n (λf. FALSE) (TRUE)
b) (4pt)DefineafunctionPREDinλ-calculus,sothatgivenanumbern,thefunctionreturnsitspredecessor, assuming the predecessor of 0 is 0 Hint: follow the idea in Problem 4a. You might need to use PAIR. Solution:
PRED λn. RIGHT (n (λp. PAIR (SUCC (LEFT p)) (LEFT p)) (PAIR 0 0))
c) (4pt) Use your encoding of PRED to define a subtraction function MINUS, so that MINUS n1 n2 returns n1 − n2 when n1 ≥ n2, and 0 otherwise.
Solution:
MINUS λn1 n2. n2 PRED n1
d) (4pt)Recallthatinlecturenote2,wehavedefinedMULT(theencodingof×)basedonPLUS(theencoding of +): MULT λn1 n2. (n1 (PLUS n2) 0). Try to define MULT on Church numerals without using PLUS (replacing PLUS with an equivalent term under α/β reduction doesn’t count as a solution). Hint: by definition, we have n f = λz. fn z, which can be interpreted as repeating an arbitrary function f for n times to parameter z. The goal here is to repeat an arbitrary function f for n1 × n2 times (according to the definition of n1 × n2).
Solution:
MULT λn1 n2 f. (n2 (n1 f))
Assignment 1 Solution, Cmpsc 461 2020 Fall