Assignment 3: Derivation Trees and λ-calculus

Parameters:

  • Due date: Monday Sept 30, 11:59PM EST
  • Use the following code template: here
  • Upload a code.rkt solution to Gradescope. It will give you a score, but this is not your final score; some of the test cases will be kept private. You should test all your code thoroughly.
  • Upload a solution.pdf solution to Gradescope containing the derivation trees and inference rules you draw on paper.
  • Ask questions on Piazza or during office hours.
  • Perform all the work for this project by yourself. You may discuss with your classmates, but you must write your own code and solve your own exercises..

Problem 1: Derivation Trees for if-then-else

Recall the ite language from class:

;;; type expr =
;;;   | add of expr * expr
;;;   | mul of expr * expr
;;;   | num of number
;;;   | bool of bool
;;;   | ite of expr * expr * expr
(struct eadd (e1 e2) #:transparent)
(struct emul (e1 e2) #:transparent)
(struct enum (n) #:transparent)
(struct ebool (n) #:transparent)
(struct eite (guard thn els) #:transparent)


;;; type value =
;;;    | vnum of number
;;;    | vbool of bool
(struct vbool (b) #:transparent)
(struct vnum (n) #:transparent)

;;; to-num : value -> number
;;; converts a value to a number or raises a runtime error
(define (to-num v)
  (match v
    [(vnum n) n]
    [_ (error "runtime")]))

;;; to-num : value -> bool
;;; converts a value to a bool or raises a runtime error
(define (to-bool v)
  (match v
    [(vbool b) b]
    [_ (error "runtime")]))


;;; interp : expr -> value
;;; evaluates an expression to a value
(define (interp e)
  (match e
    [(eadd e1 e2)
     (let [(n1 (to-num (interp e1)))
           (n2 (to-num (interp e2)))]
       (vnum (+ n1 n2)))]
    [(emul e1 e2)
     (let [(n1 (to-num (interp e1)))
           (n2 (to-num (interp e2)))]
       (vnum (* n1 n2)))]
    [(ebool b) (vbool b)]
    [(eite guard thn els)
     (let [(vguard (to-bool (interp guard)))]
       (if vguard (interp thn) (interp els)))]
    [(enum n) (vnum n)]))

In this exercise you will be drawing derivation trees for this language.

Problem 1a [10 points]: Inference rules

First start off by defining the inference rules for the language that you will use for drawing the derivation trees.

Refer to the lecture notes 4 for an example of the inference rules for the let language.

Please draw the inference rules on a piece of paper, photograph it and then submit it with the rest of your assignment.

Problem 1b [10 points]: Derivation Trees

Using the inference rules you defined in the previous sub-problem, draw a derivation tree for the following programs:

    (interp
     (eite (ebool #t) (enum 10) (enum 20)))

    (interp
     (eite (ebool #f) (enum 30) (enum 20)))

    (interp
     (eite (ebool #f) (enum 30)
      (eadd (enum 20) (emul (enum 10) (enum 20)))))

Please draw your derivation trees on a piece of a paper, photograph it and submit it with the rest of your assignment.

Problem 2: $\lambda$s do grow on trees

Recall the inference rules for evaluating the $\lambda$-calculus:

\[\inferrule{E-LAM}{}{\abs{x}{e} \Downarrow \abs{x}{e}} \quad \inferrule{E-APP}{ e_1 \Downarrow \abs{x}{e_{\text{body}}} \quad e_{\text{arg}} \Downarrow v_{\text{arg}} \quad e_{\text{body}}[x \mapsto v_{\text{arg}}] \Downarrow v }{ (e_1 \app e_{\text{arg}}) \Downarrow v }\]

These inference rules can be used to draw derivation trees, which prove that a term evaluates to a particular value. For example, the following derivation tree proves that $(((\abs{x}{\abs{y}{y}}) \app (\abs{x}{\abs{y}{x}})) \app (\abs{x}{\abs{y}{y}}))$ evaluates to $\abs{x}{\abs{y}{y}}$:

\[\inferrule{E-APP}{ \inferrule{E-APP}{ \inferrule{E-LAM}{}{ \abs{x}{\abs{y}{y}} \Downarrow \abs{x}{\abs{y}{y}} }\quad \inferrule{E-LAM}{}{ \abs{x}{\abs{y}{x}} \Downarrow \abs{x}{\abs{y}{x}} }\quad \inferrule{E-LAM}{}{ (\abs{y}{y})[x \mapsto \abs{x}{\abs{y}{x}}] \Downarrow \abs{y}{y} } }{ ((\abs{x}{\abs{y}{y}}) \app (\abs{x}{\abs{y}{x}})) \Downarrow \abs{y}{y} }\quad \inferrule{E-LAM}{ }{ \abs{x}{\abs{y}{y}} \Downarrow \abs{x}{\abs{y}{y}} }\quad \inferrule{E-LAM}{ }{ y[y \mapsto \abs{x}{\abs{y}{y}}] \Downarrow \abs{x}{\abs{y}{y}} } }{ (((\abs{x}{\abs{y}{y}}) \app (\abs{x}{\abs{y}{x}})) \app (\abs{x}{\abs{y}{y}})) \Downarrow \abs{x}{\abs{y}{y}} }\]

Problem 2a [20 Points]: Church booleans

The booleans (true and false) can be represented in the λ-calculus using the Church encoding:

\[\begin{aligned} \text{true} & \equiv \abs{a}{\abs{b}{a}} \\ \text{false} & \equiv \abs{a}{\abs{b}{b}} \\ \text{not} & \equiv \abs{p}{\abs{a}{\abs{b}{((p \app b) \app a)}}} \\ \text{and} & \equiv \abs{p}{\abs{q}{((p \app q) \app p)}} \end{aligned}\]

  1. $\text{not} \app \text{true}$ is equivalent to $((\abs{p}{\abs{a}{\abs{b}{((p \app b) \app a)}}}) \app (\abs{a}{\abs{b}{a}}))$. Draw the derivation tree for:

    \[((\abs{p}{\abs{a}{\abs{b}{((p \app b) \app a)}}}) \app (\abs{a}{\abs{b}{a}})) \Downarrow \abs{a}{\abs{b}{(((\abs{a}{\abs{b}{a}}) \app b) \app a)}}\]

  2. OPTIONAL (no points): $\text{not} \app \text{true}$ should be equal to the lambda term for $\text{false}$, which is $\abs{a}{\abs{b}{b}}$. But this doesn’t exactly match the result from (a). Does this mean that our definition of $\text{not}$ is incorrect? Why or why not?

  3. $((\text{and} \app \text{true}) \app \text{false})$ is equivalent to $(((\abs{p}{\abs{q}{((p \app q) \app p)}}) \app (\abs{a}{\abs{b}{a}})) \app (\abs{a}{\abs{b}{b}}))$. Draw the derivation tree for:

    \[(((\abs{p}{\abs{q}{((p \app q) \app p)}}) \app (\abs{a}{\abs{b}{a}})) \app (\abs{a}{\abs{b}{b}})) \Downarrow \abs{a}{\abs{b}{b}}\]

    HINT: This tree is wide. You may want to turn the paper sideways.

Problem 2b [20 Points]: Church numerals

The natural numbers $0, 1, 2, \dots$ can also be represented in the λ-calculus using another Church encoding:

\[\begin{aligned} \text{zero} & \equiv \abs{f}{\abs{x}{x}} \\ \text{one} & \equiv \abs{f}{\abs{x}{(f \app x)}} \\ \text{succ} & \equiv \abs{n}{\abs{f}{\abs{x}{(f \app ((n \app f) \app x))}}} \end{aligned}\]

  1. $\text{succ}$ is the “successor” function, which computes the next number in the sequence by adding one. $(\text{succ} \app \text{zero})$ is equivalent to $((\abs{n}{\abs{f}{\abs{x}{(f \app ((n \app f) \app x))}}}) \app (\abs{f}{\abs{x}{x}}))$. First compute what this term evaluates to, then draw the derivation tree for it.

    HINT: Similar to problem 2a(1), $(\text{succ} \app \text{zero})$ doesn’t evaluate to exactly the same term as the definition of one above.

  2. Like everything in the $\lambda$-calculus, numbers are themselves functions that can be applied. For example, $((\text{one} \app \text{zero}) \app \text{zero})$ is equivalent to $(((\abs{f}{\abs{x}{(f \app x)}}) \app (\abs{f}{\abs{x}{x}})) \app (\abs{f}{\abs{x}{x}}))$. Compute what this term evaluates to and draw the derivation tree.

Problem 3 [40 Points]: Church encoding of the ITE language

Recall the definition of the if-then-else language

;;; type expr =
;;;   | add of expr * expr
;;;   | mul of expr * expr
;;;   | num of number
;;;   | bool of bool
;;;   | ite of expr * expr * expr
(struct eadd (e1 e2) #:transparent)
(struct emul (e1 e2) #:transparent)
(struct enum (n) #:transparent)
(struct ebool (n) #:transparent)
(struct eite (guard thn els) #:transparent)

In this exercise you will translate this language into lambda calculus. Recall the definition of lambda calculus from class.

;;; type lexpr =
;;;   | ident of string
;;;   | lam of string * lexpr
;;;   | app of lexpr * lexpr
(struct ident (s) #:transparent)
(struct lam (id body) #:transparent)
(struct app (e1 e2) #:transparent)

On this problem you will be compiling the if-then-else language into the lambda calculus; this process is called Church encoding. Your Church encoding should satisfy the following compiler correctness square (discussed in Lecture 6):

ITE prog --------------------> lambda calc prog 
   |          church encode           |
   |                                  |
   | interp-ite                       | iterp-lambda-calc
   |                                  |
   |                                  |
  \/         church encode           \/
ITE value -------------------> lambda calc value

This quare says that for all ITE programs prog, the following is always true:

(equivalent? (church-encode (interp-ite prog))
             (interp-lambda-calc (church-encode prog)))

Note however, you cannot rely on Racket’s built in equal? function because some lambda terms are extensionally equivalent that are not syntactically equivalent (see Lecture 6). So, to test your encodings, we have provided you with help functions run-church-bool-with-racket and run-church-num-with-racket. You can also use the compiler-square function to run a given ITE program both ways and it will return a boolean, showing whether the 2 ways return the same value.

> (run-church-num-with-racket 
    (church-encode (eite (ebool #t) 
                         (emul (enum 2) (eadd (enum 3) (enum 4)))
                         (enum 2)))) 
14
> (run-church-bool-with-racket (church-encode (ebool #t)))
#t
> (run-church-bool-with-racket (church-encode (ebool #f)))
#f

Here is the definitions for addition and multiplication with Church numerals, where m and n are the input Church numerals.

\[\begin{aligned} \text{add} & \equiv \abs{m}{\abs{n}{\abs{f}{\abs{x}{((m \app f) \app ((n \app f) \app x))}}}} \\ \text{multiply} & \equiv \abs{m}{\abs{n}{\abs{f}{\abs{x}{((m \app (n \app f)) \app x)}}}} \end{aligned}\]

Your task: implement the church-encode function with the following signature.

;;; church-encode: expr -> lexpr
;;; Translates a given expression from If-Then-Else language into lambda calculus
(define (church-encode expr)
  (error "implement me"))

Hint: before trying to implement anything, do some examples by hand so you understand how encoding work and operate. Use some identifiers like f and v to check that the result behaves as you expect it to. Additionally, some of the examples in Exercises 1 and 2 above are examples of Church encodings; write test cases for your church encoding function that handles these test cases.