Lambda Calculus Interpreter

The window above is a lambda calculus REPL. You can type a lambda expression and it will be evaluated when you press enter. Keep reading to learn about the expected syntax and supported features.

Grammar

The parser only understands the following simple grammar (parentheses around applications, nowhere else).

<exp> ::= <var>
       |  λ<var>.<exp>
       |  (<exp> <exp>)

For convenience, you can use a backslash instead of λ.

REPL

Type an expression and it will be evaluated in normal order. The result is displayed using De Bruijn indices.

> (\x.x \x.x)
λ.1

De Bruijn indices are the internal representation and the displayed form, but cannot be used as input.

Global variables

Evaluation results can be stored in global variables. Whenever there is a name for an expression, it is printed in the REPL instead of the lambda expression.

> ID = \x.x
ID

This makes it easier to write complex expressions and improves readability. To get the lambda expression, just type the name.

> ID
λ.1

Delete variable bindings with an 'empty assignment'.

> ID =
Removed variable binding 'ID = λ.1'

A few useful global variables are loaded by default on startup, e.g., TRUE, FALSE, NOT, ONE, SUCC, EXP, CONS, and Y. They can be overwritten and deleted just like any other variable. Type a single dot . to get a list of all available global variables.

The same expression can have several names and all of them are printed.

> ((AND TRUE) FALSE)
NIL, ZERO, FALSE

Reduction strategies

By default, the interpreter evaluates under abstractions (to normalize as much as possible and get the best variable mapping). For some expressions this results in infinite recursion, for example with the fixed-point combinator Y. In such cases you can switch to a 'lazy' reduction strategy by adding a question mark after the expression.

> Y
scala.scalajs.js.JavaScriptException: InternalError: too much recursion
> Y ?
λ.(λ.(2 (1 1)) λ.(2 (1 1)))

If we apply the Y combinator, e.g., to the length function and the list of booleans below, we may obtain an expression that can be reduced to normal form.

> LENGTH = \len.\l.(((IF (ISNIL l)) ZERO) (SUCC (len (CDR l))))
> LIST = ((CONS TRUE) ((CONS TRUE) NIL))
> ((Y LENGTH) LIST)
TWO

How does it work?

I implemented the interpreter in Scala and compiled the code to JavaScript using Scala.js, so all of this runs in your browser.

This page was moved from my old website.