[picture of Ulambda]

John's
Lambda Calculus
and
Combinatory Logic
Playground

[picture of Ucomb]

Pictured above you can see on the left the 210 bit binary lambda calculus self-interpreter, and on the right the 272 bit binary combinatory logic self-interpreter Both are explained in detail in my latest paper available in PostScript and PDF, and in somewhat less detail in Wikipedia. Inspired by an April 13 FP Lunch blog by Thorsten Altenkirch, I was able to improve the constant in the symmetry-of-information theorem from 1876 down to 1636. On Mar 3 2009 I further reduced the constant down to 1388! And on Mar 10, I determined the first 4 bits of the halting probability: .0001! 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 uni="./blc u8 @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 2162 0068 43da fcfb 597b
0000010
# uni @stutter.Blc++stdin
hello
hheelllloo

# od -Ad -x bf.Blc
0000000 8a22 8085 6061 06a0 2041 a67a fa7f 6001
0000016 fea8 77a8 03a0 16ed 48e8 02c5 0341 a7d0
0000032 ea41 8fdf 834e 7fa9 bbf4 eb74 fd2f fd33
0000048 1c00 fea8 a168 1efd a180 147e f7da f3f4
0000064 187f 7ff9 c538 5002 0b15 4034 bf4f b06f
0000080 50f2 efbf c3e1 3973 fc2a fc3f 3c3f 3c3c
0000096 973c 6a85 ef00 c536 b402 dde9 c152 1739
0000112 1738 b068 0041
0000117
# cat hw.bf
# ++++++++++[>+++++++>++++++++++>+++>+<<<<-]>++.>+.+++++++..+++.>++.<<+++++++++++++++.>.+++.------.--------.>+.>.]
# uni @bf.Blc++@hw.bf
Hello World!
showing a 10 byte program for ``stuttering'', and a 117 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. A LISP interpreter based on a combinatory logic graph reduction engine can be found here. 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:

This 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"