# A simple lambda interpreter

Posted on 2018 03 27 by phimuemue

I was never an expert of lambda-calculus, but I always wanted to learn (at least the basics of) it. So, I decided to write a very simplistic interpreter for the untyped lambda calculus.

## Goals for the project

The goals for this small tool are relatively simply to describe:

• Simple user interface: command-line based, repl-loop-like. In particular, I wanted to help the user with manual lambda calculations. For this reason, I wanted support for some things:
• Abbreviations/macros, so that the user does not need to input too many things at once.
• Step-by-step evaluation of lambda expressions.
• Simple codebase.
• Language of choice: Haskell (using Parsec to parse user input).

Here's a screenshot of an early version:

As you can see, the program supports colors for specific parts of a lambda expression. A beta-reduction that's going to take place in the next step is displayed such that the function that is applied is displayed in red, while the argument is printed blue.

## Lambda expressions

A very straightforward approach to representing expressions in Haskell could look as follows:

data Expression =
Variable String
| Abstraction String Expression
| Application Expression Expression

However, I decided to equip abstractions and applications with an additional flag indicating whether the respective abstraction can be eta-reduced or the respective application can be beta-reduced. This results in the following declaration:

data Expression =
Variable String
-- abstractions may be eta-convertible
| Abstraction Bool String Expression
-- applications may be beta-convertible
| Application Bool Expression Expression

While this makes pattern matching more cumbersome in many places, it gives more freedom in other contexts: Different reduction strategies can be implemented in a more general manner and we do not have to update the color-printing routine for each reduction strategy: We simply set the corresponding flags (the ones that shall be reduced in the next step), pretty-print the expression and apply the reductions.

I also installed some smart constructors that automatically create abstractions or applications with the flag set to False. From now on, we will also call these flags tags.

## Parsing lambda expressions

I never used a Parser combinator before and was pleasantly surprised how comfortable it is to use Parsec. We can parse lambda expressions in under 40 lines of code (and I suppose this code can be improved):

variableParser :: Parser Expression
variableParser = do r <- many1 (noneOf " .\\()")
return (Variable r)

applicationParser :: Parser Expression
applicationParser = do content <- endBy1 vl spaces
return $foldl1 (\a b -> application a b) content where vl = (try variableParser <|> try parensLambdaParser) abstractionParser :: Parser Expression abstractionParser = do char '\\' spaces varlist <- (endBy1 variableParser spaces) char '.' spaces body <- lambdaParser spaces return$ foldr (\(Variable v) a -> abstraction v a)
body varlist

parensLambdaParser :: Parser Expression
parensLambdaParser = do char '('
spaces
content <- lambdaParser
spaces
char ')'
_ <- spaces
return content

lambdaParser :: Parser Expression
lambdaParser = (try applicationParser)
<|> (try variableParser)
<|> (try abstractionParser)
<|> (try parensLambdaParser)

parseLambda s = case parse lambdaParser "(unknown)" s of
Right a -> Just a
Left _ -> Nothing

## Rewriting lambda expressions

### Normal-order

For now, let us simply consider how we can implement the normal order reduction. As said before, we first of all set only those tags to True whose beta-reductions shall be done. The following code does exactly this:

betaReducible term = case term of
Variable _ -> False
e@(Application _ (Abstraction _ _ _) _) -> True
Application _ f x -> (betaReducible f) || (betaReducible x)
Abstraction _ x f -> betaReducible f

normalOrderTags term = case term of
Application _ e@(Abstraction _ x f) y -> Application True e y
Application _ f x -> if betaReducible f
then application (normalOrderTags f) x
else application f (normalOrderTags x)
Abstraction _ x f -> abstraction x (normalOrderTags f)
e -> e

The simple case distinction of normalOrderTags works as follows:

• If we have an application whose first part is an abstraction, we will be able to perform a beta reduction.
• If we have an application whose first part is not an abstraction, we check whether its first component is beta-reducible. If so, we install the proper tags in the first subexpression and leave the second as it is. If not, we install possible tags in the second subexpression.
• If we have an abstraction, we have to compute the tags within the body of the abstraction.
• If we have something else (i.e. a variable), we simply return it as it is.

The case distinction in betaReducible is structured similar.

If we now want to apply all beta-reductions that we have found by using normalOrderTags, we can use the following function:

-- applyTags takes a (possibly) tagged expression and returns an untagged one
applyTags :: Expression -> Expression
applyTags term = case term of
Variable x -> Variable x
Application False f x -> application (applyTags f) (applyTags x)
Application True (Abstraction _ x f) y -> replaceVariable f x y
Application True _ y -> error "Disallowed tagged application."
Abstraction False x f -> abstraction x (applyTags f)
Abstraction True x (Application _ f y) -> applyTags f
Abstraction True x _ -> error "Disallowed tagged abstraction."

Again, we have simple case distinctions, but now incorporating the value of the tag so that we can determine whether the current subterm shall be reduced or not.

### All outermost reductions

Another, more aggressive reduction strategy is to take all outermost possible reductions and perform them. The relevant code could look as follows:

allOutermostTags :: Expression -> Expression
allOutermostTags term = case term of
-- eta-reducible abstraction
Abstraction _ x e@(Application _ f (Variable y)) ->
if x==y
then Abstraction True x e
else Abstraction False x $allOutermostTags e -- beta-reducible application Application _ e@(Abstraction _ x f) y -> Application True e y -- "normal stuff" Variable x -> Variable x Abstraction _ x f -> Abstraction False x$ allOutermostTags f
Application _ f x -> Application False tf tx
where tf = allOutermostTags f
tx = allOutermostTags x

Note that this does not include "nested" reductions. I.e. if we set the tag for a beta reduction, we won't set any tags for its two subexpressions.

## Code

The full code is hosted over there at github.