Lambda crocodiles

Introduction

Bret Victor has invented a game where the rules of lambda calculus are realized by alligators eating each other. I have implemented this system in Haskell, and with crocodiles. To play with it, simply download this file and run ghci croco.hs.

In the following I briefly describe the rules of the game and the usage of the program, and I present a few things you can do with crocodile calculus. The game is to figure out these things for yourself, so: Spoiler alert!

And that's how it's done

The program displays the families of crocodiles as ASCII-graphics. This here is a hungry crocodile guarding its egg:

-+-°<
 O

To make it, I entered Croco[Egg 0] at the ghci prompt.

Here is a hungry crocodile that guards its somewhat more complex family (The eggs are connected with the crocodiles they belong to):

----+----°<
-+--|-°<
 O  O

For this crocodile family I had to enter Croco[Croco[Egg 0, Egg 1]]. This means: A hungry crocodile guarding a hungry crocodile that guards two eggs, where the first egg belongs to the hungry crocodile directly above it (0 hungry crocodiles in between), while there is one hungry crocodile between the second egg and its mother (Hence the 1 behind the second Egg).

An old crocodile does not have any own eggs, does not eat and just guards its family. If I enter Old[Croco[Croco[Egg 0, Egg 1]], Croco[Egg 0, Egg 0]], I get the following graphic:

=====================
----+----°< -+--+-°< 
-+--|-°<     O  O    
 O  O

Eating and Hatching

If there are several crocodiles next to each other in the same family, the leftmost crocodile (provided it is hungry) eats its right neighbour including family:

=====================
----+----°< -+--+-°< 
-+--|-°<     O  O   
 O  O

Subsequently it dies from overeating and disappears. But from each of its eggs (here just one) hatches a whole family identical to the one that was just eaten:

===============
-+----------°< 
 O -+--+-°<    
    O  O       

The old crocodile now has fulfilled its purpose, as its family can now fend for itself (On the topmost level, it consists of only a single crocodile), so the old crocodile dies. All that remains is:

-+----------°< 
 O -+--+-°<  
    O  O      

With the Haskell program, these rules can be applied automatically. The command

sim 3 [Croco[Croco[Egg 0, Egg 1]], Croco[Egg 0, Egg 0]]

simulates three steps (Eating and hatching, or the dying of an old crocodile) and produces the output

=====================
----+----°< -+--+-°< 
-+--|-°<     O  O    
 O  O                

===============
-+----------°< 
 O -+--+-°<    
    O  O       

-+----------°< 
 O -+--+-°<    
    O  O       

The old crocodile has been inserted automatically, because the second parameter of sim is a list of families, which needs to be combined into a single family for simulation.

Data types

It turns out you can represent diverse data type with crocodile families. Of course, all crocodile families are functions: Eating just means take as argument and eggs are parameters. Old crocodiles are parentheses. But in principle, you can encode any data type as a function/crocodile family.

Truth values

The easiest data to encode as functions are the truth values true and false. They each consist of two crocodiles that will eat two crocodile familes, where true will leave as the final output only the first eaten family, whereas false leaves the second. The families look accordingly:

true:

-+----°< 
-|-°<    
 O   

false:

------°< 
-+-°<    
 O     

These two crocodile families are predefined in the program under the names true and false.

Why are those the truth values? Because you can use them easily to implement an if function: The application of a truth value to two values is the if function! If you feed two alternatives to a truth value, the result is the first alternative if the truth value was true, and the second alternative if it was false.

Natural numbers

Natural numbers are encoded as functions according to the system of Church numerals: A crocodile family representing a natural number n eats a family f and a family o. The result is a situation where the family f is applied n times in a row to o. We may interpret o as initial value and f as successor function. Alternatively, we can interpret the Church-encoding of the number n as a higher-order function that takes a single function f as its argument and returns a function that corresponds to the n-fold composition of f with itself, for example with n=5 it returns f⁵=f∘f∘f∘f∘f.

This is how the crocodile families for the numbers from 0 to 4 look like:

------°< 
-+-°<    
 O    
 
-+-------°< 
-|--+-°<    
 O  O  

-+--+-------°< 
-|--|--+-°<    
 O =|==|=      
    O  O  

-+--+--+-------°< 
-|--|--|--+-°<    
 O =|==|==|=      
    O =|==|=      
       O  O      

-+--+--+--+-------°< 
-|--|--|--|--+-°<    
 O =|==|==|==|=      
    O =|==|==|=      
       O =|==|=      
          O  O    

In the program, you can generate the number crocodile families by applying the function number to ordinary Haskell integers.

Arithmetic operations

Addition is a fairly simple arithmetic operation, but it is more complex than multiplication and powers when calculating with crocodiles. Here is the crocodile family for addition, available in the program under the name plus:

