February 27^th, 2022 @ justine’s web page

The Lambda Calculus is a programming language with a single keyword.
It’s the Turing tarpit discovered by Turing’s doctoral advisor. This
blog post introduces a brand new 400 byte implementation of binary
lambda calculus as an x86-64 Linux ELF executable. Friendly portable C
code and prebuilt APE binaries are provided
for other platforms too.

SectorLambda implements a Church-Krivine-Tromp virtual machine with
monadic I/O. In 400 bytes we’ve managed to achieve garbage collection,
lazy lists, and tail recursion. The interpreter works by extracting the
least significant bit from each stdin byte. Output consists of 0 and 1
bytes. It’s 64-bit however displacement is limited to [0,255] so
programs can’t be too huge. That makes it a fun tool for learning, but
for more industrial scale applications a 520 byte version is provided
too, that overcomes many of those limitations, although it requires
writing code at an even higher difficulty setting.

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

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

cc -no-pie -static -nostdlib -Wl,-oformat:binary -o blc blc.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

Why It Matters

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 521 byte virtual machine is expressive enough to
implement itself in just 43 bytes, which is one tenth its size! As a
virtual machine it also has capabilities that the JVM lacks, even though
it’s literally six orders of a magnitude tinier. Something like this
could have practical applications in compression formats, which need a
small busy beaver that can produce large amounts of data. It’s also just
downright cool.

For example, if you built a compression tool you could have it encode a
file as a lambda expression that generates it. Since it’s difficult to
introduce a new compression format that most people haven’t installed,
you could prefix the compressed file with this 400 byte interpreter to
get autonomous self-extracting archives that anyone can use. Binary
Lambda Calculus would also make more sense than LISP as an embedded
microprocessor.

Compilation

Programs are encoded in the following format:

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

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

Programming

This program means exit(0) because it returns $nil or []:

λ λλ0

This program returns [⊥,⊤] so it prints 10.

λ [[$pair $false] [[$pair $true] $nil]]

This program means if (1 - 1 == 0) putc('1') else putc('0');

λ [[[$if [$iszero [[$sub $one] $one]]]
      [[$pair $false] $nil]]
   [[$pair $true] $nil]]

This program does the same thing as the ident program but is more
spelled out. The two arguments the runtime passes are gro
and put (or λ
[[0 wr0] wr1]).
Index 110 is is the outer parameter and 10 is the inner parameter. So
this program is the same as doing for (;;) putc(getc())

λλ [1 0]
││
│└binds `put` or `(λ 0 wr0 wr1)` [cited as 0]
└binds `gro` or `⋯` [cited as 1]

This will invert a stream of bits using the Y combinator. It’s got a
whopping 16kBps of throughput.

# a.k.a. Y(λab.(λc.c)b(λcde.❬¬c,ad❭)⊥)
[$Y λλ [[[$if 0] λλλ [[$pair [$not 2]] [4 1]]] $nil]]
    ││           │││
    ││           ││└consumes $nil terminator [uncited]
    ││           │└binds 𝑝 input bit [cited as 1]
    ││           └binds (λ 0 𝑝 ⋯) [cited as 2]
    │└binds gro (λ 0 𝑝 ⋯) [cited by first 0]
    └binds recursive function [cited as 4]

If you want an explanation of what’s going on, you can use the
lambda.com interpreter with the -r
flag. For example, here’s the above code reduced with empty input. You
can see it doing things like applying the Y combinator. Then it reads
some input, and it uses the input bit as a predicate in an if condition.
Unlike LISP, lambda calculus does head reduction, so the evaluator could
be thought of as lazily consuming a stream of continuations. This whole
paradigm is the reason why languages like Haskell don’t need so many
parentheses.

$ nil="λλ 0"
$ true="λλ 1"
$ false="λλ 0"
$ not="λ [[0 $false] $true]"
$ Y="λ [λ [1 [0 0]] λ [1 [0 0]]]"
$ printf %s "[$Y λλ [[0 λλλ [[$pair [$not 2]] [4 1]]] $nil]]" | ./compile.sh | ./lambda.com -r
[Y λλ [[0 λλλ [[pair [¬ 2]] [4 1]]] ⊥]]
λ [0 put] [[Y λλ [[0 λλλ [[pair [¬ 2]] [4 1]]] ⊥]] ⋯]
0 put
Y λλ [[0 λλλ [[pair [¬ 2]] [4 1]]] ⊥] ⋯ put
λ [1 [0 0]] λ [1 [0 0]] ⋯ put
1 [0 0] ⋯ put
λλ [[0 λλλ [[pair [¬ 2]] [4 1]]] ⊥] [0 0] ⋯ put
λ [[0 λλλ [[pair [¬ 2]] [4 1]]] ⊥] ⋯ put
0 λλλ [[pair [¬ 2]] [4 1]] ⊥ put
⋯ λλλ [[pair [¬ 2]] [4 1]] ⊥ put
⊥ λλλ [[pair [¬ 2]] [4 1]] ⊥ put
λ 0 ⊥ put
0 put
⊥ put
λ 0

