(λ-calculus ^{(revisited for dummies (like me))})

introduction

The λ-calculus (lambda calculus) is a formal system in mathematical logic and computer science for expressing computation by way of variable binding and substitution. First formulated in the 30s by Alonzo Church, the λ-calculus found early successes in the area of computability theory, such as a negative answer to Hilbert’s Entscheidungsproblem.

This is a "quasi BNF" definition of λ-calculus:

In other words, a λ-expression can be recursively defined as

1. a variable:     x is a char,
2. an abstraction: y is a variable and f an expression, 
3. an application: g is an abstraction and h an expression.

The least one can say is that these three rules are not obvious and the syntax is terse!

So, first, we will write λ-calculus expressions using the LISP explicit prefixed parenthesized syntax, more verbose (Lot of Insane Silly Parenthesis) but without any implicit priority rules difficult to memorize:

λy.f    will be written   (λ (y) f) 
gh      will be written   (g h)

Then, in order to explore some of λ-calculus expressions - ie to actually compute algorithms in realtime - we will rewrite them using the lambdatalk language, working in the current wiki, lambdatank, on top of any modern web browser. See coding for details.

We will only be interested in the construction of numbers in a language supposed to ignore them and we will successively

See also some others explorations:

1. λ-talk syntax

A λ-talk valid expression is made of:

1. words        : [^\s{}]*  // group of chars except space and {}
2. abstractions : {lambda {words} expressions}
3. applications : {abstraction expressions}

Note that:

{{lambda {:arg} :arg} Hello} 
-> Hello

((λ (y) ((λ (x) x y) A)) B) -> ((λ (y) A y) B) -> A B

We will agree to write simply

((λ (x y) x y) A B) -> A B

So, using the {λ talk} syntax we understand that

{{lambda {:a :b} :b :a} Hello World}  
-> World Hello

swaps two words. It's not magic, it's noting but a term rewriting process.

More generally {{lambda {words} expression} expression} is an Immediately Invoked Function expression, an IIFE. The inner expression {lambda {words} expression} is a special form called abstraction and evaluated in a pre-processing step to a function's reference. The outer expression - which became {function_ref expression} - is a nested form called application evaluated from inside out.

{lambda {words} expression}

λ-talk is implemented so that

Regarding rule 3.1) geeks talk about partial application or currying. About rule 3.3) they talk about variadicity. In lambdatalk lambdas can't get values from the context, a behaviour called closure by geeks. Happily the rule 3.1) helps to work arounds this weakness. As we will find out in the following.

{def name expression}

For convenience we introduce a second special form, {def name expression}, to replace (long) expressions by (short) names. For instance we can split the IIFE into two steps:

1) abstraction: give a name to the anonymous function,

{def SWAP {lambda {:a :b} :b :a}}
-> SWAP

2) application: and apply it to different words.

{SWAP hello world}
-> world hello

Note: λ-talk doesn't know closures. Lambdas are pure black boxes completely independent of any context. There are not free variables taking automatically their values from the context. If you need them you have to redefine them, manually. In fact, as the following will prove, there is a life without closures in a world where functions are first class and accept de facto a number of values lesser or greater than the number of arguments.

More can ne seen in this page coding.

2. booleans & pairs

Booleans don't exist, let's build them

{def TRUE {lambda {:a :b} :a}}
-> TRUE
{def FALSE {lambda {:a :b} :b}}
-> FALSE
{def IF {lambda {:a :b :c} {:a :b :c}}}
-> IF

{IF TRUE yes no}
-> yes
{IF FALSE yes no}
-> no

Functions can be nested, leading to powerful data and control structures. This is how the concept of pair is built in lambda-calculus (VIGRE):

[true] = λab.a        // (λ (a b) a)
[false] = λab.b       // (λ (a b) b)
[cons] = λabm.m a b   // (λ (a b m) ((m a) b))
[car]  = λp.p(λxy.x)  // (λ (p) (p [true]))
[cdr]  = λp.p(λxy.y)  // (λ (p) (p [false]))

designed with in mind:

