Binary Lambda Calculus

Program:

Bits of output (leave blank to read all output):

Output:

What is this?

This is an interpreter for binary lambda calculus as described here.

In short, BLC is ordinary untyped lambda calculus in de Bruijn notation, encoded to a binary string using the following rules:

Lambda expressions are represented by \(00\) followed by the body of the expression.
Application is represented by \(01\) followed by the function first, and then the argument.
Variables are represented by \(1\) repeated \(n+1\) times (where \(n\) is the index of the variable in de Bruijn notation) followed by \(0\).

A BLC program consists of a binary string containing a lambda term in the above encoding, followed by the input string. To evaluate the program, the input string is applied to the lambda term in the form of a list of boolean values, where \(0\) becomes true and \(1\) becomes false. The resulting expression is also a list of boolean values, which is converted back to a binary string which is the output of the program.

Data structures

There are several important data structures to understand. Since every value in lambda calculus is a function, this means lists and boolean values are functions too.

True is represented by \(λx y.x\)
False is represented by \(λx y.y\)
A list is represented by \(λf.f h t\) where \(h\) is the first value in the list, and \(t\) is the rest of the list. The empty list is nil, which is equivalent to false.

So using the above rules, the binary string \(01\) becomes \(\langle true, \langle false, nil \rangle \rangle\) which is equal to \(λa.a (λb c.b) (λb.b (λc d.d) (λc d.d))\)

This is currently an experimental project. Feature requests, bug reports, and other improvements can be suggested on this project's GitHub Issues page. Pull requests and collaboration are welcome.