This program means for x in reversed(stdin): put(x)

# a.k.a. λa.a(ω(λbcde.d(bb)(λf.fce)))⊥
λ [[0 [λ [0 0] λλλλ [[1 [3 3]] λ [[0 3] 1]]]] $nil]

This program means ['1'] * 4**3 times. If you need to
exponentiate larger numbers like 9**3 (big data by FP standards) then
you’ll need to tune the STACK parameter in blc.S to ask the operating
system for something bigger than what’s provided by default.

λ [[$Y λλ [[[$if [$iszero 0]]
                $nil]
             [[$pair $false]
              [1 [$dec 0]]]]]
   [[$pow $four] $three]]

Here’s a BLC interpreter written in BLC which is 232 bits.

[[λ [0 0]
  λλλ [[[0 λλλλ [2 λ [[4 [2 λ [[1 [2 λλ [2 λ [[0 1] 2]]]]
                               [3 λ [3 λ [[2 0] [1 0]]]]]]]
                      [[0 [1 λ [0 1]]]
                       λ [[3 λ [3 λ [1 [0 3]]]] 4]]]]]
        [2 2]] 1]]
 λ [0 [λ [0 0] λ [0 0]]]]

Here’s a Hilbert space filling curve generator using the 8-bit version:

$ curl https://justine.lol/lambda/hilbert.Blc >hilbert.Blc
$ curl https://justine.lol/lambda/Blc >Blc
$ chmod +x Blc
$ { cat hilbert.Blc; printf 123; } | ./Blc
 _   _   _   _
| |_| | | |_| |
|_   _| |_   _|
 _| |_____| |_
|  ___   ___  |
|_|  _| |_  |_|
 _  |_   _|  _
| |___| |___| |

Definitions

Here’s some important values:

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

Here’s some important abstractions:

if="λ 0"
pair="λλλ [[0 2] 1]"
car="λ [0 $true]"
cdr="λ [0 $false]"
or="λλ [[1 1] 0]"
and="λλ [[1 0] 1]"
not="λ [[0 $false] $true]"
xor="λλ [[1 [$not 0]] 0]"
iszero="λ [[0 λ $false] $true]"
Y="λ [λ [1 [0 0]] λ [1 [0 0]]]"

Here are your integers:

zero="λλ 0"
one="λλ [1 0]"
two="λλ [1 [1 0]]"
three="λλ [1 [1 [1 0]]]"
four="λλ [1 [1 [1 [1 0]]]]"
five="λλ [1 [1 [1 [1 [1 0]]]]]"
six="λλ [1 [1 [1 [1 [1 [1 0]]]]]]"
seven="λλ [1 [1 [1 [1 [1 [1 [1 0]]]]]]]"
eight="λλ [1 [1 [1 [1 [1 [1 [1 [1 0]]]]]]]]"
nine="λλ [1 [1 [1 [1 [1 [1 [1 [1 [1 0]]]]]]]]]"

Here’s some arithmetic:

pow="λλ [0 1]"
mul="λλλ [2 [1 0]]"
dec="λλλ [[[2 λλ [0 [1 3]]] λ 1] λ 0]"
sub="λλ [[0 $dec] 1]"
inc="λλλ [1 [[2 1] 0]]"
add="λλλλ [[3 1] [[2 1] 0]]"
fac="λλ [[[1 λλ [0 [1 λλ [[2 1] [1 0]]]]] λ1] λ0]"
min="λλλλ [[[3 λλ [0 1]] λ1] [[2 λλ [3 [0 1]]] λ1]]"
div="λλλλ [[[3 λλ [0 1]] λ 1] [[3 λ [[[3 λλ [0 1]] λ [3 [0 1]]] λ0]] 0]]"
mod="λλλλ [[[3 $cdr] [[3 λ [[[3 λλλ [[0 [2 [5 1]]] 1]] λ1] 1]] λ1]] λλ0]"

Here’s some predicates:

eq="λλ [[[[1 λ [[0 λ0] λ0]] [[0 λλλ [1 2]] λλ0]] λλλ0] λλ1]"
le="λλ [[[1 λλ [0 1]] λλλ1] [[0 λλ [0 1]] λλλ0]]"
lt="λλ [[[0 λλ [0 1]] λλλ0] [[1 λλ [0 1]] λλλ1]]"
odd="λ [λ [0 0] λλ [[0 λλ 1] λ [[0 λλ 0] [2 2]]]]"
divides="λλ [[[1 $cdr] [$omega λ[[[1 λλλ [[0 [2 λλ0]] 1]] λ[1 1]] λλ1]]] λλ0]"