[car]([cons]AB) -> A
[cdr]([cons]AB) -> B

This is how this can be translated in λ-talk, renaming [cons, car, cdr] as [kons, kar, kdr] in order to avoid conflicts with existant ones defined as primitives in the λ-talk's dictionary:

{def kons {lambda {:a :b :m} {:m :a :b}}}       
-> kons
{def kar  {lambda {:p} {:p TRUE}}} 
-> kar
{def kdr {lambda {:p} {:p FALSE}}}  
-> kdr

Testing:

{kar {kons A B}} -> A
{kdr {kons A B}} -> B

Note that {kons A B} is a partial application. The kons function is waiting for three values, gets only two, memorizes them in its body and returns a new function waiting for the missing one. This function will be called by kar or kdr to return the first or the last value, A or B.

3. Church numbers

In pure λ-calculus natural numbers don't exist. Alonzo Church defined [0,1,2,3,...,n] as successive functions waiting for 2 values, usually written like this:

[zero] = λfn.n        = (λ (f n) n)
[one]  = λfn.f(n)     = (λ (f n) (f n))
[two]  = λfn.f(f(n))  = (λ (f n) (f (f n)))
...

easily translated in {λ talk}

{def zero  {lambda {:f :x} :x}} -> zero
{def one   {lambda {:f :x} {:f :x}}} -> one
{def two   {lambda {:f :x} {:f {:f :x}}}} -> two
{def three {lambda {:f :x} {:f {:f {:f :x}}}}} -> three
{def four  {lambda {:f :x} {:f {:f {:f {:f :x}}}}}} -> four
{def five  {lambda {:f :x} {:f {:f {:f {:f {:f :x}}}}}}} -> five
  ... 
{def N {lambda {:f :x} {:f {:f ... {:f :x}}..}}} // N times

Calling these functions with two values displays strange strings:

{zero 0 0}  -> 0
{one 0 0}   -> ⊂0 0⊃
{two 0 0}   -> ⊂0 ⊂0 0⊃⊃
{three 0 0} -> ⊂0 ⊂0 ⊂0 0⊃⊃⊃
{four 0 0}  -> ⊂0 ⊂0 ⊂0 ⊂0 0⊃⊃⊃⊃
{five 0 0}  -> ⊂0 ⊂0 ⊂0 ⊂0 ⊂0 0⊃⊃⊃⊃⊃

It's not exactly what we want, let's imagine how 720 should be displayed! So - forgetting that we are not allowed to use any javascript number and operator - we define a function, church, translating these strange sequences into a readable decimal number:

{def church
 {lambda {:n} {:n {lambda {:x} {+ :x 1}} 0}}} 
-> church

and we get:

{church zero} -> 0
{church one}  -> 1
{church two}  -> 2
and so on...

Note: Church numbers are iterators per se so, for instance, we could build a function iterating n times a word

{def iterate
 {lambda {:n :a}
  {{:n {{lambda {:a :x} :a :x} :a}} .}}}
-> iterate 

{iterate five hello}
-> hello hello hello hello hello .

We will exploit this property in the next section.

See also OnTheRepresentationOfDataInLambdaCalculus.pdf

3. iteration ⁽¹⁾

So, a Church number N iterates N times the application of a function f on a variable x. This definition gives the basis of a first set of operators, [succ, add, mul, power] usually defined like this:

[succ]  = λnfx.f(n f x)    // (λ (n f x) (f ((n f) x)))
[add]   = λnmfx.n f(m f x) // (λ (n m f x) ((n f) ((m f) x))
[mul]   = λnmf.m(n f)      // (λ (n m f) (m (n f)))
[power] = λnm.m n          // (λ (n m) (m n))

In λ-talk we will write:

{def succ {lambda {:n :f :x} {:f {:n :f :x}}}}
-> succ
{def add {lambda {:n :m :f :x} {{:n :f} {:m :f :x}}}} 
-> add 
{def mul {lambda {:n :m :f :x} {:n {:m :f} :x}}}
-> mul
{def power {lambda {:n :m :f :x} {{:m :n :f} :x}}}
-> power

