LAMP: Exercise 2 Untyped Lambda-Calculus

Exercise 2 Untyped Lambda-Calculus

English only

This page has been updated with sections Tips and Partial Solution.

Food for thought has been moved to the main course page.

The parial implementation had a bug in EvaluatorPhase::isNumericVal (the solution fixed it). Sorry.

This page is best viewed with Mozilla Firefox or any other browser that displays Unicode math symbols correctly. The symbol ⊢ should look roughly like |-.

Administrative Issue:

Please register in groups of two during this session.

Emacs is installed now! set the environment variable HOME to your home directory, and create a _emacs file there with these lines

(setq load-path 
      (cons 
         (expand-file-name "C:/Program Files/Scala/support/emacs") 
         load-path)
)
(require 'scala-mode)
(require 'scala-mode-auto)
(global-font-lock-mode 1)   ;; syntax highlighting
(transient-mark-mode t)     ;; highlight the active (selected) region

Exercise 2 (untyped) Lambda Calculus

This exercise aims to test and deepen your understanding of the lambda calculus. For this, the lambda calculus is extended with arithmetic expressions that we have seen last week. The terms E are arithmetic expressions and lambda expressions (variables x, abstraction \x.E and application E E. An abstraction \x.E binds the variable x.

Some of these terms can be considered values (meaningful results of computation). These are arithmetic values (BV and NV) and lambda abstractions. Since lambda abstractions are anonymous functions, that means functions are first-class values.

By convention, application is left associative and the body of lambda abstractions extends as far to the right as possible. Parentheses can be used to group terms.

Computation in call-by-value lambda calculus is call-by-value beta reduction combined with corresponding congruence rules. We keep the reduction rules for arithmetic expressions from last week. Only the if is a bit more general, it works for any pair of lambda terms E1 and E2, not just for arithmetic ones.

E ::= x   
      E E 
      \x.E
      true
      false
      zero
      succ E
      pred E
      iszero E
      if E then E else E

V ::=  BV
       NV
       \x.E 

BV ::= true   
       false

NV ::= zero   
       succ NV

Computation

Congruence

 
(\x.E) V → [x/V]E
 

 
if true  then E1 else E2 → E1

 
if false then E1 else E2 → E2

 
isZero zero     → true

 
isZero succ NV  → false

 
pred zero → zero

 
pred succ NV → NV

E1 → E1'

E1 E2 → E1' E2

E2 → E2'

V E2 → V E2'

E → E'

if E then E1 else E2 → if E' then E1 else E2

E → E'

isZero E → isZero E'

E → E'

pred E → pred E'

E → E'

succ E → succ E'

[x / V]E means substitution modulo renaming of bound variables. All occurrences of x are replaced with V, and we check that the bound variables in E are different from free variables in V. This can be very costly to check!

Renaming can be avoided using a nameless representation for terms. The idea is to replaces name references by "structural references" (a number that indicates how much lambdas we have to go up).

Substitution then means replacing a number j with a term s in t, which is written [j / s]t. Such structural reference have to be maintained during substitution. This happens with an operation called shift.

If E contains abstractions, the numbers that point to outer abstractions need to be shifted in order to preserve the meaning. But references that point to abstractions inside s may not be shifted however. For this the shifting function has a cutoff parameter c.

With the help of shift, substitution on de Bruijn terms is then defined as

                      k   if k < c
shift(c, d, k)     ={ 
                      k+d if k >= c

shift(c, d, \.t)   = \.shift(c+1, d, t)

shift(c, d, t1 t2) = (shift(c,d,t1) shift(c,d,t2))

                       s   if k == j
[j / s] k        = { 
                       k   otherwise

[j / s] \.t     = \.[j+1 / shift(0,1,s)] t

[j / s] \.t1 t2) = (([j / s] t1) ([j / s] t2))

Task 2.1 (from TAPL page 67)

Write down the nameless representations for these terms (you can keep the names in the abstractions).

\s.\z.z
\s.\z.s (s z)
\m.\n.\s.\z.m s (n s)
\f.\x.f (\y. x x y) (\y. x x y)
(\x.(\x.x)) (\x.x)

Task 2.2 From named terms to de Bruijn terms...

Write a program that does this mechanical translation. Download and unpack the partial implementation and complete DeBruijnPhase.

source -- Parser --> term with RawVar -- DeBruijnPhase --> term with Var

Use the class Context to represent naming contexts. A naming context is like list of strings (we will see next week, why it is clever to have Context that implements the Scala Map interface instead of just using a list). Here are its methods

update returns a new context with the name given as argument added.
indexOf returns the index of a name in this context
length the length of the context
lookup to find the i-th element of the context
fresh which returns a fresh name (different from all names in the context) and a new context in which this name is bound

In src/lamba/Expr.scala you find new definitions for Var,Lam,App,RawVar. In lambda abstractions Lam, names of bound variables will be kept as debugging info. Also for debugging, you should store the context length in Var.

You can compile with

scalac -d classes src\lambda\*.scala

You can test with

scala lambda.Main -deBruijn <sourcefile1> <sourcefile2> ...

Some test files with the extension ".lam" can be found in the directory test.

Task 2.3 ...and back

With the help of the debugging information (the names in the abstractions), we can get back to terms with names. Implement method toString(ctx: Context) in class Expr. Test with

scala lambda.Main -deBruijn -print <sourcefile1> <sourcefile2> ...

Task 2.4 Call-By-Value Evaluator

Complete all missing methods in Evaluator to obtain a call-by-value evaluator for lambda terms. Test with

scala lambda.Main <sourcefile1> <sourcefile2> ...

Run some tests. If you are convinced that it works, try to evaluate breakCallByValue.lam.

Task 2.5 Call-By-Name Evaluator

You have seen the call-by-name evaluation strategy. Here are the rules: we reduce an application of a lambda abstraction even though the argument is not necessarily value. The congruence rule needs to be adapted in order to keep the strategy deterministic.

 
(\x.E1) E2 → [x/E2]E1
 

E1 → E1'

E1 E2 → E1' E2

E2 → E2'     V ≠ \x.E

V E2 → V E2'

Which line do you have to change in your implementation to get call-by-name evalution? What behaviour can be observed when running call-by-name on the file breakCallByValue.lam

Tips

The class Context is a subtype of scala.collection.immutable.ListMap[String,Binding]. It is an immutable map, that means update does not modify the existing object, but return a new one.

>val x = new Context();           // x is an empty map
>val y = x.update("A", NameBind); // y is a map { A -> NameBind }
>y("A")
NameBind
>x("A");                          // x is not modified
error: key not found

Apart from applying a context ctx, one can also make a get:

>def f(y:Context) = {  // y is a context
>y.get("B").match {
  case Some(z) => ...//y contains "B"
  case None    => ...//y does NOT contain "B"
}

For error reporting, you can use the method Main.reportError

case RawVar(inf, x) => ...Main.reportError(inf, "undefined variable:"+x);

Partial Solution

Here are solutions to Expr.scala and DeBruijnPhase.scala

The only interesting cases in the match of de Bruijn translation removeNames(e) are RawVar and Lam. We give their implementation here together with rules that specify what removeNames does

    case RawVar(inf, n) => 
      val ix = ctx.indexOf(n).match {
        case Some(i) => i
        case None    => 
          Main.reportError(inf, "undefined variable");
          nerrors = nerrors + 1;
          -1
      };
      Var(inf, ix, ctx.length);

Γ ⊢ removeNames(RawVar(inf,x)) = Var(inf,Γ.indexOf(x))

    case Lam(inf, x, e) => 
      Lam(inf, x, removeNames(e, ctx.update(x, NameBind)));

Γ, x ⊢ removeNames(e) = f

Γ ⊢ removeNames(Lam(inf,x,e)) = Lam(inf,x,f)

Here is the solution for the terms from above:

removeNames(\s.\z.z)                         = \s.\z.0
removeNames(\s.\z.s (s z))                   = \s.\z.1 (1 0)
removeNames(\m.\n.\s.\z.m s (n s))           = \m.\n.\s.\z.3 1 (2 1)
removeNames(\f.\x.f (\y. x x y) (\y. x x y)) = \f.\x.f (\y. 1 1 0) (\y.1 1 0)
removeNames((\x.(\x.x)) (\x.x))              = (\x.(\x.0)) (\x.0)

You have some more time to complete EvaluatorPhase.scala in case you did not finish.