Tooling

Here’s how you’d use the blcdump utility:

$ printf 0010 | blcdump.com -l 2>/dev/null
λa.a

# convert to traditional notation
$ blcdump.com -l /dev/null
ω(λab.b(λcdef.f(c⊥⊤)(aad))⊥)

# convert to de Bruijn notation
$ blcdump.com /dev/null
[ω λλ [[0 λλλλ [[0 [[3 ⊥] ⊤]] [[5 5] 2]]] ⊥]]

# convert Blc to blc
$ blcdump.com -bB /dev/null
00011001010001101000000001010101100000000000010...

# create portable lambda expression
$ blcdump.com -lnNS /dev/null
(a.a a) (a.(b.(b (c.(d.(e.(f.(f(c (g.(h.h)) (g.(h.g)))(a a d)))))) (c.(d.d)))))

Here’s how you’d use the lam2bin utility:

$ { printf 'λa.a' | lam2bin.com; printf 1010; } | blc
1010
$ { printf '\a.a' | lam2bin.com; printf 1010; } | blc
1010
$ { printf 'ω(λab.b(λcdef.f(c⊥⊤)(aad))⊥)' | lam2bin.com; printf 1010; } | blc
0101

Here’s how you’d use the asc2bin utility:

$ { printf 'λa.a' "http://justine.lol/lam2bin.com" asc2bin.com; echo hello; } | Blc
hello

Runtime

Your VM expands your program on startup as follows:

𝑝 ⟶ [λ [0 λ [[0 wr0] wr1]] [𝑝 ⋯]]

The lazy list convention reduces as follows:

⋯ ⟹ $nil                     ;; if eof / error
⋯ ⟹ λ [[0 $false] ⋯]         ;; if ~getc() & 1
⋯ ⟹ λ [[0 $true] ⋯]          ;; if  getc() & 1

The wr0 and wr1 conventions reduce as follows:

wr0 ⟹ λ [0 λ [[0 wr0] wr1]]  ;; w/ putc(0) side-effect
wr1 ⟹ λ [0 λ [[0 wr0] wr1]]  ;; w/ putc(1) side-effect

The 8-bit (capital Blc) runtime expands using big-endian lists. For
example, space (0b00100000) would be:

λ [[0 λ [[0 ⊤] λ [[0 ⊥] λ [[0 ⊥] λ [[0 ⊤] λ [[0 ⊥] λ [[0 ⊤] λ [[0 ⊤] λ [[0 ⊤] ⊥]]]]]]]]] ⋯]

Binaries
 

-rwxr-xr-x 1 jart jart  400 Feb 27 12:15 blc (linux x86-64 only)
-rwxr-xr-x 1 jart jart  521 Feb 27 12:15 Blc (linux x86-64 only)
-rwxr-xr-x 1 jart jart  32K Feb 27 12:11 tromp.com (ioccc 2012)
-rwxr-xr-x 1 jart jart  68K Feb 27 12:11 lambda.com (friendly)
-rwxr-xr-x 1 jart jart  60K Feb 27 12:11 blcdump.com
-rwxr-xr-x 1 jart jart  52K Feb 27 12:11 bru2bin.com
-rwxr-xr-x 1 jart jart  56K Feb 27 12:11 lam2bin.com

Programs

-rw-r--r-- 1 jart jart  84 Feb 27 12:54 invert.blc
-rw-r--r-- 1 jart jart 167 Feb 27 12:52 primes.blc
-rw-r--r-- 1 jart jart 232 Feb 27 12:52 uni.blc
-rw-r--r-- 1 jart jart  43 Feb 27 12:52 uni.Blc
-rw-r--r-- 1 jart jart  67 Feb 27 12:52 reverse.blc
-rw-r--r-- 1 jart jart   9 Feb 27 12:52 reverse.Blc
-rw-r--r-- 1 jart jart 186 Feb 27 12:52 symbolic.Blc
-rw-r--r-- 1 jart jart 143 Feb 27 12:52 hilbert.Blc
-rw-r--r-- 1 jart jart 141 Feb 27 12:52 parse.Blc
-rw-r--r-- 1 jart jart 112 Feb 27 12:52 bf.Blc
-rw-r--r-- 1 jart jart 112 Feb 27 12:55 hw.bf

Scripts

-rwxr-xr-x 1 jart jart  343 Feb 27 12:06 compile.sh
-rwxr-xr-x 1 jart jart  224 Feb 27 12:06 trace.sh
-rwxr-xr-x 1 jart jart  661 Feb 27 12:06 lam2sh.sh
-rwxr-xr-x 1 jart jart  573 Feb 27 12:06 lam2sqr.sh
-rwxr-xr-x 1 jart jart  565 Feb 27 12:06 sqr2lam.sh

Sources

