[picture of Ulambda]

John's
Lambda Calculus
and
Combinatory Logic
Playground

    000100011001100101000110100
     000000101100000100100010101
     11110111          101001000
     11010000          111001101
     000000000010110111001110011
     11111011110000000011111001
     10111000
     00010110
    0000110110

  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 210 bit binary lambda calculus (blc) self-interpreter, and on the right a 167 bit primes program 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 < primes.blc | head -c 300
(Outputting much more than 300 bits runs will land your computer in swap hell.)

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. 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.

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 m8 uni8.lam"
# cat stutter.lam
let
  stutter = \l l(\c\r\d\z z c (\z z c (stutter r)))l
in stutter
# make stutter.Blc
./blc B stutter.lam > stutter.Blc
# od -Ad -x stutter.Blc
0000000 8446 0016 c25b 3fdf 9ade
0000010
# cat stutter.Blc - | uni 8
hello
hheelllloo

# make primes.Blc
./blc B 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 B bf.lam > bf.Blc
# od -Ad -x bf.Blc
0000000 5144 01a1 5584 02d5 70b7 2230 32ff 00f0
0000016 f9bf 7f85 e15e 956f 7d7f c0ee 54e5 0068
0000032 5558 fbfd 45e0 fd57 fbeb b6f0 2ff0 07d6
0000048 6fe1 d773 14f1 c0bc ff0b 1f2e 6fa1 1766
0000064 5be8 2fef ffcf ff13 cae1 2034 c80a 0bd0
0000080 ee99 e51f 7fff 6a5a ff1f ff0f 9d87 d004
0000096 00ab db05 4023 3bb7 cc28 b0c0 0e6c 1074
0000112
# 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 112 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"