Deriving Static Properties of Variables through Syntactic Analysis

• Distinguish static vs. dynamic properties of a program.
  First example of syntactic analysis of a program (viewed as a data).
• Syntax of Lambda calculus:

  <exp> ::= <varref>
          | (lambda (<var>) <exp>)
          | (<exp> <exp>)
  

• Free vs. bound variables:
  variable is bound in an expression if it refers to a formal parameter introduced in the expression.
• Definition:
  A variable x occurs free in an expression E if and only if:
  • E is a variable reference and E is the same as x; or
  • E is of the form (E1 E2) and x occurs free in E1 or E2; or
  • E is of the form (lambda (y) E'), where y is different from x and x occurs free in E'.

  (define varref? symbol?)
  (define vardecl? symbol?)
  (define application? (lambda (e) (and (list? e) (= (length e) 2))))
  (define lambda? 
    (lambda (e) (and (list? e)
                     (= (length e) 3)
                     (eq? (car e) 'lambda)
                     (list? (second e))
                     (= (length (second e)) 1)
                     (vardecl? (car (second e))))))
  (define operator car)
  (define operand cadr)
  (define var caadr)
  (define body caddr)
  
  (define free-vars 
    (lambda (exp)
      (cond ((varref? exp) (list exp))
            ((application? exp)
             (let ((e1 (operator exp))
                   (e2 (operand exp)))
               (union (free-vars e1) (free-vars e2))))
            ((lambda? exp)
             (let ((var (var exp))
                   (body (body exp)))
               (remove var (free-vars body)))))))
  

• Scope:
  Scope of a variable declaration = Region in which references to the variable refer to the declaration. In lexically scoped languages, scope can be determined statically (by inspection of code of program).
• Holes in the scope of a variable:
  

  > (define x
     (lambda (x)
       (map (lambda (x) (+ x 1)) x)))
  > (x '(1 2 3))
  (2 3 4)
  

• Lexical Address of a variable:
  Definition:
  • Depth of a varref: how many "contours" (lambda expressions) are crossed from varref to its declaration (as an arg in a lambda).
  • Position: if allow more than one var per lambda, position of var within its binding lambda-list (starts at 0).
  The pair (depth, position) is sufficient to link any varref to its declaration. Note a varref as (v : d p).

  (lambda (x y)
    ((lambda (a)
       (x (a y)))
    x))
  
  (lambda (x y)
    ((lambda (a)
       ((x : 1 0) ((a : 0 0) (y : 1 1))))
     (x : 0 0)))
  

  In fact, names of variables are not needed!

  (lambda 2
    ((lambda 1
       ((: 1 0) ((: 0 0) (: 1 1))))
     (: 0 0)))
  

  Note that the following expression is impossible:

  (lambda (a)
    (lambda (a)
      (a : 1 0)))
  

• Alpha-conversion: Renaming Variables, Name Capture
  Since names of variables are not necessary, can replace them. (lambda (x) x) is always the same function whatever name is used for x. General program transformation: rename formal parameters. But must be careful of 2 problems:
  • Do not use as a new name the name of a free variable in the body of the lambda expression:

      (lambda (x) (cons x '()))
      

    is different from:

      (lambda (cons) (cons cons '()))
      

  • Second problem is when dealing with holes in the scope of the replaced variable:

      (lambda (x)
        ((lambda (x) (cons x '()))
         (cons x '())))
      

    may be transformed to:

      (lambda (y)
        ((lambda (x) (cons x '()))   ;; KEEP x in the body
         (cons y '())))
      

    but should NOT be transformed to:

      (lambda (y)
        ((lambda (x) (cons y '()))
         (cons y '())))
      

  Proper definition of alpha-conversion:
  exp[y/x]: exp with y for x. Replace all free occurrences of variable x with variable y.

  (lambda (var) exp) == (lambda (var') exp[var'/var])