-rw-r--r-- 1 jart jart  17K Feb 27 12:15 blc.S
-rw-r--r-- 1 jart jart  12K Feb 24 17:25 Blc.S
-rw-r--r-- 1 jart jart 3.1K Feb 27 12:18 Makefile
-rw-r--r-- 1 jart jart 1023 Feb 27 12:03 tromp.c
-rw-r--r-- 1 jart jart 7.9K Feb 27 12:04 lambda.c
-rw-r--r-- 1 jart jart 3.1K Feb 27 12:05 asc2bin.c
-rw-r--r-- 1 jart jart 7.9K Feb 27 12:05 lam2bin.c
-rw-r--r-- 1 jart jart 8.3K Feb 27 12:05 bru2bin.c
-rw-r--r-- 1 jart jart 4.7K Feb 27 12:08 blcdump.c
-rw-r--r-- 1 jart jart 1.3K Feb 27 12:05 blc.h
-rw-r--r-- 1 jart jart 4.5K Feb 27 12:09 debug.c
-rw-r--r-- 1 jart jart 2.2K Feb 27 12:09 error.c
-rw-r--r-- 1 jart jart 2.4K Feb 27 12:09 getbit.c
-rw-r--r-- 1 jart jart 7.9K Feb 27 12:04 lambda.c
-rw-r--r-- 1 jart jart 1.8K Feb 27 12:10 needbit.c
-rw-r--r-- 1 jart jart 2.5K Feb 27 12:08 parse.c
-rw-r--r-- 1 jart jart  35K Feb 27 12:08 print.c
-rw-r--r-- 1 jart jart 1023 Feb 27 12:03 tromp.c
-rw-r--r-- 1 jart jart 2.5K Feb 27 12:10 vars.c

DWARF Transparency

-rwxr-xr-x 1 jart jart 419K Feb 27 12:11 tromp.com.dbg
-rwxr-xr-x 1 jart jart 822K Feb 27 12:11 lambda.com.dbg
-rwxr-xr-x 1 jart jart 736K Feb 27 12:11 blcdump.com.dbg
-rwxr-xr-x 1 jart jart 663K Feb 27 12:11 bru2bin.com.dbg
-rwxr-xr-x 1 jart jart 677K Feb 27 12:11 lam2bin.com.dbg

Blinkenlights Demo

Similar to the demos included in the
earlier SectorLISP blog post, here’s a
screencast of SectorLambda running
in Blinkenlights. The program being
typed into the console is the identity function 0010 a.k.a. (λ 0) a.k.a.
λ𝑥.𝑥. Once the program is typed in, any further keystrokes will be
echo’d based on the least significant bit.

On the bottom right you can see heap allocations on the stack increasing
as it builds its list. On the top right you can see immutable terms grow
as it reads input. Those terms are written immediately after the
executable image.

Subroutine Diagrams

λ [$omega [0 λ 1]]

000100011010011000110

λ [[[0 λλ [[0 1] 0]] $omega] 0]

00010101100000010110110100001101010

00010101100000000101111010000111
10011101000001100010

000000000101011111000000110110001
100101111000000111110011011000110

λ [[0 [$omega
       λλλλ [[1 [3 3]] λ [[0 3] 1]]]]
    $nil]

0001011001000110100000000001011100
111110111100001011011110110000010

λ [$omega λλ [[0 $false] [1 1]]]

00010001101000000101100000100111
0110

00010001101000000101100000110011
10110

00000101011100000011011000000011
00101100000011011000000010

00000101010111000010110001000100
10110000000011101110000010000000
100000110

λλλλ [[3 1] [[2 1] 0]]

000000000101111101100101111011010

λλ [[0 λλλ [[[2 λλ [0 [1 3]]]
            λ 1] λ 0]] 1]

00000101100000000101011110000001
100111011110001100010110

λλ [[[1 λλ [0 [1
    λλ [[2 1] [1 0]]]]] λ 1]
        λ 0]

00000101011100000011001110000001
0111101100111010001100010

[$Y λλ [[[$if 0]
             λλλ [[$pair [$not 2]]
                         [4 1]]]
           $nil]]

01000110100000010110000000000101
10010111110000010000011001011111
11011111101110000010

00010001101000000101100000100001
011000001100111101110

00010001101000000101100000110000
101100000100111101110

00000101011000000110110000000100
10111000000110110000000110

000101100100011010000000000001011
011110010111100111111011111011010

division

λabcd.a(λef.fe)(λe.d)(a(λe.b(λfg.gf)(λf.c(fe))(λf.f))d)

λλλλ [[[3 λλ [0 1]] λ 1] [[3 λ [[[3 λλ [0 1]] λ [3 [0 1]]] λ 0]] 0]]

0000000001010111110000001101100011001011111000010101111100000011
01100001111100110110001010

modulus

λabcd.a(λe.e(λfg.f))(a(λe.b(λfgh.h(f(cg))g)(λf.e)d)(λe.d))(λef.f)