and test:

{church {succ zero}}  -> 1
{church {succ one}}   -> 2
{church {succ three}} -> 4
{church {add two three}}   -> 5
{church {mul two three}}   -> 6
{church {power three two}} -> 9

{church {power two {mul four four}}} -> 65536

4. iteration ⁽²⁾

Building "opposite" functions like prev, subtract, divide is not so easy - and Church itself avoided them in the primitive version of λ-calculus. This is where, thanks to Kleene, the concept of pairs comes in to help us... With pairs we can now build the predecessor operator. The definition given in λ-calculus:

[pred.pair] = λp.[cons](([cdr] p) ([succ](cdr p)))
[pred]  = λn.[car](n [pred.pair]([cons] 0 0))

says that pred.pair gets a pair [a,a] and returns a pair [a,a+1] ; pred computes n iterations of pred.pair starting on the pair [0,0], leading to the pair [n-1,n] and returns the first, n-1. Translated in λ-talk:

{def pred.pair {lambda {:p} {kons {kdr :p} {succ {kdr :p}}}}} 
-> pred.pair 
{def pred {lambda {:n} {kar {{:n pred.pair} {kons zero zero}}}}} 
-> pred

Some tests:

{church {pred zero}}  -> 0  // nothing exists before zero
{church {pred one}}   -> 0
{church {pred two}}   -> 1
{church {pred three}} -> 2

This is a vizualisation of the process:

[0 , 0]   = [0,0]
[0 , 0+1] = [0,1]
[1 , 1+1] = [1,2]
[2 , 2+1] = [2,3] -> pred of 3 is 2

We can now define the subtract operator. Following jwodder.freeshell.org:

SUB := λmn. n PRED m     // (λ (m n) ((n PRED) m))

{def subtract {lambda {:m :n} {{:n pred} :m}}}
-> subtract

and testing:

{church {subtract four three}} -> 1
{church {subtract one one}} -> 0

the factorial

The factorial function n! = 1*2*3*...*n uses to be introduced via recursion:

n = 0 -> factorial(0) = 1
n > 0 -> factorial(n) = n*factorial(n-1)

At this point we choose an iterative approach similar to the approach used to build the pred operator. The following definition given in λ-calculus:

[ifac.pair] = (λp.[cons]([succ]([car]p))([mul]([car]p)([cdr]p)))
[ifac] = λn.[cdr](n[ifac.pair]([cons]1 1))

says that ifac.pair gets a pair [a,b] and returns a pair [a+1,a*b]. fac computes n iterations of ifac.pair starting on the pair [1,1], leading to the pair [n,n!] and returns the second, n!.

Translated in λ-talk:

{def ifac.pair
 {lambda {:p} {kons {succ {kar :p}} {mul {kar :p} {kdr :p}}}}}
-> ifac.pair
{def ifac
 {lambda {:n} {kdr {{:n ifac.pair} {kons one one}}}}}
-> ifac

we can test:

2!  = {church {ifac two}}                -> 2
3!  = {church {ifac three}}              -> 6
4!  = {church {ifac four}}               -> 24
5!  = {church {ifac five}}               -> 120      // 55ms
6!  = {church {ifac {add three three}}}  -> 720      // 64ms 
7!  = {church {ifac {add three four}}}   -> 5040     // 167ms 
8!  = {church {ifac {add four four}}}    -> 40320    // 950ms 
9!  = {church {ifac {mul three three}}}  -> 362880   // 8700ms 
10! = {church {ifac {add five five}}}     -> 3628800 // 94600ms

This is a vizualisation of the process for 5!

[1 , 1]           = [1,1]
[2 , 1*2]         = [1,2]
[3 , 1*2*3]       = [1,6]
[4 , 1*2*3*4]     = [1,24]
[5 , 1*2*3*4*5]   = [1,120] -> 5! = 120

For the fun, this is how {ifac five} could be written replacing names, [one, five, mul, succ, kons, kar, kdr, fac.pair, fac], by their lambda expressions:

