A simple lambda interpreter

Posted on April 2, 2014 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:

Here's a screenshot of an early version:

Screenshot of the program, during the computation of 2^2

Screenshot of the program, during the computation of \(2^2\)

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:

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.