λλλλ [[[3 λ [0 λλ 1]] [[3 λ [[[3 λλλ [[0 [2 [5 1]]] 1]] λ 1] 1]] λ 1]] λλ 0]

0000000001010111110000110000011001011111000010101111100000000101
100111100111111101101100011011000110000010

divides predicate

λab.a(λc.c(λde.d))((λc.cc)(λc.b(λdef.f(d(λgh.h))e)(λd.cc)(λde.d)))(λcd.d)

0000010101110000110000011001000110100001010111000000001011001111
000001011000011101100000110000010

binary lambda calculus interpreter

(λa.aa)(λabc.c(λdefg.e(λh.d(f(λi.h(g(λjk.i(λl.lkj)))(f(λj.g(λk.ik(jk))))))(h(g(λi.ih))(λi.f(λj.g(λk.j(kh)))e))))(aa)b)(λa.a((λb.bb)(λb.bb)))

0101000110100000000101011000000000011110000101111110011110000101
1100111100000011110000101101101110011111000011111000010111101001
1101001011001110000110110000101111100001111100001110011011110111
1100111101110110000110010001101000011010

binary lambda calculus interpreter w/ byte i/o

λa.a((λb.bb)(λb.(λcde.e(λfgh.g(λijk.(λl.f(c(λm.i(l(λno.m(λp.pon)))(c(λn.l(λo.mo(no)))))j)(i(l(λm.mi)j)(c(λm.l(λn.m(ni)))g)))d)(λi.i(λj.cd(λk.kfj))))(λf.f(cd)))(bb))(λbc.b((λd.dd)(λd.dd))))

0001100101000110100001000000010110000000010111000000001000101111
1111001011111111111000010111111001110000001111000010110110111001
1111111111100001111000010111101001110101110010111110010110000110
1111101110010111111111110000111000011100110111111011111101111111
1000011000010111111111011111110000101101111110110000110011111011
10011010000001110010001101000011010

Goldbach

(λa.a((λb.bb)(λbcd.(λef.ae(f(bbe)))(λe.eed(λf.fc)e))(λbcde.e)))((λa.aa)(λabc.c(λde.e)((λd.aad((λe.ee)(λe.d(ee))))(λd.(λe.e(e(bd)))(λefgh.hf(ge)))))(λabcd.d(λef.e)(ca)))

0100011001010001101000000001000001011111110110011001011111101111
1011000010101011010110000110111101000000000100101000110100000000
1011000001001000101011111011110100100011010000111001101000010001
1001100111110110000000000101101110011101111000000000010110000011
00111011110

Goodstein

λa.a(λbcd.b(λe.c(λfg.e(λhij.jh(if))(λh.g)(λhi.i)))(λef.de(d(λg.e(λhij.g(cdi(λkl.j(λm.mkl))(λkl.j(λm.kml))h)ij))f)))(λb.b)(λb.b(λcd.c)(λc.c))(λb.b(λcde.c))(λb.b)(λbc.b(λde.cd(de)))(λbc.b(λde.cd(d(de)))c)(λb.b)

0001010101010101011000000001011110000111100000010101111000000001
0110111001110111110001100000100000010111101100101111000011110000
0000101011111001010101011111111101111111011000000111100001011011
1011000000111100001011110101101110110101000100001011000001100010
0001100000001110001000000111000000101111011001110100000010111000
0001011110110011100111010100010

primes

λa.(λb.(λc.b(b((λd.dd)(λdef.f(λgh.h)((λg.ddg((λh.hh)(λh.g(hh))))(λghij.jh(i(eg)))))(λdef.b(fd))))((λde.d(d(de)))(ccc)(λdefg.ge(fd))(λdefg.g)))(λcd.c(cd)))(λbc.c(λde.d)b)

0001000100010111001110010100011010000000010110000010010001010111
1101111010010001101000011100110100000000001011011100111001111111
0111100000000111111001101110010101000001110011100111010010110101
0000000000101101110011101111000000000100000011100111010000001011
00000110110

sort

λa.(λb.bb)(λb.(λcde.e(λfg.(λh.hh)(λhi.i(λjkl.hhk(λm.j(λnopqrs.sm(n(λu.uoq)q)(nr(λu.uor)))(λnop.p(λqr.mq(λs.sqr))no)))(λj.(λk.jkkk)(λkl.l)))e(λhijk.(λl.h(d(λmn.n))(c(l(λmn.m))i(c(l(λmn.n))jk)))(λlm.d(λn.nlm)))))(bb))(λb.b)a(λbc.c)

0001010101000110100001000000011000000101010001101000000101100000
0001010111111011111011000010111110000000000000010101101111111001
0111111100001011011111101111011100101111111011000010110111111011
1000000001010110000001011111110110000101101110110111011000010001
0101110101010000010111000000000010001011111100111111111100000100
1010111111111110011000001101111001010111111111110011000001011101
1000000111111111110000101101110110011010001010000010