-+----------------------°< 
-|-----+-------------°<    
-|--+--|--+-------°<       
-|--|--|--|--+-°<          
 O  O =|==|==|=            
       O  O  O    

What does it mean? Essentially the following: Eat two numbers, a successor function and an initial value. Then let one number eat the successor function and the initial value. Then let the other number eat the successor function and the result of the previous gluttony.

Because the last two arguments of the the addition function are interpreted as successor function and initial value, the result after eating the first two arguments is already number crocodile family, that then proceeds to eat the last two arguments. Thus we can interpret plus as a function with two parameters that returns a number. Hence plus is a binary prefix operator.

The infix operator version of addition is simply the functions that turns a natural number into its successor:

----+-------------°< 
-+--|--+-------°<    
-|--|--|--+-°<       
 O =|==|==|=         
    O  O  O   

If you feed this crocodile family and a number family m to a number family n, then this (+1) function will be applied n times to m, giving m+n.

Infix minus works (with restrictions) quite similarly, only that you use the function that turns each natural number into its predecessor (and zero to zero). As a crocodile family, it looks like this:

-+----------------------------------°< 
-|--------+----------------------°<    
-|--------|--------+----------°<       
 O ----+--|----°< -|-°< -+-°<          
   -+--|--|-°<     O     O             
    O =|==|=                           
       O  O                            

The aforementioned restrictions are:

1. You cannot get negative numbers. Instead, the result is 0. Negative numbers cannot even be represented with simple Church numerals.
2. The order of operands is swapped with respect to ordinary minus. That's why in the program I called this crocodile family sunim.

The multiplication function is simpler than the previous operators:

-+-------------°< 
-|--+-------°<    
-|--|--+-°<       
 O =|==|=         
    O  O    

It is easiest to understand if you interpret the numbers as higher-order functions that iterate a given function the appropriate number of times. So the multiplication family eats three families: A number m, a number n and a function f. The function is fed to n, so it is iterated n times, thus the intermediate result is fⁿ. This is subsequently passed to m and is iterated m times: (fⁿ)^m = f^n·m. The multiplication function is available under the name times.

The most simple arithmetic operation is the power function, available in the program under the name power:

----+----°< 
-+--|-°<    
 O  O    

It simply eats two numbers and feeds the first (b for base) to the second (e for exponent). To understand it, you should imagine what the result does to a function f. This function f plays the role of the initial value for e, while b takes the role of the successor function. b applied once to f is f^b, thus f iterated b-fold. b applied twice to f is (f^b)^b=f^b2, and so on. Now e applies b e times to f, so we get f^be. Thus the result of power (number b) (number e) is the number crocodile family for b^e. Except if e=0, then it does not work.

Tuples

Tuples (a, b, c, ...) can in general be represented as crocodile families like this:

-+---------------°<
 O  a  b  c  ...

An n-tuple eats a function taking n parameters and applies that function to the elements of the tuple. To read-access a tuple, you have to pass it the action you want to do with its elements. For example, to get the first element of a pair you pass it true, and for the second element false. A crocodile family that constructs a pair from two arguments is available in the program under the name pair.

Alternatives

An element of a disjoint union of data types T and U is either an element t of T or an element u of U, together with the information which of both it is. As a crocodile family this may be represented thus:

-+-------°<    
-|----°<       
 O  t   

---------°<    
-+----°<       
 O  u   

Such a family is fed two functions: The first for the case that it is an element of T and the second for the case that it is an element of U. The program defines the crocodile families left and right, which each eat a value and wrap it as an element of T or U, respectively.

Recursive functions

This is the crocodile family with the name indigestible:

-+-----------+----------°< 
-|--+--+-°< -|--+--+-°<    
 O =|==|=    O =|==|=      
    O  O        O  O   

If you feed it a crocodile family f, you get something that is returned unchanged by f: (indigestible f) = (f (indigestible f)) = (f (f (indigestible f)))...

We are dealing here with a so-called fixed-point combinator. Using it, we can define recursive functions, for example the factorial function:

============================================================
indigestible --------------------------------+------------°<
             --------+--------------------+--|--------+-°<
             isZero  O  (number 1) =======|==|========|=
                                   times  O =|========|=
                                             O =======|=
                                               sunim  O

where isZero is defined as

-+----------------------°< 
 O ---------°< -+----°<    
   ------°<    -|-°<       
   -+-°<        O          
    O  

f in this case is the family that is fed to indigestible. Subsequently, indigestible feeds (indigestible f) to f, thus (indigestible f), which is the factorial function, is available for the evaluation of f: Recursion!

However, using my program to calculate something as simple as 3! takes a long time. This is because the order of the eating steps is chosen unfavorably, so that huge intermediate results arise.