[picture of Ulambda]

John's
Lambda Calculus
and
Combinatory Logic
Playground

    000100011001100101000110100
     000000101100000100100010101
     11110111          101001000
     11010000          111001101
     000000000010110111001110011
     11111011110000000011111001
     10111000
     00010110
    0000110110    [picture of Primes]

  0011010100 0101000101 0001000001
  0100000100 0101000100 0001000001
  0100000100 0101000001 0001000001
  0000000100 0101000101 0001000000
  0000000100 0100000101 0000000001
  0100000100 0001000100 0001000001
  0100000000 0101000101 0000000000
  0100000000 0001000101 0001000001
  0100000000 0100000100 0001000001
  0100000100 0101000000 0001000000
  ...

Pictured above you can see on the left the 206 bit binary lambda calculus (blc) self-interpreter in graphical notation, and on the right a 167 bit primes program, in both binary and graphical notation, together with the first 300 bits of output. You can run this right away by feeding primes.blc into the tiny blc interpreter in perl with

  perl blc.pl -b < primes.blc | head -c 300
(Outputting much more than 300 bits in Perl will land your computer in swap hell.) or into the blc interpreter in C with
  cc -DM=999999 -m32 -std=c99 uni.c -o uni
  ./uni -b < primes.blc | head -c 1024
Option -b denotes bit-oriented IO rather than the default byte-oriented mode. An obfuscated version of this interpreter won as Most functional in the 2012 International Obfuscated C Code Contest.

Binary lambda calculus is explained in detail in my latest paper available in PostScript and PDF, and in somewhat less detail in Wikipedia.

Inspired by an April 13, 2008 FP Lunch blog by Thorsten Altenkirch, I was able to improve the constant in the symmetry-of-information theorem from 1876 down to 1636, and again on Mar 3, 2009 down to 1388. On September 3, 2011, Bertram Felgenhauer came up with a monadic evaluator that allows one to keep track of the bits of input read so far, which avoids the need for symbolic reduction, and cut the constant all the way down to 667 bits. Bertram also improved the brainfuck interpreter by 64 bits.

On Mar 10, 2009, I determined the first 4 bits of the halting probability: .0001. On June 17, 2011, following a suggestion by Chris Hendrie, I changed the integer/string correspondence to avoid reversing. This big-endian representation makes lexicographic order on delimited numbers coincide with numeric order.

In March 2012 I worked out this simplest stepwise lambda calculus reducer, a necessary ingredient in a proof of the Symmetry of Information theorem.

This design of a minimalistic universal computer was motivated by my desire to come up with a concrete definition of Kolmogorov Complexity, which studies randomness of individual objects. All ideas in the paper have been implemented in the the wonderfully elegant Haskell language, which is basically pure typed lambda calculus with lots of syntactic sugar on top. An example session:

# alias uni8="./blc run8 uni8.lam"
# cat > stutter.lam
let
  stutter = \l l(\c\r\d\z z c (\z z c (stutter r)))l
in stutter
^D
# make stutter.Blc
./blc Blc stutter.lam > stutter.Blc
# od -Ad -x stutter.Blc
0000000 8446 0016 c25b 3fdf 9ade
0000010
# cat stutter.Blc - | uni8
hello
hheelllloo

# make primes.Blc
./blc Blc primes.lam > primes.Blc
# od -Ad -x primes.Blc
0000000 9911 8046 2458 de57 a191 00cd ce2d 787f
0000016 cd07 b0c0 006c
0000021
# cat primes.Blc - | uni8 | head -c 50
00110101000101000101000100000101000001000101000100
# make bf.Blc
./blc Blc bf.lam > bf.Blc
# wc bf.Blc
  0   2 104 bf.Blc
# cat hw.bf
# ++++++++++[>+++++++>++++++++++>+++>+<<<<-]>++.>+.+++++++..+++.>++.<<+++++++++++++++.>.+++.------.--------.>+.>.]
# cat bf.Blc hw.bf | uni8
Hello World!
showing a 10 byte program for ``stuttering'', a 21 byte program for primes, and a 104 byte Brainfuck interpreter.

This online course at Oberlin College provides a very readable introduction to combinators. Colin Taylor has written a very similar interpreter for the Lambda Calculus, while Gregory Chaitin, promotor of algorithmic information theory, wrote one for LISP. The Unlambda Programming Language is a combinator based language with input, output, delayed evaluation, and call-with-current-continuation. Interpreters have been written in many languages, including c, java, perl, scheme, SMLNJ, CAML, and even in unlambda itself! Recently, Ben Rudiak-Gould (benrgATdarkDOTdarkwebDOTcom) made available a most comprehensive combinatory logic interpreter, using Church numerals for character encodings. By tying the combinator code to standard input/output, his Lazy K language supports familiar utilities such as sort! To top it off, he provides a compiler (itself written in Scheme) from (a subset of) Scheme into Lazy K. Chris Barker also has several pages of interest, including a Lambda tutorial and some highly minimalistic languages.


Before discovering how to interpret lambda calculus in binary, I figured out how to make a universal machine in binary combinatory logic. The former turns out to be a lot more descriptive, i.e. generally needing fewer bits. But for historical interest, I keep this old applet here: Actually, it slows down page loading too much, so I comment it out.

This program is an interpreter for the simplest language possible: both functions and data are represented by combinators, built up from S and K by application. The primitive combinators are defined by

Combinator identifiers are all a single character. Apart from the primitive combinators S and K, the interpreter has the following predefined combinators: In the text input field, you can enter definitions such as the above, or combinations to be evaluated. In case the result is too large to be shown in detail, parts of it are shown as asterisks. If the result can be interpreted as a list, this is shown as an output string with bits 0,1 and again asterisks indicating non-bit elements. An example session is (input lines shown with a > prompt):
> 2fx=f(fx)
defines 2 as (S(S(KS)K)I)
> 222(P0)$
of size 46
head reduces in 53 steps to S(S(K(S(SKK)))KK)(K(SKK(S(K(S(*K)))K)(SKK(S(K(*K))(SKK(S(*)K)))(SKK(S(K(*))(*K(*(*))))(SKK(S(*)(*(*)))(KK)))))) of size 167
outputs 16 bits "0000000000000000"