Exercise 4 Buffer Session

This exercise session can be used to complete the exercises of the previous weeks.

For those who have already finished, here is an optional task to deepen your understanding on the use of type systems in compilers.

Symbols instead of Indices

We have used de Bruijn indices to avoid name clashes. Another way that is closer to what actually happens in compilers is to use Symbols.

A symbol is an object that is generated for each name definition (in our languages, that would be lambda abstraction). Name references are then resolved to symbol references by name analysis.

Since objects can easily be distinguished from each other, name clashes cannot happen - symbols are not compared based on their name, but on their memory location.

There will be no solutions for these exercises.

Optional Task 4.1

Change the implementation of the untyped lambda evaluator to use symbols.

• Write a class Symbol to represent symbols. It must not be a case class.
• add mutable fields var sym:Symbol to Lam and Var
• change the Context so that it is a subclass of scala.collection.immutable.ListMap[Symbol,Binding]
• Replace the DeBruijnPhase with a NameAnalysis phase that generate and sets symbols. Change the Main class so that it calls NameAnalysis instead of DeBruijnPhase
• Change the substitution in the evaluator, so that it works on symbols instead of integer indices. Test your program.

Optional Task 4.2

• Adapt your changes to the simply typed evaluator.
• Do you still need the class Context after name analysis?

Optional Task 4.3 (only for the lambda addicted)

A more elegant way to formulate the lambda calculus is to fix a set of constants, for our language C = {true,false,succ,pred,iszero,if} and define the set of terms as E ::= x | E E | \x.E | c where c is a constant. Constants are typed.

In addition to beta reduction, there is a set C_rules that defines how to apply reductions on applications built up from constants.

Write up the formal definitions, for an arbitrary set C_rules.

Based on this definition, write scala functions for the constructors succ,zero,true,false which represent Num as Int, Bool as Boolean. Write Scala functions for the predefined functions that compute the desired value. These are your C_rules (you need to create an initial context so that names that look like free variables are bound to the constants).

Write a fast interpreter for our language (which does not output single reductions) using the functions.