The Lambda Calculus is a mathematical language with one keyword. It's a Turing tarpit, discovered by Turing's doctoral advisor. This page introduces a 400 byte implementation of binary lambda calculus as an x86-64 Linux ELF executable. Friendly portable C code and prebuilt APE binaries are provided below for folks on other platforms too.

This implements a Church-Krivine-Tromp virtual machine with ASCII I/O. In 400 bytes we've managed to achieve garbage collection, lazy lists, and tail recursion. It extracts the least significant bit from an stdin byte. Output is only 0 and 1 bytes. It's slow but easy for learning. Displacement is limited to [0,255] so programs can't be too huge.

-rwxr-xr-x 1 jart jart  400 Feb 27 12:15blc
-rw-r--r-- 1 jart jart  17K Feb 27 12:15blc.S

Your virtual machine may be compiled on Linux for Linux x64 as follows:

cc -no-pie -static -nostdlib -Wl,-oformat:binary -o blcblc.S

Your program is read from stdin followed by its input. Here's a simple tutorial using the identity function (λ 0), which is encoded as (00 10) in the binary lambda calculus:

$ { printf 0010; printf 0101; } | ./blc; echo
0101

If you're on Mac, Windows, FreeBSD, NetBSD, or OpenBSD then you can do this instead:

$ curl <https://justine.lol/lambda/lambda.com> >lambda.com
$ chmod +x lambda.com
$ { printf 0010; printf 0101; } | ./lambda.com; echo
0101

Programs written in the binary lambda calculus are outrageously small. For example, its metacircular evaluator is 232 bits. If we use the 8-bit version of the interpreter (the capital Blc one) which uses a true binary wire format, then we can get a sense of just how small the programs targeting this virtual machine can be.

$ curl <https://justine.lol/lambda/uni.Blc> >uni.Blc
$ curl <https://justine.lol/lambda/Blc> >Blc
$ chmod +x Blc
$ { cat uni.Blc; printf ' '; printf 'hello world'; } | ./Blc; echo
hello world
$ ls -hal uni.Blc
-rw-r--r-- 1 jart jart 43 Feb 17 21:24 uni.Blc

This means that our 400 byte virtual machine implementation has an expressive enough byte code language, that it can implement itself in one tenth the size! This sort of thing could have practical applications in things like compression formats. See the busy beaver example below. It's also just downright cool.

The ASCII binary serialization format, is defined as follows:

00      means abstraction   (pops in the Krivine machine)
01      means application   (push argument continuations)
1⋯0     means variable      (with varint de Bruijn index)
000010  e.g. means λλ0
0000110 e.g. means λλ1

You can use sed shell scripts as a byte code compiler. All it has to do is s/λ/00/g, s/\\[/01/g, s/[^01]//g, etc.

#!/bin/sh
tr \\\\n n |
  sed '
      s/;.*//
      s/#.*//
      s/1/⊤/g
      s/0/⊥/g
      s/λ/00/g
      s/\\[/01/g
      s/9/11111111110/g
      s/8/1111111110/g
      s/7/111111110/g
      s/6/11111110/g
      s/5/1111110/g
      s/4/111110/g
      s/3/11110/g
      s/2/1110/g
      s/⊤/110/g
      s/⊥/10/g
      s/[^01]//g
    '

We can now write nicer looking programs:

{ printf %s "(λ 0)" | ./compile.sh
  printf 00010101
} | ./blc

Here's some important values:

nil="λλ0"
false="λλ0"
true="λλ1"