►C311/  H311/  A596 Spring 2025 – Programming Languages
▼Assignments
•3 Assignment 3:   Variables
    contents  ← prev  up  next → 

3 Assignment 3: Variables

There may, indeed, be other applications of the system than its use as a logic.

——Alonzo Church, writing about the lambda calculus in 1932

Guidelines for this assignment
Assignment
Part 1: Natural Recursion Refresher

Recall this grammar of natural numbers:
  NaturalNumber = 0
  | (+ 1 NaturalNumber)

  1. Consider the following partial definition of the list-ref function. It is intended to operate similarly to Racket’s list-ref. The input n is a zero-based index. Therefore, the input is bad data if n is greater than or equal to the length of ls.

    (define list-ref
      (lambda (ls n)
        (letrec
          ([nth-cdr (lambda (n)
                      ;; complete the definition
                      )])
          (car (nth-cdr n)))))

    The body of the function that is the right-hand side of nth-cdr is missing. Complete the definition of list-ref with a naturally recursive implementation of nth-cdr, so that the following work correctly. You should not need to modify the provided code beyond completing the function body containing a comment.

    > (list-ref '(a b c) 2)
    'c
    > (list-ref '(a b c) 0)
    'a

    Remember, you need not consider bad data in your definition.

Part 2: Free and Bound Variables

The lambda calculus can be thought of as a tiny subset of Scheme. It only has three kinds of expressions:

  • variables

  • lambda expressions that take exactly one argument and have exactly one body

  • applications of one expression to another

In other words, below is the grammar of lambda-calculus expressions:
  Lambda-Exp = Symbol
  | (lambda (Symbol) Lambda-Exp)
  | (Lambda-Exp Lambda-Exp)
Unless otherwise stated, you must use match in each of the remaining problems. The brainteasers might be easier with it as well. For the most part, you should expect to be performing natural recursion on lambda-calculus expressions. You should only need the features of match demonstrated in class.

  1. Redefine and test the below procedure lambda-exp? that takes a value E and returns #f (false) if the input lambda-expression is not well formed, i.e. it contains bad data. Otherwise it returns #t (true).

    (define lambda-exp?
      (λ (E)
        (letrec
          ([p
            (λ (e)
              (match e
                [`,y #t]
                [`(lambda (,x) ,body) (p body)]
                [`(,rator ,rand . ,more) (or (p rator) (p rand))]
                [else #f]))])
          (p E))))
    Unfortunately, the above program doesn’t meet these expectations. Fix it so it does.

    > (lambda-exp? 'x)
    #t
    > (lambda-exp? '(lambda (x) x))
    #t
    > (lambda-exp? '(lambda (f) (lambda (x) (f (x x)))))
    #t
    > (lambda-exp? '(lambda (x) (lambda (y) (y x))))
    #t
    > (lambda-exp? '(lambda (z) ((lambda (y) (a z)) (h (lambda (x) (h a))))))
    #t
    > (lambda-exp? '(lambda (lambda) lambda))
    #t
    > (lambda-exp? '((lambda (lambda) lambda) (lambda (y) y)))
    #t
    > (lambda-exp? '((lambda (x) x) (lambda (x) x)))
    #t
    > (lambda-exp? '((lambda (5) x) (lambda (x) x)))
    #f
    > (lambda-exp? '((lambda (x) x) (lambda (x) x) (lambda (x) x)))
    #f
    > (lambda-exp? '((lambda (lambda (x) x) x)  (lambda (x) x)))
    #f

  2. Define and test a procedure var-occurs? that takes a variable name and a lambda-calculus expression and returns a boolean answering whether that variable occurs in the expression. Here and forevermore in this class we use the word “occur” in its technical sense: for us, a place where a variable is bound (also known as the formal) does not count as a variable occurrence.

    > (var-occurs? 'x 'x)
    #t
    > (var-occurs? 'x '(lambda (x) y))
    #f
    > (var-occurs? 'x '(lambda (y) x))
    #t
    > (var-occurs? 'x '((z y) x))
    #t

  3. Define and test a procedure vars that takes a lambda-calculus expression and returns a list containing all variables that occur in the expression. This should be a straightforward modification of the fixed-up lambda-exp? in question 2. The order of the variables in your answer does not matter.

    > (vars 'x)
    (x)
    > (vars '(lambda (x) x))
    (x)
    > (vars '((lambda (y) (x x)) (x y)))
    (x x x y)
    > (vars '(lambda (z) ((lambda (y) (a z))
                          (h (lambda (x) (h a))))))
    (a z h h a)

  4. Define and test a modification of vars called unique-vars that behaves like vars but does not return duplicates. It may help you to review how you implemented the function sparse-natset-union in Assignment 2: Representation Independence.

    > (unique-vars '((lambda (y) (x x)) (x y)))
    (x y)
    > (unique-vars '((lambda (z) (lambda (y) (z y))) x))
    (z y x)
    > (unique-vars '((lambda (a) (a b)) ((lambda (c) (a c)) (b a))))
    (c b a)

  5. Define and test a procedure var-occurs-free? that takes a symbol and a lambda-calculus expression and returns #t if that variable occurs free in that expression, and #f otherwise.

    > (var-occurs-free? 'x 'x)
    #t
    > (var-occurs-free? 'x '(lambda (y) y))
    #f
    > (var-occurs-free? 'x '(lambda (x) (x y)))
    #f
    > (var-occurs-free? 'x '(lambda (x) (lambda (x) x)))
    #f
    > (var-occurs-free? 'y '(lambda (x) (x y)))
    #t
    > (var-occurs-free? 'y '((lambda (y) (x y)) (lambda (x) (x y))))
    #t
    > (var-occurs-free? 'x '((lambda (x) (x x)) (x x)))
    #t

  6. Define and test a procedure var-occurs-bound? that takes a symbol and a lambda-calculus expression and returns #t if that variable occurs bound in the expression, and #f otherwise.

    > (var-occurs-bound? 'x 'x)
    #f
    > (var-occurs-bound? 'x '(lambda (x) x))
    #t
    > (var-occurs-bound? 'y '(lambda (x) x))
    #f
    > (var-occurs-bound? 'x '((lambda (x) (x x)) (x x)))
    #t
    > (var-occurs-bound? 'z '(lambda (y) (lambda (x) (y z))))
    #f
    > (var-occurs-bound? 'z '(lambda (y) (lambda (z) (y z))))
    #t
    > (var-occurs-bound? 'x '(lambda (x) y))
    #f
    > (var-occurs-bound? 'x '(lambda (x) (lambda (x) x)))
    #t

  7. Define and test a procedure unique-free-vars that takes a lambda-calculus expression and returns a list of all the variables that occur free in that expression. Order doesn’t matter, but the list must not contain duplicate variables. You may find it helpful to use the definition of unique-vars from question 5 as a starting point.

    > (unique-free-vars 'x)
    (x)
    > (unique-free-vars '(lambda (x) (x y)))
    (y)
    > (unique-free-vars '((lambda (x) ((x y) e)) (lambda (c) (x (lambda (x) (x (e c)))))))
    (y e x)

    Note that in the third example above,

    ((lambda (x) ((x y) e)) (lambda (c) (x (lambda (x) (x (e c))))))

    is a single lambda-calculus expression (a procedure application), not a list of lambda-calculus expressions.

  8. Define and test a procedure unique-bound-vars that takes a lambda-calculus expression and returns a list of all the variables that occur bound in the input expression. Order doesn’t matter, but the list must not contain duplicate variables.

    > (unique-bound-vars 'x)
    ()
    > (unique-bound-vars '(lambda (x) y))
    ()
    > (unique-bound-vars '(lambda (x) (x y)))
    (x)
    > (unique-bound-vars '((lambda (x) ((x y) e)) (lambda (c) (x (lambda (x) (x (e c)))))))
    (x c)
    > (unique-bound-vars '(lambda (y) y))
    (y)
    > (unique-bound-vars '(lambda (x) (y z)))
    ()
    > (unique-bound-vars '(lambda (x) (lambda (x) x)))
    (x)
Part 3: Lexical Addressing

In class, we introduced an arithmetic language with local variables:
  Expr = Number
  | (add Expr Expr)
  | (sub Expr Expr)
  | Symbol
  | (local Symbol Expr Expr)
We also showed how to represent variables by de Bruijn indices:
  DeBruijn = Number
  | (add DeBruijn DeBruijn)
  | (sub DeBruijn DeBruijn)
  | (var NaturalNumber)
  | (local DeBruijn DeBruijn)
We related these two grammars by defining a compiler lex that compiled Expr to DeBruijn.

  1. Define an interpreter for DeBruijn expressions. Specifically, define a function value-de-bruijn that takes a DeBruijn expression and a list of numbers and returns the value of the given expression.
    > (value-de-bruijn '(add 10 (local (add 1 1) (sub 5 (var 0)))) '())
    13
    > (value-de-bruijn '(add 10 (local 5 (local (add 1 1) (sub (var 1) (var 0))))) '())
    13
    > (value-de-bruijn '(add 10 (local 1 (local (add (var 0) (var 0)) (sub 5 (var 0))))) '())
    13
    The input list is an accumulator that starts as the empty list. It can be thought of as the environment because it provides the values of the free variables of the given expression:
    > (value-de-bruijn '(var 0) '(10 11 12 13 14))
    10
    > (value-de-bruijn '(var 1) '(10 11 12 13 14))
    11
    > (value-de-bruijn '(var 2) '(10 11 12 13 14))
    12
    The goal is to provide a second way to run an Expr E, namely, the value produced by (value-of E environments (empty-env)) should also be produced by (value-de-bruijn (lex E) '()).

    Define this function value-de-bruijn by natural recursion on the input expression.

Let’s turn from our arithmetic language back to the lambda calculus. As in the previous section, we restrict our lambdas to have only one argument. The lexical address (or de Bruijn index) of a variable occurrence is the number of lambdas between the place where the variable is bound (also known as the formal) and the place where it occurs. For example, in the following expression:
(lambda (x)
  (lambda (o)
    (lambda (r)
      (lambda (s)
        (lambda (p)
          (lambda (g)
            o))))))
The o at the very bottom is a bound occurrence. Its lexical address is 4, because there are four lambda expressions between the formal o near the top and the occurrence of o at the bottom.

  1. Below is the grammar of lexically-addressed lambda-calculus expressions:
      Lambda-deBruijn = Symbol
      | (var NaturalNumber)
      | (lambda Lambda-deBruijn)
      | (Lambda-deBruijn Lambda-deBruijn)
    Define and test a procedure lambda-lex that takes a Lambda-Exp and an accumulator (which starts as the empty list), and returns the same expression as a Lambda-deBruijn. Replace each bound variable occurrence by a list of two elements: the symbol var followed by the lexical address of the variable. Leave free variables as is; that is why the first line of the grammar above still allows a Symbol alone to constitute a Lambda-deBruijn.

    > (lambda-lex '(lambda (x) x)
                  '())
    (lambda (var 0))
    > (lambda-lex '(lambda (y) (lambda (x) y))
                  '())
    (lambda (lambda (var 1)))
    > (lambda-lex '(lambda (y) (lambda (x) (x y)))
                  '())
    (lambda (lambda ((var 0) (var 1))))
    > (lambda-lex '(lambda (x) (lambda (x) (x x)))
                  '())
    (lambda (lambda ((var 0) (var 0))))
    > (lambda-lex '(lambda (x) (lambda (x) (y x)))
                  '())
    (lambda (lambda (y (var 0))))
    > (lambda-lex '(lambda (y) ((lambda (x) (x y)) (lambda (c) (lambda (d) (y c)))))
                  '())
    (lambda ((lambda ((var 0) (var 1))) (lambda (lambda ((var 2) (var 1))))))
    > (lambda-lex '(lambda (a)
                     (lambda (b)
                       (lambda (c)
                         (lambda (a)
                           (lambda (b)
                             (lambda (d)
                               (lambda (a)
                                 (lambda (e)
                                   (((((a b) c) d) e) a)))))))))
                  '())
    (lambda
      (lambda
        (lambda
          (lambda
            (lambda
              (lambda
                (lambda
                  (lambda
                    ((((((var 1) (var 3)) (var 5)) (var 2)) (var 0)) (var 1))))))))))
    > (lambda-lex '(lambda (a)
                     (lambda (b)
                   (lambda (c)
                     (lambda (w)
                       (lambda (x)
                     (lambda (y)
                       ((lambda (a)
                          (lambda (b)
                        (lambda (c)
                          (((((a b) c) w) x) y))))
                        (lambda (w)
                          (lambda (x)
                        (lambda (y)
                          (((((a b) c) w) x) y)))))))))))
                  '())
    (lambda
      (lambda
        (lambda
          (lambda
            (lambda
          (lambda
            ((lambda
               (lambda
                 (lambda
                   ((((((var 2) (var 1)) (var 0)) (var 5)) (var 4)) (var 3)))))
             (lambda
               (lambda
             (lambda
               ((((((var 8) (var 7)) (var 6)) (var 2)) (var 1)) (var 0))))))))))))
    > (lambda-lex '(lambda (a)
                     (lambda (b)
                   (lambda (c)
                     (lambda (w)
                       (lambda (x)
                     (lambda (y)
                       ((lambda (a)
                          (lambda (b)
                        (lambda (c)
                          (((((a b) c) w) x) y))))
                        (lambda (w)
                          (lambda (x)
                        (lambda (y)
                          (((((a b) c) w) h) y)))))))))))
                  '())
    '(lambda
       (lambda
         (lambda
           (lambda
             (lambda
               (lambda
                 ((lambda
                    (lambda
                      (lambda ((((((var 2) (var 1)) (var 0)) (var 5)) (var 4)) (var 3)))))
                  (lambda
                    (lambda
                      (lambda ((((((var 8) (var 7)) (var 6)) (var 2)) h) (var 0))))))))))))

    There are a number of ways you can approach this problem. Our suggestion is to build some lambda expressions with pen and paper, and then by hand find the lexical addresses of some variables that occur in them. Try and do it almost mechanically, starting from the body of the innermost lambda of the expression and working your way out. If there is more than one innermost lambda, pick one, resolve it and repeat. Then think about what it is you’re doing, and figure out how to do it without having to go back up the tree. That is, ensure that when you get to a variable position in the expression where you need to fill in the lexical address, that you already have all the information you need to figure it out.

Brainteasers

  1. Define a compiler from DeBruijn back to Expr. Specifically, define a function unlex that takes a DeBruijn expression and two lists of symbols and returns the equivalent Expr expression.
    > (unlex '(add 10 (local (add 1 1) (sub 5 (var 0))))
             '(J K L)
             '())
    (add 10 (local J (add 1 1) (sub 5 J)))
    > (unlex '(add 10 (local 5 (local (add 1 1) (sub (var 1) (var 0)))))
             '(V J K)
             '())
    (add 10 (local V 5 (local J (add 1 1) (sub V J))))
    > (unlex '(add 10 (local 1 (local (add (var 0) (var 0)) (sub 5 (var 0)))))
             '(I J K)
             '())
    (add 10 (local I 1 (local J (add I I) (sub 5 J))))
    The first input list is an accumulator that supplies the variable names in the output, starting with the variable name that the outermost locals should bind. If this list contains duplicates, or is too short (in other words, supplies fewer names than there are nested levels of local in the input), then it is bad data and need not be considered in your definition.
    > (unlex '(add (local 2 (local 3 (sub (var 0) (var 1))))
                   (local 5 (local 7 (sub (var 0) (var 1)))))
             '(x y z)
             '())
    (add (local x 2 (local y 3 (sub y x)))
         (local x 5 (local y 7 (sub y x))))
    The second input list is an accumulator that starts as the empty list. It provides the names of the free variables of the given expression:
    > (unlex '(var 0) '(x y z) '(a b c d))
    a
    > (unlex '(var 1) '(x y z) '(a b c d))
    b
    > (unlex '(var 2) '(x y z) '(a b c d))
    c

  2. Consider the function e1=e2? defined below:
    (define e1=e2?
      (lambda (e1 e2)
        (equal? (lambda-lex e1 '()) (lambda-lex e2 '()))))
    This function determines whether two lambda-calculus expressions are equivalent up to variable renaming:
    > (e1=e2? '(lambda (x) x) '(lambda (y) y))
    #t
    > (e1=e2? '(lambda (z) x) '(lambda (z) y))
    #f
    > (e1=e2? '(lambda (x) (lambda (y) (x y))) '(lambda (x) (lambda (z) (x z))))
    #t
    > (e1=e2? '(lambda (x) (lambda (y) (x y))) '(lambda (x) (lambda (x) (x x))))
    #f
    Unfortunately, this function works by producing intermediate results using lambda-lex. If e1 and e2 are big and obviously different—for instance, if e1 is a big lambda but e2 is a big application—then it is wasteful to produce these intermediate results.

    Let’s reduce this waste. Define e1=e2? without using lambda-lex, but by natural recursion on the inputs e1 and e2. The input-output behavior of e1=e2? should stay the same, so the tests above should still pass. Moreover, if (say) e1 is a lambda and e2 is an application, then the function should return #f immediately, without inspecting e1 or e2 any further. To track which variable names in e1 correspond to which variable names in e2, you should introduce an accumulator (which starts as the empty list) or two.

Just Dessert

  1. A variable can both occur free and occur bound in the same expression. Define a predicate var-occurs-both? that takes a variable and a lambda-calculus expression, and returns two values: first a boolean indicating whether the variable occurs free in the expression, then a boolean indicating whether the variable occurs bound in the expression. Your solution should be a one-pass solution, meaning you should not recur over the same data twice, and you should not use an accumulator. In order to return two values, pack them up into a cons pair.
    > (var-occurs-both? 'x '(lambda (x) (x (lambda (x) x))))
    (#f . #t)
    > (var-occurs-both? 'x '(x (lambda (x) x)))
    (#t . #t)
    > (var-occurs-both? 'x '(lambda (y) (x (lambda (x) x))))
    (#t . #t)
    > (var-occurs-both? 'x '(lambda (x) (lambda (x) (x (lambda (x) x)))))
    (#f . #t)
    > (var-occurs-both? 'x '(lambda (x) (lambda (y) (lambda (x) (x (lambda (x) x))))))
    (#f . #t)
    > (var-occurs-both? 'x '(lambda (y) (lambda (x) (lambda (z) (lambda (x) (x (lambda (x) x)))))))
    (#f . #t)

    contents  ← prev  up  next →