{church 
{{lambda {:n}
 {{lambda {:p} {:p 
   {lambda {:x :y} :y}}} {{:n 
    {lambda {:p}
    {{lambda {:a :b :m} {{:m :a} :b}}
     {{lambda {:n :f :x} {:f {{:n :f} :x}}}
      {{lambda {:p} {:p 
        {lambda {:x :y} :x}}} :p}}
        {{lambda {:n :m :f} {:m {:n :f}}}
         {{lambda {:p} {:p
           {lambda {:x :y} :x}}} :p}
           {{lambda {:p} {:p
             {lambda {:x :y} :y}}} :p}}}}} 
             {{lambda {:a :b :m} {{:m :a} :b}}
               {lambda {:f :x} {:f :x}}
                {lambda {:f :x} {:f :x}}}}}}
                 {lambda {:f :x} {:f {:f {:f {:f {:f :x}
}}}}}}}
-> 120

Here is an IIFE in a pure λ-calculus style!

5. recursion ⁽¹⁾

Numerous other operators/structures/combinators can be built following the same scheme as it can be seen for instance in Collected Lambda Calculus Functions. In the following we choose another way and are going to use recursion. We need nothing but a predicate function, {zero? number} returning TRUE if the number is zero else FALSE:

{def zero? {lambda {:c} {:c {TRUE FALSE} TRUE}}}
-> zero?

{zero? zero}
-> TRUE
{zero? one}
-> FALSE
{zero? two}
-> FALSE
...

Using this predicate function let's rewrite the factorial in a recursive style,

if n = 0
then fac(n) = 1
else fac(n) = n*fac(n-1)

leading to, without explanations:

{def rfac {lambda {:n}
 {{IF {zero? :n}
  {lambda {:n} one}
  {lambda {:n} {mul :n {rfac {pred :n}}}}} :n}}}
-> rfac

{church {rfac five}}
-> 120

{church {rfac {add five five}}}  // 10!
-> 3628800 // in 114830ms 

Now some explanations: replacing in rfac the two inner lambdas by #T and #F

