Homework 4

Due Friday, Nov 8, 2019 at 8pm

A PDF version of this document is located here.

Use the following commands to download and unpack the distribution code:

$ wget https://eecs490.github.io/homework/hw4/starter-files.tar.gz
$ tar xzf starter-files.tar.gz

You may work alone or with a partner. Please see the syllabus for partnership rules. As a reminder, you may not share any part of your solution outside of your partnership. This includes code, test cases, and written solutions.

  1. Lambda calculus. For this question, you may use the symbol \(\lambda\) or the capital letter L to signify a \(\lambda\).

    1. Evaluate the \(\lambda\)-calculus term below until it is in normal form. You must follow the standard rules for normal-order evaluation. Show each \(\alpha\)-reduction and \(\beta\)-reduction step, as in the following:

      \begin{align*} &(\lambda x.~ x)~ (\lambda x.~ x)\\ \rightarrow~ &(\lambda x.~ x)~ (\lambda y.~ y)~ &(\alpha\textrm{-reduction})\\ \rightarrow~ &\lambda y.~ y~ &(\beta\textrm{-reduction}) \end{align*}

      In plain text:

      (L x. x) (L x. x)
      -> (L x. x) (L y. y)              (alpha-reduction)
      -> L y. y                         (beta-reduction)

      Term to evaluate:

      \begin{equation*} (\lambda x.~ \lambda y.~ x~ \lambda x.~ y~ x)~ (\lambda w.~ w)~ (\lambda x.~ x~ x)~ a \end{equation*}

      Hint: Evaluating this term requires a total of five \(\beta\)-reductions and one \(\alpha\)-reduction.

    2. The following function maps a pair containing numbers \((m, n)\) to a pair containing \((m+1, m)\):

      \begin{equation*} pairincr~ =~ \lambda p.~ pair~ (incr~ (first~ p))~ (first~ p) \end{equation*}

      Applying it to \(pair~ m~ n\) produces:

      \begin{align*} pairincr~ (pair~ m~ n)~ &=~ (\lambda p.~ pair~ (incr~ (first~ p))~ (first~ p))~ (pair~ m~ n)\\ &\rightarrow~ pair~ (incr~ (first~ (pair~ m~ n))~ (first~ (pair~ m~ n)))\\ &\rightarrow~ pair~ (incr~ m)~ (first~ (pair~ m~ n))\\ &\rightarrow~ pair~ (incr~ m)~ m \end{align*}

      Using \(pairincr\), define a \(decr\) function that decrements a Church numeral:

      \begin{equation*} decr~ =~ \lambda n.~ \textrm{[fill in your solution]} \end{equation*}

      Hint: What is the result when \(pairincr\) is applied to the pair \((0, 0)\)? What about when it is applied twice?

  2. Semantic equivalence. Write a transition rule in big-step operational semantics that specifies the evaluation of a let* form in Scheme in terms of let and let*. As an example, the expression

    (let* ((v1 e1) (v2 e2) (v3 e3)) body)

    is equivalent to

    (let ((v1 e1)) (let* ((v2 e2) (v3 e3)) body))

    Fill in the recursive rule below:

    \begin{equation*} \cfrac{}{\langle(\textbf{let*}~ ((v_1~ e_1)~ \dots~ (v_k~ e_k))~ body), \sigma\rangle \rightarrow~~~~~~~~~~~~~~}~~~ \textrm{if}~ k > 1 \end{equation*}

    Also fill in the rule for the base case:

    \begin{equation*} \cfrac{}{\langle(\textbf{let*}~ ((v~ e))~ body), \sigma\rangle \rightarrow~~~~~~~~~~~~~~} \end{equation*}

    For this question and Q2, you may write subscripts with or without a preceding underscore (e.g. v_1 or v1, and e_k or ek), and you may use the word sigma instead of \(\sigma\).

  3. Scope. Suppose we wanted to add the \(\bf let\) construct to the simple imperative language defined in lecture, with the following syntax:

    \begin{equation*} S ~\rightarrow~ \textbf{let}~ V~ =~ A~ \textbf{in}~ S~ \textbf{end} \end{equation*}

    The semantics of this construct are to execute the body \(S\) of the \(\bf let\) in the context of a state in which the result of evaluating the given expression \(A\) is bound to the variable \(V\). After the \(\bf let\) is executed, the variable should be restored to its previous value. Fill in the big-step transition rule describing this behavior below:

    \begin{equation*} \cfrac{}{\langle\textbf{let}~ v = a~ \textbf{in}~ s, \sigma\rangle \rightarrow~~~~~~~~~~~~~~} \end{equation*}
  4. Type systems and recursion. The language that we used to explore type systems does not have a direct mechanism for defining a recursive function. Suppose we wanted to add a \(\bf letrec\) construct, which is similar in structure to \(\bf let\):

    \begin{equation*} E ~\rightarrow~ (~ \textbf{letrec}~ V~ :~ T~ =~ E~ \textbf{in}~ E~ ) \end{equation*}

    A syntactic difference is that the variable must be explicitly typed in a \(\bf letrec\). Then if the initializer is a function abstraction, it is allowed to refer to itself by name in its body. For example, the following defines a factorial function:

    \begin{align*} &(\textbf{letrec}~ fact : Int \rightarrow Int =\\ &~~~~(\textbf{lambda}~ n : Int .~\\ &~~~~~~~~(\textbf{if}~ (n <= 0)~ \textbf{then}~ 1~ \textbf{else}~ (n * (fact~ (n - 1))))\\ &~~~~)\\ &~~~~\textbf{in}~ (fact~ 5)\\ &) \end{align*}

    Fill in the following typing rule for the \(\bf letrec\) construct:

    \begin{equation*} \cfrac{ }{ \Gamma ~\vdash~ (\textbf{letrec}~ v : T_1 = t_1~ \textbf{in}~ t_2) ~:~ ~~~~~~~~~~~~~~ } \end{equation*}

    For this question, you may write subscripts with or without a preceding underscore (e.g. t_1 or t1), and you may use the word Gamma and the symbols |- instead of \(\Gamma\) and \(\vdash\).

  5. Vtables. Consider the following C++ code:

    struct A {
      void foo() {
        cout << "A::foo()" << endl;
      virtual void bar() {
        cout << "A::bar()" << endl;
    struct B : A {
      virtual void foo() {
        cout << "B::foo()" << endl;
      void bar() {
        cout << "B::bar()" << endl;
    int main() {
      A *aptr = new B;

    This code prints the following when run:

    1. Draw the vtables for A and B.
    2. Briefly explain how the compiler translates the method calls in main().
  6. Dispatch dictionaries and inheritance. In the course notes, we saw a definition of a bank account ADT using functions and dispatch dictionaries. The following is a version of this ADT using built-in Python dictionaries:

    def account(initial_balance):
        def deposit(amount):
            new_balance = dispatch['balance'] + amount
            dispatch['balance'] = new_balance
            return new_balance
        def withdraw(amount):
            balance = dispatch['balance']
            if amount > balance:
                return 'Insufficient funds'
            balance -= amount
            dispatch['balance'] = balance
            return balance
        def get_balance():
            return dispatch['balance']
        dispatch = {}
        dispatch['balance'] = initial_balance
        dispatch['deposit'] = deposit
        dispatch['withdraw'] = withdraw
        dispatch['get_balance'] = get_balance
        def dispatch_message(message):
            return dispatch[message]
        return dispatch_message

    Implement an ADT for a checking account that is a derived version of a bank account but charges a $1 fee for withdrawal. Fill in the ADT definition for checking_account() in the hw4.py file.

    Do not repeat code from account(). Instead, implement a scheme for deferring to account() where possible.


Place your solution to question 6 in the provided hw4.py file. Write your answers to questions 1-5 in a PDF file named hw4.pdf. Submit hw4.py to the autograder before the deadline. Submit hw4.pdf to Gradescope before the deadline. Be sure to register your partnership on the autograder and Gradescope if you are working with a partner.