Project LambdaCan

Lambda Calculus in a Can

(Arduino board mountedin can)

You can get soup in a can. You can get bread in a can (*). Now the long wait is over! You can finally get Lambda Calculus in a can.

Project LambdaCan is an amusing exercise in absurdity. It implements a reducer (interpreter) for the Lambda Calculus, a formal system (programming language) developed by Alonzo Church in the 1930's to attack the deepest mathematical problem of the day. This was the Entscheidungsproblem, the question of whether or not there exists an algorithm capable of deciding the truth or falsehood of all statements in mathematics.

Project LambdaCan takes this tool for exploring the most profound mathematical problems and implements it on a microcontroller better suited to the most mundane of tasks, like running a vending machine or microwave oven. And it sticks the microcontroller in a can that you can connect to your PC using a USB cable.

Of course, the extreme overhead involved in supporting the painfully abstract Lambda Calculus notation makes LambdaCan struggle to compute arithmetic as simple as 11 + 12 = 23. The microcontroller would perform much better if programmed in its native language. Furthermore, the very idea of plugging a LambdaCan coprocessor into a typical PC to perform computations is absurd since the PC could undoubtedly handle much larger computations faster on its own.

But... hey, it's Lambda Calculus in a can!

Build your own LambdaCan

(Components used in Project LambdaCan) LambdaCan is essentially an Arduino Diecimila board mounted in a cough drop can using epoxy putty. The Diecimila board uses an Atmel ATmega168 microcontroller with 16KB of flash RAM and 1KB of SRAM. It is a favorite of the microcontroller hacking community with plenty of Free software support available online. Here are the steps:
  1. Download the LambdaCan software here. Follow the instructions in the tarball to build it and upload it to the Diecimila board.
  2. Cut a hole in the can for the Diecimila's USB connector to poke through.
  3. Put the Diecimila board in a small plastic bag. Cover the bottom edges of the can with epoxy putty. While the putty is still soft, mash the plastic-wrapped Diecimila board into it until the board is in position with its USB connector poking out of the hole in the can. The plastic bag will keep the sticky epoxy off of your board. Remove the board and let the epoxy putty harden. Discard the plastic bag.
  4. Spraypaint the can. Let it dry.
  5. Put the Diecimila board into the can. The hardened expoy putty should ensure that it remains in the proper position. Close can. Done!
FYI:

Using LambdaCan

(LambdaCan in action)

To use LambdaCan, boot your favorite GNU/Linux machine and then plug LambdaCan in to a free USB port. Run

screen /dev/ttyUSB0 9600
in a shell to interact with LambdaCan. Alternately, the instructions included with the source can tell you how to build a POSIX version of the software that you can run in a shell without needing the LambdaCan hardware.

The syntax of the Lambda Calculus is very simple: it has variables like x and functions like (\x.x). This function, for example, takes one argument x and returns the value of that argument---it's the identity function. In Church's original syntax, the \ would be a lambda. The period is a little syntactic sugar to make the function more readable by visually separating parameters from body. The Lambda Calculus also includes applications of functions. For example, ((\x.x) A) applies the above identity function to the argument A. Reducing expressions, at least in the simplest cases, amounts to syntactically substituting arguments for formal parameters in function bodies, like so:

>> ((\x.x) A);;
-> A
\>

To reduce, we match the argument A with the formal parameter x, and then replace all occurrences of x in the body with A. The -> symbol indicates one step of reduction, the \> symbol indicates no further reduction is possible.

Here's the formal grammar LambdaCan uses. Note that you can put spaces and carriage returns anywhere you want, but you must end your input with ;;

START    ::= FORMULA ';;'

FORMULA  ::= VARIABLE
         |   '(' FORMULA FORMULA ')'
         |   '(' '\' VARIABLE '.' FORMULA ')'

VARIABLE ::= [A-Z,a-z]

In it's most basic form, there are no numbers or strings in the Lambda Calculus---only functions. However, you can invent conventions on how to encode numbers as functions. One such convention called "Church numerals" encodes numbers as follows:

0 = (\s.(\z.z))
1 = (\s.(\z.(s z)))
2 = (\s.(\z.(s (s z))))

Every number is represented by a distinct function of two arguments: s and z. The number of applications of s encodes the numeric value: zero for 0, one for 1, two for 2 and so on. Using this convention, you encode the operation M + N as follows:

(\M.(\N.(\s.(\z.(M (s (N (s z))))))))

So when asked to calculate 1 + 1 = 2, LambdaCan produces the following output:

>> ((
>> (\M.(\N.(\s.(\z.((M s) ((N s) z))))))
>> (\s.(\z.(s z))))
>> (\s.(\z.(s z))))
>> ;;
-> ((\N.(\s.(\z.(((\s.(\z.(s z))) s) ((N s) z))))) (\s.(\z.(s z))))
-> (\s.(\z.(((\s.(\z.(s z))) s) (((\s.(\z.(s z))) s) z))))
-> (\s.(\z.(((\s.(\z.(s z))) s) ((\z.(s z)) z))))
-> (\s.(\z.(((\s.(\z.(s z))) s) (s z))))
-> (\s.(\z.((\z.(s z)) (s z))))
-> (\s.(\z.(s (s z))))
/>
Nodes used:
        40
Vars used:
        MNsz

Here is 11 + 12 = 23, a computation that uses nearly all of the LambdaCan's available memory:

((
(\M.(\N.(\s.(\z.((M s) ((N s) z))))))
(\s.(\z.(s (s (s (s (s (s (s (s (s (s (s z))))))))))))))
(\s.(\z.(s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))))))
;;

-> ((\N.(\s.(\z.(((\s.(\z.(s (s (s (s (s (s (s (s (s (s (s z))))))))))))) s) ((N s) z))))) (\s.(\z.(s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))))))
-> (\s.(\z.(((\s.(\z.(s (s (s (s (s (s (s (s (s (s (s z))))))))))))) s) (((\s.(\z.(s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))))) s) z))))
-> (\s.(\z.(((\s.(\z.(s (s (s (s (s (s (s (s (s (s (s z))))))))))))) s) ((\z.(s (s (s (s (s (s (s (s (s (s (s (s z))))))))))))) z))))
-> (\s.(\z.(((\s.(\z.(s (s (s (s (s (s (s (s (s (s (s z))))))))))))) s) (s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))))))
-> (\s.(\z.((\z.(s (s (s (s (s (s (s (s (s (s (s z)))))))))))) (s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))))))
-> (\s.(\z.(s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))))))))))))))))
/>
Nodes used:
        124
Vars used:
        MNsz

Download

LambdaCan source, buildable for both Arduino Diecimila and POSIX:

Notes:


View this page in Romanian thanks to Aleksandra Seremina.

Tim Fraser's homepage at the WPI alumni site

$Id: lambdacan.html,v 1.4 2008-02-01 23:03:13 tim Exp modded 19 Nov 2012 $