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!

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

at the ghci prompt.`Croco[Egg 0]`

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

.
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 `Croco[Croco[Egg 0, Egg 1]]`

).
`Egg`

An old crocodile does not have any own eggs, does not eat and just guards its family.
If I enter

, I get the following graphic:`Old[Croco[Croco[Egg 0, Egg 1]], Croco[Egg 0, Egg 0]]`

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

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.

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.

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 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*^{5}=*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.

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:

- You cannot get negative numbers. Instead, the result is 0. Negative numbers cannot even be represented with simple Church numerals.
- 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 ^{n}*. This
is subsequently passed to

`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

`power (number `*b*) (number *e*)

is the number crocodile family for Tuples (*a*, *b*, *c*, ...) can in general be represented as crocodile families like this:

-+---------------°< Oa 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`

.

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:

-+-------°< -|----°< Ot---------°< -+----°< Ou

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.

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.

Contact and legal info
| © 2016-07-31 injamben.de