compliant brainf#*k interpreter

λa.(λb.a((λc.cc)(λc.(λd.(λe.(λf.(λg.(λh.g(f(h(f(h(f(h(h(e(b(λijk.ikj)))))(f(f(e(λijklm.m(λn.inkl)))(e(b(λi.i))))(g(e(λijklmn.nj(ijklm)))))))(h(h(f(g(e(λijkl.l(λm.im(λn.njk)))))(g(e(λijkl.ki(λm.mjl)))))))))(g(h(h(f(h(h(λij.jd(λk.e((λl.ll)(λlmn.n((λo.oo)(λopq.p(q(oo))(λr.k(llr))))mn))k))))(g(h(λijk.k(λl.l)j)))))))))(f(e(λh.h))))(λg.fg(e(λh.h))))(λfgh.h(λi.ifg)))(λefg.gd(λhij.j(λk.e(hk))i)))(cc)))(λc.(λd.dd)(λde.e((λf.f(f(f(λgh.h(λij.i)g))))(λfg.f(fg))(λfg.g))(dd))(c(λdefghi.i))c))(λbcd.c((λe.ee)(λefg.f(λhij.eei(λkl.g(λm.m(lh)k)(bhl(λm.m))))(gf(λhij.hji)))d(λef.e)))

0001000101110010001101000010001000100010001000111001011110011001
0111100110010111100110011001111100111111110000000010111101011001
0111100101111001111100000000000011000010101111111010111101110011
1110011111111000100111001111100000000000000101101111100101010111
1111011111011110111011001100110010111100111001111100000000001100
0010111111010000101101111101111001110011111000000000010111011110
0001011011110110011100110011001011110011001100000010110111111100
0010111111110010001101000000001010110010001101000000001011100110
0111101110000111111111001011111111011111110101101010011100110000
0000101100010110011100111100010000101110100111100010000000011000
0101101111011100000000101101111000000001011000011111111001111101
0110011010000101010001101000000101100101000110011001100000010110
0000110110000001110011101000001001110110011000000000000010100000
0001110010101000110100000000101110000000010101111111011111101100
0000101111111000010110011101111110111001010111111111111011111010
00100101101100000000101111010110100000110

How It Works

#define IOP 0  // code for gro, wr0, wr1, put
#define VAR 1  // code for variable lookup
#define APP 2  // code for applications
#define ABS 3  // code for abstractions
#define REF(c) (++(c)->refs, c)

struct Parse {
  int n;
  int i;
};

struct Closure {
  struct Closure *next;
  struct Closure *envp;
  int refs;
  int term;
};

static const char kRom[] = {
    APP, 0,  //  0 (λ 0 λ 0 (λ 0 wr0 wr1) put) (main gro)
    ABS,     //  2 λ 0 λ 0 (λ 0 wr0 wr1) put
    APP, 0,  //  3
    VAR, 0,  //  5
    ABS,     //  7
    APP,     //  8
    ABS,     //  9 λ 0 λ 0 wr0 wr1
    APP, 2,  // 10
    VAR,     // 12
    IOP,     // 13
    ABS,     // 14 λ 0 wr0 wr1
    APP, 4,  // 15
    APP, 1,  // 17
    VAR,     // 19
    IOP,     // 20 wr0
    IOP, 0,  // 21 wr1
};

long ip;                // instruction pointer
long end;               // end of code pointer
int mem[TERMS];         // bss memory for terms
struct Closure *frep;   // freed closures list
struct Closure *contp;  // continuations stack
struct Closure root = {.refs = 1};
struct Closure *envp = &root;

void Gc(struct Closure *p) {
  for (; p && p != &root; p = p->envp) {
    if (--p->refs) break;
    Gc(p->next);
    p->next = frep;
    frep = p;
  }
}

void Var(void) {
  int i, x;
  struct Closure *t, *e;
  e = t = envp;
  x = mem[ip + 1];
  for (i = 0; i < x && e != &root; ++i) e = e->next;
  if (e == &root) Error(10 + x, "UNDEFINED VARIABLE %d", x);
  ip = e->term;
  envp = REF(e->envp);
  Gc(t);
}

void Gro(void) {
  int c;
  if ((c = fgetc(stdin)) != -1) {
    mem[end++] = ABS;
    mem[end++] = APP;
    mem[end++] = 4;
    mem[end++] = APP;
    mem[end++] = 2;
    mem[end++] = VAR;
    mem[end++] = 0;
    mem[end++] = ABS;
    mem[end++] = ABS;
    mem[end++] = VAR;
    mem[end++] = ~c & 1;
  } else {
    mem[end++] = ABS;
    mem[end++] = ABS;
    mem[end++] = VAR;
    mem[end++] = 0;
  }
}

