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

On Pi day 2023 I gave an online talk about AIT and BLC based on these slides.

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

  cc -O uni.c -o uni
  ./uni -b < primes.blc

Binary lambda calculus is explained in detail in my latest paper available in PostScript and PDF, and in somewhat less detail in this former Wikipedia entry ported to gist.

I recently proposed a functional Busy Beaver which led to this OEIS entry.

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!

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.

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

• Kxy=x
• Sxyz=xz(yz)

• I=SKK
• Y=SSK(S(K(SS(S(SSK))))K)
• Pxyz=zxy
• 0xy=x
• 1xy=y
• ?$=0
• ?(Pxy)=1

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