{def #T {lambda {:n} one}}
-> #T
{def #F {lambda {:n} {mul :n {rfac {pred :n}}}}} 
-> #F

{def rfac {lambda {:n} {{IF {zero? :n} #T #F} :n}}}

we understand that for some value N:

if N = five 
then {zero? five} = FALSE
and {rfac five} = {{FALSE #T #F} five}
-> {#F five} 
-> {{lambda {:n} {mul :n {rfac {pred :n}}}} five} 
-> {mul five {FAC {pred five}}}  
-> {mul five {FAC four}}          // a recursive call 

if N = zero 
then {zero? zero} = kar
and {rfac zero} =  {{kar {kons #T #F}} zero}
-> {#T zero}
-> {{lambda {:n} one} zero}
-> one                           // the end case leading to:

{mul five {mul four {mul three {mul two {mul one one}}}}} = 120

This is a tail recursive version

{def trfac {lambda {:a :b}
  {{IF {zero? :b}
   {lambda {:a :b} :a}
   {lambda {:a :b} {trfac {mul :a :b} {pred :b}}}} :a :b}}}
-> trfac

{church {trfac one five}}
-> 120

{church {trfac one {add five five}}}
-> 3628800  // in 51173ms

So, trfac is twice as fast as rfac and ifac. But it still very slow, because the Church encoding is a smart but very primitive way to represent numbers which quickly brings the computer to its knees. See how λ-calculus using binary numbers of variable length breaks the glass ceiling.

6. recursion ⁽²⁾

Let's explore some new algorithms

div, mod & gcd

{def divide                          
  {lambda {:a :b}
   {{IF {zero? {subtract :b :a}}
    {lambda {:a :b} {add one {divide {subtract :a :b} :b}}}
    {lambda {:a :b} zero} } :a :b}}}
-> divide 

{def mod                            
 {lambda {:a :b}
  {subtract :a {mul {divide :a :b} :b}}}}
-> mod

{def gcd
 {lambda {:a :b}
  {{IF {zero? :b} 
   {lambda {:a :b} :a}
   {lambda {:a :b} {gcd :b {mod :a :b}}}} :a :b}}}
-> gcd

{church {divide five two}}
-> 2
{church {mod five two}}
-> 1

{church {gcd four two}}
-> 2
{church {gcd {fac five} three}}
-> 3

fibonacci

{def fib
 {lambda {:a :b :n}
  {{IF {zero? :n}
   {lambda {:a :b :n} :a}
   {lambda {:a :b :n} {fib {add :a :b} :a {pred :n}}}}
   :a :b :n}}}
-> fib

{church {fib zero one {add five five}}}
-> 55
-> {church {fib zero one {mul five five}}}
-> 75025

the Towers of Hanoï

{def hanoi
 {lambda {:n :from :to :via}
  {{IF {zero? :n}
   {lambda {:n :from :to :via} }
   {lambda {:n :from :to :via}
    {hanoi {pred :n} :from :via :to}
      {br} move disc {church :n} from tower :from to tower :to 
    {hanoi {pred :n} :via :to :from} 
   }} :n :from :to :via}}}
-> hanoi

Testing

{hanoi four A B C}
->  
 move disc 1 from tower A to tower C  
 move disc 2 from tower A to tower B  
 move disc 1 from tower C to tower B  
 move disc 3 from tower A to tower C  
 move disc 1 from tower B to tower A  
 move disc 2 from tower B to tower C  
 move disc 1 from tower A to tower C  
 move disc 4 from tower A to tower B  
 move disc 1 from tower C to tower B  
 move disc 2 from tower C to tower A  
 move disc 1 from tower B to tower A  
 move disc 3 from tower C to tower B  
 move disc 1 from tower A to tower C  
 move disc 2 from tower A to tower B  
 move disc 1 from tower C to tower B

the Hilbert curve

{def left
 {lambda {:d :n}
  {{IF {zero? :n}
   {lambda {:d :n} }
   {lambda {:d :n} T90      {right :d {pred :n}}
                   M:d T-90 {left  :d {pred :n}}
                   M:d      {left  :d {pred :n}}
                   T-90 M:d {right :d {pred :n}}
                   T90
   }} :d :n}}}
-> left
{def right
 {lambda {:d :n}
  {{IF {zero? :n}
   {lambda {:d :n} }
   {lambda {:d :n} T-90    {left  :d {pred :n}}
                   M:d T90 {right :d {pred :n}}
                   M:d     {right :d {pred :n}}
                   T90 M:d {left  :d {pred :n}}
                   T-90
  }} :d :n}}}
-> right

Testing

{left 10 one}
-> T90  M10 T-90  M10  T-90 M10  T90

{left 10 two}
-> T90 T-90  M10 T90  M10  T90 M10  T-90 M10 T-90 T90  M10 T-90  M10  T-90 M10  T90 M10 T90  M10 T-90  M10  T-90 M10  T90 T-90 M10 T-90  M10 T90  M10  T90 M10  T-90 T90

{left 10 three}
-> T90 T-90 T90  M10 T-90  M10  T-90 M10  T90 M10 T90 T-90  M10 T90  M10  T90 M10  T-90 M10 T-90  M10 T90  M10  T90 M10  T-90 T90 M10 T90  M10 T-90  M10  T-90 M10  T90 T-90 M10 T-90 T90 T-90  M10 T90  M10  T90 M10  T-90 M10 T-90 T90  M10 T-90  M10  T-90 M10  T90 M10 T90  M10 T-90  M10  T-90 M10  T90 T-90 M10 T-90  M10 T90  M10  T90 M10  T-90 T90 M10 T90 T-90  M10 T90  M10  T90 M10  T-90 M10 T-90 T90  M10 T-90  M10  T-90 M10  T90 M10 T90  M10 T-90  M10  T-90 M10  T90 T-90 M10 T-90  M10 T90  M10  T90 M10  T-90 T90 T-90 M10 T-90 T90  M10 T-90  M10  T-90 M10  T90 M10 T90 T-90  M10 T90  M10  T90 M10  T-90 M10 T-90  M10 T90  M10  T90 M10  T-90 T90 M10 T90  M10 T-90  M10  T-90 M10  T90 T-90 T90

three sequences of words which can be used by a turtle graphic tool - understanding the T+/-90 and M10 commands - to display the first three of the following Hilbert curves:

See also fromroots2canopy or coding.

7. Y-combinator

It may be interesting to know that all these recursive algorithms can be written as true λ calculus expressions exclusively made of words, abstractions and applications. In other words we must forget definitions. But a recursive function calls its name inside its body and we will rewrite it as an almost-recursive one, arfac, without any name's reference and call the function using some Y-combinator acting as a bridge. Let's apply this process to the factorial function:

{def Y {lambda {:f} {:f :f}}}  // see mockingbird below
-> Y

{def arfac {lambda {:f :n}
  {{IF {zero? :n} 
   {lambda {:f :n} one}
   {lambda {:f :n} {mul :n {:f :f {pred :n}}}}
  } :f :n}}}
-> arfac

{church {{Y arfac} five}}
-> 120

We can compose Y and arfac into Yarfac:

{def Yarfac
 {lambda {:n}
  {{{lambda {:f} {:f :f}}
   {lambda {:f :n}
    {{IF {zero? :n}
     {lambda {:f :n} one}
     {lambda {:f :n} {mul :n {:f :f {pred :n}}}}
    } :f :n}}} :n}}}
-> Yarfac

{church {Yarfac five}}
-> 120

and even forget the name Yarfac, building an IIFE:

{church
 {{lambda {:n}
  {{{lambda {:f} {:f :f}}
   {lambda {:f :n}
    {{IF {zero? :n}
     {lambda {:f :n} one}
     {lambda {:f :n} {mul :n {:f :f {pred :n}}}}
    } :f :n}}} :n}} five}}
-> 120

It is left to the reader to patiently replace the names by their lambda expressions leading to the nested expression displayed at the end of section 4. In a pure λ-calculus style!

See also mockingbird and stackoverflow

This is a variant of Y avoiding duplication of :f in the body of arfac

{def YY
 {lambda {:h}
  {{{lambda {:h :x}
     {:h {{lambda {:x :a} {{:x :x} :a}} :x} }} :h}
   {{lambda {:h :x} 
     {:h {{lambda {:x :a} {{:x :x} :a}} :x} }} :h}}}}
-> YY

{def arfac2 {lambda {:f :n}
  {{IF {zero? :n} 
   {lambda {:f :n} one}
   {lambda {:f :n} {mul :n {:f {pred :n}}}}
   } :f :n}}}
-> arfac2

{church {{YY arfac2} five}}
-> 120

A matter of choice.

conclusion

We have seen that, using nothing but Church numbers and pairs, we can compute 1*2*3*4*5*.... No booleans, no if then else control structure, no loop structure or any magic Y combinator. How is it possible to do such a miracle? Maybe because Church numbers and pairs contain all that stuff!

A perfect example of the equivalence of code and data. Homoiconicity as they say!

Note 1: every results in this page, even the last value 10! = 3628800, are actually computed with λ-talk, reduced to its bare foundation, the λ-calculus. Just open the editor frame of this page to read, edit and test all algorithms in real time.

Note 2: λ-talk doesn't follow the walk(tree(token(str))) evaluation approach and is based on a single regular expression, /\{([^\s{}]*)(?:[\s]*)([^{}]*)\}/g, evaluating in a single loop the code, which is all along a simple flat string made of words. Something like a Turing stripe/machine.

Note 3: Church numbers could be seen as tiny CPUs, small primitive engines ready to iterate. Not dead datas stored in a memory and sequentially given to some CPU iterating on them, but an arborescent structure of CPUs interacting in a de facto parallel process. Maybe it's how Google's data centers work.

Maybe it's how our brain works, full of Church neurons. Why not ?

Don't blame me, I'm joking.

Alain Marty, 2016/05/01, updated on 2020/02/03, on 2021/11/10 and on 2024/0727

references