Homework 4

Due Friday, Nov 8, 2019 at 8pm

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

$ wget https://amirkamil.github.io/eecs490/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 \Downarrow~~~~~~~~~~~~~~}~~~ \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 \Downarrow~~~~~~~~~~~~~~} \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~ \textbf{end}, \sigma\rangle \Downarrow~~~~~~~~~~~~~~} \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;
     aptr->foo();
     aptr->bar();
   }
   

   This code prints the following when run:

   A::foo()
   B::bar()
   

   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.