{λ way}

user:anonymous

{img {@ src="data/escher-stairs.jpg" width="100%" title="Escher stairs"}}

_h1 λ-calc {sup {i (in λ-talk)}}

{center ( See also [[calc2talk]], [[turing]] )}

{blockquote {center Feel free to write a comment in [[forum]].}}
{hr}
{blockquote
{b 6!} = ((λ (:n) ((λ (:p) (:p (λ (:x :y) :y))) ((:n (λ (:p) ((λ (:a :b :m) ((:m :a) :b)) ((λ (:n :f :x) (:f ((:n :f) :x))) ((λ (:p) (:p (λ (:x :y) :x))) :p)) ((λ (:n :m :f) (:m (:n :f))) ((λ (:p) (:p (λ (:x :y) :x))) :p) ((λ (:p) (:p (λ (:x :y) :y))) :p))))) ((λ (:a :b :m) ((:m :a) :b)) (λ (:f :x) (:f :x)) (λ (:f :x) (:f :x)))))) (λ (:f :x) (:f (:f (:f (:f (:f (:f :x)))))))) = {b 720}
}
{hr}
{blockquote
"Perfection is reached not when there is nothing to add but when there is nothing to remove."
} 
{pre {center
BNF definition of the λ-calculus: e ::= x|λx.e|e1e2
}}
_p in other words: 
{pre

1. variable:    a char as [x,y,..,f,g,..] is a valid λ-term,
2. abstraction: if x is a variable and t is a valid λ-term, 
                then λx.t or (λ (x) t) is a valid λ-term,
3. application: if t and s are both valid λ-terms, 
                then ts or (t s) is a valid λ-term.
}

_p The least one can say is that it's not obvious and the syntax is rather terse! In this page, in order to understand the mechanisms of this amazing language that inspired the Lisp, I will translate in a more readable syntax, the λ-talk syntax, some basic objects of λ-calculus, {i numbers, operators, pairs} and show how a factorial can be computed without recursion.

_p And in order to be closer to the λ-talk syntax, I will write λ-calculus expressions using explicit parenthesis: {code (λ (x) t) , (t s)} and not {code λx.t , ts}.

_h5 1. lambdas

_p Lambdas are central in the λ-calculus and we must remember that a lambda is an anonymous function binding in its body a variable to a future value. This is an illustration from [[Palmström|http://palmstroem.blogspot.fr/2012/05/lambda-calculus-for-absolute-dummies.html]]:

{img {@ src="http://4.bp.blogspot.com/-5_DZOH_aqGc/U7eWeeGKSxI/AAAAAAAADyY/O3wr5_XXbZs/s1600/lambda2.png" width="100%" title="A picture from Palmstroem"}}

_p Not so easy, isnt'it? We can understand that {code (ab)} replaces {code y} in {code x(yz)} but what else? Using the λ-talk syntax we will write things in a more explicit shape, beginning with the definitions of "abstraction" and "application" on a first simple example  :

{pre
1) abstraction:  '{lambda {:one :two} :one brave new :two} 
-> an anonymous function
2) application: '{{lambda {:one :two} :one brave new :two} Hello World} 
-> {{lambda {:one :two} :one brave new :two} Hello World}
}

_p In λ-calculus functions are unary. They must be nested to simulate several arguments: 
{pre
((λ {del (x y)} x y) Hello World)          // this is not allowed

((λ (y) ((λ (x) x y) Hello)) World)  // this is allowed
-> ((λ (y) Hello y) World)
-> Hello World
}

_p In λ-talk functions can be applied to any number of values, at once or successively:
{pre
1) at once:
'{{lambda {:a :b} :a :b} Hello World War}
-> {{lambda {:a :b} :a :b} Hello World War}

2) or successively:
'{{{{lambda {:a :b} :a :b} Hello} World} War}
'{{{lambda {:b} Hello :b} World} War}
-> Hello World
}
_p Do you see how {code War} has been avoided? λ-talk functions are nice! 
_p Below, we can follow the evaluation of a λ-talk application when values are called at once and successively.

