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!

- Download the LambdaCan software here. Follow the instructions in the tarball to build it and upload it to the Diecimila board.
- Cut a hole in the can for the Diecimila's USB connector to poke through.
- 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.
- Spraypaint the can. Let it dry.
- Put the Diecimila board into the can. The hardened expoy putty should ensure that it remains in the proper position. Close can. Done!

- You can open the can if you need to hit the board's reset button.
- Since we used the epoxy putty only to harden into a shape to accept the board and not to glue the board in place, if you want you can remove the board and use it for something else later.

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

screen /dev/ttyUSB0 9600in 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

LambdaCan source, buildable for both Arduino Diecimila and POSIX:

- (*) On bread in a can: yes, it does exist. In the early 90's my college roommates and I came into the possession of a can labelled "Brown Bread in a Can". Having never imagined such a food product, we marvelled at it in disbelief for many months before somewhat apprehensively opening the can to see what it actually contained. Predictably, it was a small loaf of brown bread. We doused the loaf in alcohol, set it on fire, and tossed the flaming mass out the window. This entire episode made sense to us at the time.
- I ported the code from an earlier Lambda Calculus reducer I had made for an older Zilog board, here. It took some significant modifications to make it fit into the Atmel ATMega168's 1KB of SRAM.

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 $