--- tags: programming languages --- # Interpreting Lambda Calculus Pen-and-Paper (2022) Quite some material has accumulated, so I here summarize some salient points and then discuss the interpreter in more detail. Refer back to the earlier parts of these lecture notes for full detail. In particular, we will learn - the formal definition of capture avoiding substitution - to execute by hand $\lambda$-calculus programs according to its operatial semantics - how our Haskell implementation of the interpreter for $\lambda$-calculus works. ## Review ### Syntax of $\lambda$-calculus We review one example to remind us of the relevant notation. **Example:** - The $\lambda$-caclulus term $(\lambda x.x) a$ is written in our programming language LambdaNat as `(\x.x)a`. - Parsing this program via `echo "(\ x.x)a" | ./TestLambdaNat` gives us the linearized AST ```haskell Prog (EApp (EAbs (Id "x") (EVar (Id "x"))) (EVar (Id "a"))) ``` - For readability, in the following, it is tempting to abbreviate these trees as in ```haskell EApp (EAbs "x" (EVar "x")) (EVar "a") ``` but it is safer to do this only after we gained some practice. ### FAQs - Why do we need a grammar? The grammar is needed to generate the parser. - Why do we need a parser? The parser is needed to turn a program into its AST. - Why do we need an AST? The AST is used by the interpreter to evaluate (=run=execute) the program. - Ok, this sounds not too complicated. But I remember there was also sth like concrete syntax trees. What are they for then? CSTs are an intermediate representation used by the parser. The parser creates first a CST and then turns it into an AST. - Why do I need to understand what a CST is? If you want to design your own grammar, you need to understand CSTs in order to get the order of operation right. If you know the order of operations and how to translate concrete syntax to ASTs, you don't need to make a detour via CSTs. ## Operational Semantics Mathematically, the semantics of $\lambda$-calculus is given by the $\beta$-rule, which is to say, by capture avoiding substitution. This semantics has been implemented by [our interpreter for LamdaNat](https://github.com/alexhkurz/programming-languages-2022/blob/main/src/LambdaNat0/src/Interpreter.hs). For this lecture, we only need this [fragment](https://github.com/alexhkurz/programming-languages-2022/blob/main/src/LambdaNat0/src/Interpreter-fragment.hs). In the following we will execute the interpreter pen-and-paper, both using concrete syntax and abstract syntax. ### Capture Avoiding Substitution We do some computations by hand to convince ourselves that the substitution function `subst` is doing its job. We start with $$(\lambda x. x) a$$ Following the steps specified in the interpreter, we compute (line numbers refer to [`Interpreter-fragment.hs`](https://github.com/alexhkurz/programming-languages-2022/blob/main/src/LambdaNat0/src/Interpreter-fragment.hs)): ```haskell evalCBN (EApp (EAbs (Id "x") (EVar (Id "x"))) (EVar (Id "a"))) = -- line 6 evalCBN (subst (Id "x") (EVar (Id "a")) (EVar (Id "x"))) = -- line 15 evalCBN (EVar (Id "a")) = -- line 8 EVar (Id "a") ``` **Tip:** It is easier to apply an equation if one has an English phrase for it. For example, the equation of `line 6` I remember as "substitute the variable by the argument in the body". Then, for the pattern matching my eyes only need to be able to identify what the "variable", the "argument" and the "body" are in the term at hand. We will continue this on Thursday, but try to do similar examples yourself before ... Our next example is $(\lambda x.\lambda x. x) a$ which I want to write as $$(\lambda \color{red}{x}.\lambda \color{blue}{x}.\color{magenta}{x} ) a$$ The interesting question is whether the magenta $\color{magenta}{x}$ is bound by the red or by the blue one. This makes a difference, because in the first case $(\lambda x.\lambda x. x) a$ should evaluate to $\lambda x. a$ and in the second case to $\lambda x. x$. **Activity:** Discuss which of the two possible choices is taken in the programming languages you know. Now let us see what our interpreter actually implements. ```haskell evalCBN (EApp (EAbs (Id "x") (EAbs (Id "x") (EVar (Id "x")))) (EVar (Id "a"))) = -- line 6 evalCBN(subst (Id "x") (EVar (Id "a")) (EAbs (Id "x") (EVar (Id "x")))) = -- line 22 evalCBN(EAbs (Id "y") (subst (Id "x") (EVar (Id "a")) (EVar (Id "y")))) = -- line 16 evalCBN(EAbs (Id "y") (EVar (Id "y"))) = -- line 8 EAbs (Id "y") (EVar (Id "y")) ``` We find that the interpreter does implement the expected result.