_p At once:

{pre
1)        |<-----------------------|
          |  |<---------------------|
'{{lambda {:a :b} :a+:b= {+ :a :b}} 3 4}
          |----->|-------->|  |
             |----->|-------->|
2)               3+4 = '{+ 3 4}
3)               3+4 = 7
}

_p or successively:
{pre
1)         |< ---------------------|
'{{{lambda {:a :b} :a+:b= {+ :a :b}} 3} 4}
           |----->|-------->|
2)        |< ----------------|
'{{lambda {:b} 3+:b= {+ 3 :b}} 4}  // a new function
          |---->|------->|
3)            3+4= '{+ 3 4}
4)            3+4= 7
}

_p Now it's easy to understand the following:

{pre 
'{{lambda {o a} oh happy day!} oOOOo aaAAaa} 
-> {{lambda {o a} oh happy day!} oOOOo aaAAaa}
}

_h5 2. Church numbers
_p In pure λ-calculus natural numbers don't exist. Alonzo Church defined [{code 0,1,2,3,...,n}] as successive functions waiting for 2 values:

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

_p In λ-talk, calling these functions with two values displays strange strings of {code (0}:
{pre
'{zero 0 0}  -> {zero 0 0}
'{two 0 0}   -> {two 0 0}
'{three 0 0} -> {three 0 0}
'{four 0 0}  -> {four 0 0}
'{five 0 0}  -> {five 0 0}
'{six 0 0}   -> {six 0 0}
}

_p It's not exactly what we want, let's imagine how {code 720} should be displayed! So we define a function, {code church}, translating these sequences of {code (0} in a standard number:

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

_p and we get:
{pre 
'{church zero} -> {church zero}
'{church one}  -> {church one}
'{church two}  -> {church two}
and so on...
}

_h5 3. a first set of operators
_p So, a Church number {code N} iterates {code N} times the application of a function {code f} on a variable {code x}. This definition gives the basis of a first set of operators, [{code succ, add, mul, power}] usually defined like this:
{pre
[succ]  = λnfx.f(n f x)    // (f ((n f) x))
[add]   = λnmfx.n f(m f x) // ((n f) ((m f) x)
[mul]   = λnmf.m(n f)      // (m (n f))
[power] = λnm.m n          // (m n)
}

_p In λ-talk we will write:

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

_p and test:

{pre
'{church {succ zero}}  -> {church {succ zero}}
'{church {succ one}}   -> {church {succ one}}
'{church {succ three}} -> {church {succ three}}
'{church {add two three}}   -> {church {add two three}}
'{church {mul two three}}   -> {church {mul two three}}
'{church {power three two}} -> {church {power three two}}
}

_p Building "opposite" functions like {code prev, subtract, divide} is not so easy - and Church itself  avoided them in the primitive version of λ-calculus. More complex structures than natural numbers have to be defined before, beginning with {b pairs}.

_h5 4. pairs
_p This is how the concept of pair is built in lambda-calculus ([[VIGRE|http://www.math.uchicago.edu/~may/VIGRE/VIGRE2006/PAPERS/Chariker.pdf]]):  
{pre
[cons] = λabm.m a b   // ((m a) b)
[car]  = λp.p(λxy.x)  // (p (λ (xy) x))
[cdr]  = λp.p(λxy.y)  // (p (λ (xy) y))
}

_p designed with in mind:
{pre
[car]([cons]AB) -> A
[cdr]([cons]AB) -> B
}
_p For demonstration purpose and not for necessity, I will rename [{code cons, car, cdr}] as [{code kons, kar, kdr}] in order to avoid using the existant ones defined as primitives in the λ-talk's dictionary. This is how this can be translated in λ-talk:

{pre
'{def kons {lambda {:a :b :m} {{:m :a} :b}}}       -> {def kons {lambda {:a :b :m} {{:m :a} :b}}}
'{def kar  {lambda {:p} {:p {lambda {:x :y} :x}}}} -> {def kar  {lambda {:p} {:p {lambda {:x :y} :x}}}}
'{def kdr {lambda {:p} {:p {lambda {:x :y} :y}}}}  -> {def kdr {lambda {:p} {:p {lambda {:x :y} :y}}}}
}

_p Testing:

{pre
'{kar {kons A B}} -> {car {cons A B}}
'{kdr {kons A B}} -> {cdr {cons A B}}
'{church {kar {kons {mul two three} {succ two}}}} -> {church {car {cons {mul two three} {succ two}}}}
'{church {kdr {kons {mul two three} {succ two}}}} -> {church {cdr {cons {mul two three} {succ two}}}}
}

_h5 5. the "pred" and "subtract" operators
_p With pairs we can now build the predecessor operator. The definition given in λ-calculus: 
{pre
[pred.pair] = λp.[cons](([cdr] p) ([succ](cdr p)))
[pred]  = λn.[car](n [pred.pair]([cons] 0 0))
}

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

{pre
'{def pred.pair {lambda {:p} {kons {kdr :p} {succ {kdr :p}}}}} 
-> {def pred.pair {lambda {:p}
 {cons {cdr :p} {succ {cdr :p}}}}}
'{def pred {lambda {:n} {car {{:n pred.pair} {cons zero zero}}}}} 
-> {def pred {lambda {:n}
 {car {{:n pred.pair} {cons zero zero}}}}}
}

_p we can test:

{pre
'{church {pred zero}}  -> {church {pred zero}}  // nothing before zero for Church numbers
'{church {pred one}}   -> {church {pred one}}
'{church {pred two}}   -> {church {pred two}}
'{church {pred three}} -> {church {pred three}}
}

_p This is a vizualisation of the process:

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

_p We can now define {code subtract}. Following [[jwodder.freeshell.org|http://jwodder.freeshell.org/lambda.html]]:
{pre
SUB := λmn. n PRED m  // ((n PRED) m)
'{def subtract {lambda {:m :n} {{:n pred} :m}}}
-> {def subtract {lambda {:m :n} {{:n pred} :m}}}
}

_p and testing:
{pre
'{church {subtract four three}} -> {church {subtract four three}}
'{church {subtract one one}} -> {church {subtract one one}}
}

_p Well, {code subtract} is easy, but {code div} is not, see [[jwodder.freeshell.org|http://jwodder.freeshell.org/lambda.html]]. We will see later how this operator and some others, {code DIV, TRUE, FALSE, NOT, AND, OR, LT, LEQ, Y,...}, can be built, but let's look at the factorial function, {code n! = 1*2*3*...*n}. Surprisingly, we don't need these operators, all the stuff is here to compute {code n!}.

_h5 6. computing factorial

_p The function {code factorial(n)} uses to be recursively defined like this:
{pre
n = 0 -> factorial(0) = 1
n > 0 -> factorial(n) = n*factorial(n-1)
}

_p λ-talk knows recursion, see [[recursion]] and [[Ycombinator]], but λ-calculus doesn't, at least easily. The standard approach is based on the so-called [[Ycombinator]], but at this point it looks simpler to process like we do for the {code pred} operator. The definition given in λ-calculus:

{pre
[fac.pair] = (λp.[cons]([succ]([car]p))([mul]([car]p)([cdr]p)))
[fac] = λn.[cdr](n[fac.pair]([cons]1 1))
}

_p says that {i {code fac.pair} gets a pair {code [a,b]} and returns a pair {code [a+1,a*b]}. {code fac} computes {code n} iterations of {code fac.pair} starting on the pair {code [1,1]}, leading to the pair {code [n,n!]} and  returns the second, {code n!}}. Translated in λ-talk:

{pre
'{def fac.pair
 {lambda {:p} {kons {succ {kar :p}} {mul {kar :p} {kdr :p}}}}}
-> {def fac.pair
 {lambda {:p} {cons {succ {car :p}} {mul {car :p} {cdr :p}}}}}
'{def fac
 {lambda {:n} {kdr {{:n fac.pair} {kons one one}}}}}
-> {def fac
 {lambda {:n} {cdr {{:n fac.pair} {cons one one}}}}}
}

_p we can test:

{pre
'{church {fac two}}   -> {church {fac two}}
'{church {fac three}} -> {church {fac three}}
'{church {fac four}}  -> {church {fac four}}
'{church {fac five}}  -> {church {fac five}}
}

_p This is a vizualisation of the process:

{pre
[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
}

_p For the fun, this is how {code '{fac five}} could be written without any use of names, {code one, five, mul, succ, kons, kar, kdr, fac.pair, fac}:

{pre {@ style="white-space:pre-wrap"}
'{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}}}}}}}}
-> {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}}}}}}}} 
}

_p In a pure λ-calculus style!

_h5 7. some other operators

_p Numerous other operators/structures/combinators can be built following the same scheme as it can be seen for instance in [[Collected Lambda Calculus Functions|http://jwodder.freeshell.org/lambda.html]]. Feel free to play with them!

_h5 sumary

_p We have seen that, using nothing but Church numbers and pairs, we can compute {code 1*2*3*4*5*...}. No {code booleans}, no {code if then else} control structure, no {code loop} structure or any magic {code Y} combinator. How is it possible to do such a miracle? {i Maybe because Church numbers and pairs contain all that stuff!} A Church number {code N} is the repeated application of a function on a value, say zero or false. It's an iteration structure by itself. In most of other languages numbers are "dead" datas given to control structures. In λ-calculus {b Church numbers} are iteration operators. And built on {code cons, car, cdr}, {b pairs} bring mutable states storing the intermediate and final values. A perfect example of the equivalence of code and data. {i Homoiconicity} as they say!

_ul {b Note 1}: every results in this page, for instance the last value {code 120}, are {b actually computed with λ-talk}. You can click on the top-left {code +} then on {code edit} to read the code of this page.
_ul {b Note 2}: λ-talk doesn't follow the standard evaluation approach, {code walk(tree(token(str)))}, and is exclusively based on {b Regular Expressions} evaluating in a single loop the code, a simple flat string made of words. Something like a Turing stripe/machine. More to see in [[calc2talk]], [[turing]], [[lambdatalk three]].
_ul {b 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 ? {i Don't blame me, I'm joking.}

_p {i Alain Marty, updated on 2016/05/01}

_h5 references
_ul  [[λ-calculus|http://en.wikipedia.org/wiki/Lambda_calculus]], 
_ul [[Church_encoding|https://en.wikipedia.org/wiki/Church_encoding]],
_ul [[the-y-combinator-no-not-that-one|https://medium.com/@ayanonagon/the-y-combinator-no-not-that-one-7268d8d9c46]], 
_ul [[lambda-calculus-for-absolute-dummies|http://palmstroem.blogspot.fr/2012/05/lambda-calculus-for-absolute-dummies.html]], 
_ul [[lambda calcul|http://www.mactech.com/articles/mactech/Vol.07/07.05/LambdaCalculus/index.html]],
_ul [[simonpj|http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/PAGES/V.HTM]]
_ul [[Y|http://mvanier.livejournal.com/2897.html]]
_ul [[Collected Lambda Calculus Functions|http://jwodder.freeshell.org/lambda.html]]
_ul [[epigrams|http://pu.inf.uni-tuebingen.de/users/klaeren/epigrams.html]]
_ul [[VIGRE|http://www.math.uchicago.edu/~may/VIGRE/VIGRE2006/PAPERS/Chariker.pdf]]
_ul [[palmstroem|http://palmstroem.blogspot.fr/2012/05/lambda-calculus-for-absolute-dummies.html]] 
_ul [[A Tutorial Introduction to the Lambda Calculus (Raul Rojas)|http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf]]
_ul ... and some others on the web!

{style
code '{background:#ff0}
}