void Put(void) {
  fputc('0' + (ip & 1), stdout);
  ip = 2;
}

void Bye(void) {
  int rc = mem[ip + 2];  // (λ 0) [exitcode]
  if (rc) Error(rc, "CONTINUATIONS EXHAUSTED");
  if (postdump && !rc) Dump(0, end, stderr);
  exit(0);
}

// pops continuation and pushes it to environment
void Abs(void) {
  if (!contp) Bye();
  struct Closure *t = contp;
  contp = t->next;
  t->next = envp;
  envp = t;
  ++ip;
}

struct Closure *Alloc(void) {
  struct Closure *t;
  if (!(t = frep)) {
    if (!(t = calloc(1, sizeof(struct Closure)))) {
      Error(6, "OUT OF HEAP");
    }
  }
  frep = t->next;
  t->refs = 1;
  ++heap;
  return t;
}

// pushes continuation for argument
void App(void) {
  int x = mem[ip + 1];
  struct Closure *t = Alloc();
  t->term = ip + 2 + x;
  t->envp = t->term > 21 && t->term != end ? REF(envp) : &root;
  t->next = contp;
  contp = t;
  ip += 2;
}

void Iop(void) {
  if (ip == end) {
    Gro();
  } else {
    Put();  // ip ∈ {6,13,20,21}
  }
  Gc(envp);
  envp = &root;
}

static void Rex(void) {
  switch (mem[ip]) {
    case VAR:
      Var();
      break;
    case APP:
      App();
      break;
    case ABS:
      Abs();
      break;
    case IOP:
      Iop();
      break;
    default:
      Error(7, "CORRUPT TERM");
  }
}

char GetBit(FILE* f) {
  int c;
  if ((c = fgetc(f)) != -1) c &= 1;
  return c;
}

char NeedBit(FILE* f) {
  char b = GetBit(f);
  if (b == -1) Error(9, "UNEXPECTED EOF");
  return b;
}

struct Parse Parse(int ignored, FILE* f) {
  int t, start;
  char bit, need;
  struct Parse p;
  for (need = 0, start = end;;) {
    if (end + 2 > TERMS) Error(5, "OUT OF TERMS");
    if ((bit = GetBit(f)) == -1) {
      if (!need) break;
      Error(9, "UNFINISHED EXPRESSION");
    } else if (bit) {
      for (t = 0; NeedBit(f);) ++t;
      mem[end++] = VAR;
      mem[end++] = t;
      break;
    } else if (NeedBit(f)) {
      t = end;
      end += 2;
      mem[t] = APP;
      p = Parse(0, f);
      mem[t + 1] = p.n;
      need = 1;
    } else {
      mem[end++] = ABS;
    }
  }
  p.i = start;
  p.n = end - start;
  return p;
}

void LoadRom(void) {
  long i;
  for (; end < sizeof(kRom) / sizeof(*kRom); ++end) {
    mem[end] = kRom[end];
  }
  mem[4] = 9;
  mem[1] = end - 2;
}

void Krivine(void) {
  int main;
  long gotoget;
  LoadRom();
  mem[end++] = APP;
  gotoget = end++;
  main = end;
  mem[gotoget] = Parse(1, stdin).n;
  for (;;) Rex();
}

Assembly Listing

GAS LISTING o/blc.i 			page 1


 GNU assembler version 2.34 (x86_64-alpine-linux-musl)
	 using BFD version (GNU Binutils) 2.34.
 options passed	: -aghlms=o/blc.lst
 input file    	: o/blc.i
 output file   	: o/blc.o
 target        	: x86_64-alpine-linux-musl
 time stamp    	: 2022-02-27T13:16:33.000-0800

GAS LISTING o/blc.i 			page 2


   1              	/*-*- mode:unix-assembly; indent-tabs-mode:t; tab-width:8; coding:utf-8     -*-│
   2              	│vi: set et ft=asm ts=8 tw=8 fenc=utf-8                                     :vi│
   3              	╞══════════════════════════════════════════════════════════════════════════════╡
   4              	│ Copyright 2022 Justine Alexandra Roberts Tunney                              │
   5              	│                                                                              │
   6              	│ Permission to use, copy, modify, and/or distribute this software for         │
   7              	│ any purpose with or without fee is hereby granted, provided that the         │
   8              	│ above copyright notice and this permission notice appear in all copies.      │
   9              	│                                                                              │
  10              	│ THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL                │
  11              	│ WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED                │
  12              	│ WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE             │
  13              	│ AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL         │
  14              	│ DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR        │
  15              	│ PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER               │
  16              	│ TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR             │
  17              	│ PERFORMANCE OF THIS SOFTWARE.                                                │
  18              	╚─────────────────────────────────────────────────────────────────────────────*/
  19              	
  20              	#define FASTR   0		// favor perf over tininess
  21              	#define TERMS	5000000		// number of words of bss
  22              	#define STACK	0		// bytes of stack to get
  23              	
  24              	#define IOP	0		// code for read, write0, write1, flush
  25              	#define VAR	1		// code for variable name lookup
  26              	#define APP	2		// code for applications
  27              	#define ABS	3		// code for abstractions
  28              	
  29              	#define NEXT	0*8
  30              	#define ENVP	1*8
  31              	#define REFS	2*8+0
  32              	#define TERM	2*8+4
  33              	
  34              	#define mem	%rbx
  35              	#define memd	%ebx
  36              	#define envp	%rbp
  37              	#define contp	%r9
  38              	#define frep	%r8
  39              	#define eof	%r13
  40              	#define eofb	%r13b
  41              	#define eofd	%r13d
  42              	#define idx	%r15
  43              	#define idxb	%r15b
  44              	#define idxd	%r15d
  45              	
  46              		.macro	pushpop constexpr:req register:req
  47              		.byte	0x6a,constexpr
  48              		pop	%rregister
  49              		.endm
  50              	
  51              		.macro	mxchg register:req memory:req
  52              	#if FASTR
  53              		mov	register,%rax
GAS LISTING o/blc.i 			page 3


  54              		mov	memory,register
  55              		mov	%rax,memory
  56              	#else
  57              		xchg	register,memory
  58              	#endif
  59              		.endm
  60              	
  61              		.bss
  62 0000 00000000 		.zero	TERMS
  62      00000000
  62      00000000
  62      00000000
  62      00000000
  63              		.previous
  64              	
  65 0000 7F454C46 	ehdr:	.ascii	"177ELF"
  66              	
  67              	////////////////////////////////////////////////////////////////////////////////
  68              	//	TWELVE BYTE OVERLAP		#
  69              	//	.byte	2			# EI_CLASS is ELFCLASS64
  70              	//	.byte	1			# EI_DATA is ELFDATA2LSB
  71              	//	.byte	1			# EI_VERSION is 1
  72              	//	.byte	3			# EI_OSABI is ELFOSABI_LINUX
  73              	//	.quad	0			#
  74 0004 03       	kRom1:	.byte	ABS			#  0       (λ ((0 (λ (λ ?))) ⋯))
  75 0005 02       		.byte	  APP			#  1       8
  76 0006 08       		.byte	  8			#──2──┐    -
  77 0007 02       		.byte	    APP			#  3  │    (0 (λ (λ ?)))
  78 0008 02       		.byte	    2			#──4────┐  (read (λ (λ ?)))
  79 0009 01       		.byte	      VAR		#  5  │ │  0
  80 000a 00       		.byte	      0			#  6  │ │  read
  81 000b 03       		.byte	    ABS			#──7────┘  (λ (λ ?))
  82 000c 03       		.byte	      ABS		#  8  │    (λ ?)
  83 000d 01       		.byte	        VAR		#  9  ┴    ?
  84 000e 00       		.byte	0			# exit(0) %al
  85 000f 00       		.byte	0			# elf padding                     [mark]
  86              	////////////////////////////////////////////////////////////////////////////////
  87              	
  88 0010 0200     	ehdr2:	.word	2			# e_type is ET_EXEC           [precious]
  89 0012 3E00     		.word	62			# e_machine is EM_X86_64      [precious]
  90              	
  91              	////////////////////////////////////////////////////////////////////////////////
  92              	//	FOUR BYTE OVERLAP		#
  93              	//	.long	1			# e_version is 1                  [mark]
  94 0014 58       	Bye2:	pop	%rax			# __NR_exit
  95 0015 0F05     		syscall				#
  96 0017 00       		.byte	0			# elf padding
  97              	////////////////////////////////////////////////////////////////////////////////
  98              	
  99 0018 00000000 	ehdr3:	.quad	_start			# e_entry                     [precious]
  99      00000000
 100 0020 38000000 		.quad	phdrs - ehdr		# e_phoff is 56               [precious]
 100      00000000
 101              	
 102              	////////////////////////////////////////////////////////////////////////////////
 103              	//	FOURTEEN BYTE OVERLAP		#
 104              	//	.quad	0xc681c031		# e_shoff  [should be 0]          [mark]
GAS LISTING o/blc.i 			page 4


 105              	//	.long	0xfce2abac		# e_flags  [should be 0]          [mark]
 106              	//	.word	0xc3			# e_ehsize [should be 64]         [mark]
 107 0028 57       	Get:	push	%rdi			#
 108 0029 31C0     		xor	%eax,%eax		# __NR_read
 109 002b 31FF     		xor	%edi,%edi		# stdin
 110 002d 8D73FF   		lea	-1(mem),%esi		# buf
 111 0030 0F05     		syscall				#
 112 0032 E