lambdaspeech :: lambda-calcul

1 | list | login |load

| |

_img http://lambdaway.free.fr/workshop/data/brussels/nef.jpg
{center {i A deeply nested composition of catenaries, approximated by parabolas.}}

_h1 λ-calculus {sup {i revisited}}

_p Lambda calculus (also written as λ-calculus or called “the 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 (and Stephen Kleene), lambda calculus found early successes in the area of computability theory, such as a negative answer to {i Hilbert’s Entscheidungsproblem}.

_p This is the BNF definition of λ-calculus: 
{div {@ style="font:normal 3.0em courier new; text-align:center;"}
e := x|λx.e|ee
}

_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" is a valid λ-term,
3. application: if "t" and "s" are both valid λ-terms, 
                then "ts" is a valid λ-term.
}

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

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

{pre 
λx.t    will be written   (λ (x) t) 
ts      will be written   (t s)
λx.t v  will be written   ((λ (x) t) v)
}

_p Then, in order to explore some of λ-calculus expressions - ie {i to actually compute algorithms in realtime} - we will rewrite them using the {i lambdatalk} language, working in the current wiki, {i lambdatank}, on top of any modern web browser. See [[λ-talk|?view=start]] for details.

_h2 1. syntax

_p A λ-talk valid expression is made of:

{pre
1. words         :  [^\s'{}]*
2. abstractions  :  '{lambda {words} expression}
3. applications  :  '{expression expression} 
}

_p Note that:

_ul in λ-calculus variables are single characters, in '{λ talk} variables are words, for instance:
{pre
 '{{lambda {:arg} :arg} Hello} -> {{lambda {:a} :a} Hello}
}
_ul in λ-calculus functions have only one argument, they must be composed to simulate variadic functions, for instance 
{pre
((λ (y) ((λ (x) x y) a)) b) -> ((λ (y) a y) b) -> a b
}

_p We will agree to write simply

{pre
((λ (x y) x y) a b) -> a b
} 
_ul in '{λ talk} functions can have several arguments and accept partial applications:

{pre
'{{lambda {:a :b} Hello :a :b World} brave new}    // with two values
-> {{lambda {:a :b} Hello :a :b World} brave new}                          // returns a value
'{{lambda {:a :b} Hello :a :b World} brave}        // with one value
-> '{lambda {:b} Hello brave :b World}             // returns a function
'{{lambda {:b} Hello brave :b World} new}          // with the second one
-> Hello brave new World                          // returns a value
}

_p The expression {code '{{lambda {:a :b} Hello :a :b World} brave new}} or more generally {code {b '{{lambda {words} expression} expression}}} is called an IIFE ({i Immediately Invoked Function expression}). The inner expression {code '{lambda {words} expression}} is a {i special form} called {b abstraction} and evaluated in a pre-processing step to a function's reference. The outer expression - which became {code '{function_ref expression}} - is a {i nested form} called {b application} evaluated from inside out.

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

{pre
1) give a name to the abstraction:

'{def HI
 {lambda {:a :b}
         Hello :a :b World
}}
-> {def HI {lambda {:a :b} Hello :a :b World}}

2) and apply it to different values:

'{HI brave new}
-> {HI brave new}
'{HI poor old}
-> {HI poor old}
}

_p Note that λ-talk doesn't know closures. Lambdas are pure black boxes completely independent of any context. There are not {i free variables} taking {i 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 {i life without closures} in a world where functions are first class, accept {i de facto} partial application and accept a number of values greater than the number of arguments.
_p More can ne seen in this page [[lambda]].

_h2 2. pairs

_p Functions can be nested, leading to powerful {i data and control structures}. 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   // (λ (a b m) ((m a) b))
[car]  = λp.p(λxy.x)  // (λ (p) (p (λ (xy) x)))
[cdr]  = λp.p(λxy.y)  // (λ (p) (p (λ (xy) y)))
}

_p designed with in mind:
{pre
[car]([cons]AB) -> A
[cdr]([cons]AB) -> B
}
_p This is how this can be translated in λ-talk, renaming [{code cons, car, cdr}] as [{code kons, kar, kdr}] in order to avoid conflicts with existant ones defined as primitives in the λ-talk's dictionary:

{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}} -> {kar {kons A B}}
'{kdr {kons A B}} -> {kdr {kons A B}}
}

_p Note the partial application in {code '{kons A B}}. The {code 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 {code kar} or {code kdr} to return the first or the last value, {b A} or {b B}.

_h2 3. 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, usually written like this:

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

_p easily translated in '{λ talk}

{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 N {lambda {:f :x} {:f {:f ... {:f :x}}..}}} // N times
}

_p Calling these functions with two values displays strange strings:
{pre
'{zero 0 0}  -> {zero 0 0}
'{one 0 0}   -> {one 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}
}

_p It's not exactly what we want, let's imagine how {code 720} should be displayed! So - {i forgetting that we are not allowed to use any javascript number and operator} - we define a function, {code church}, translating these strange sequences into a readable decimal 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...
}

_h2 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)    // (λ (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))
}

_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}}
}

_h2 4. the pred operator & alii

_p Building "opposite" functions like {code prev, subtract, divide} is not so easy - and Church itself avoided them in the primitive version of λ-calculus. This is where the concept of {b pairs} comes in to help us...  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} {kons {kdr :p} {succ {kdr :p}}}}} 
'{def pred {lambda {:n} {kar {{:n pred.pair} {kons zero zero}}}}} 
-> {def pred {lambda {:n}
 {kar {{:n pred.pair} {kons zero zero}}}}}
}

_p Some tests:

{pre
'{church {pred zero}}  -> {church {pred zero}}  // nothing exists before zero
'{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 the {code subtract} operator. Following [[jwodder.freeshell.org|http://jwodder.freeshell.org/lambda.html]]:
{pre
SUB := λmn. n PRED m     // (λ (m n) ((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 The factorial function {code n! = 1*2*3*...*n} uses to be introduced via recursion:

{pre
n = 0 -> factorial(0) = 1
n > 0 -> factorial(n) = n*factorial(n-1)
}

_p At this point we follow the approach used to build the {code pred} operator. The following 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} {kons {succ {kar :p}} {mul {kar :p} {kdr :p}}}}}
'{def fac
 {lambda {:n} {kdr {{:n fac.pair} {kons one one}}}}}
-> {def fac
 {lambda {:n} {kdr {{:n fac.pair} {kons one one}}}}}  
}

_p we can test:

{pre
2!  = '{church {fac two}}             -> {church {fac two}}
3!  = '{church {fac three}}           -> {church {fac three}}
4!  = '{church {fac four}}            -> {church {fac four}}
5!  = '{church {fac five}}            -> {church {fac five}}  // 25ms
10! = '{church {fac {mul two five}}}  -> 3628800  // 21400ms
}

_p This is a vizualisation of the process for 5!

{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 replacing names, [{code one, five, mul, succ, kons, kar, kdr, fac.pair, fac}], by their lambda expressions:

{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}}}}}}}}
-> 120
}

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

_h2 5. recursion

_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]]. In the following we choose another way and are going to use {b recursion}. We need nothing but a predicate function, {code '{iszero? number}} returning {code kar} if the number is {code zero} else {code kdr}:

{pre                      
'{def iszero? {lambda {:c} {:c {{lambda {:a :b} :a} kdr} kar}}}
-> {def iszero? {lambda {:c} {:c {{lambda {:a :b} :a} kdr} kar}}}

'{iszero? zero}
-> {iszero? zero}
'{iszero? one}
-> {iszero? one}
'{iszero? two}
-> {iszero? two}
...
}

_p Using this predicate function calling the {code kar} or the {code kdr} of a {code kons} let's rewrite the factorial in a recursive style:

{pre 
'{def FAC {lambda {:n}
  {{{iszero? :n}
   {kons {lambda {:n} one}
         {lambda {:n} {mul :n {FAC {pred :n}}}}}} :n}}}
-> {def FAC {lambda {:n}
  {{{iszero? :n} {kons
   {lambda {:n} one}
   {lambda {:n} {mul :n {FAC {pred :n}}}}}} :n}}}

'{church {FAC five}}
-> {church {FAC five}}
}

_p Some explanations: replacing in {code FAC} the two inner lambdas by {code T} and {code F}

{pre
'{def FAC {lambda {:n} {{{iszero? :n} {kons T F}} :n}}}
}

_p we understand that for some value {code N}:

{pre
if N = five 
then '{iszero? five} = kdr
and '{FAC five} = '{{kdr {kons T F}} five}
-> '{F five} 
-> '{{lambda {:n} {mul :n {FAC {pred :n}}}} five} 
-> '{mul five {FAC {pred five}}}  
-> '{mul five {FAC four}}          // a recursive call

if N = zero 
then '{iszero? zero} = kar
and '{FAC 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
}

;; _p Remember that lambdatalk evaluate nested forms from inside out - greadiness - and note the use of lambdas to bring a delayed evaluation - laziness - and pairs to bring a fork.

_p Now let's go on and  compute {code q & r} in {code a = p*q+r} and the gcd:

{pre

'{def //                            
  {lambda {:a :b}
   {{{iszero? {subtract :b :a}}
    {kons {lambda {:a :b} {add one {// {subtract :a :b} :b}}}
          {lambda {:a :b} zero} }} :a :b}}}
-> {def //                            
  {lambda {:x :y}
   {{{iszero? {subtract :y :x}}
    {kons {lambda {:x :y} {add one {// {subtract :x :y} :y}}}
          {lambda {:x :y} zero} }} :x :y}}}

'{def %%                             
 {lambda {:a :b}
  {subtract :a {mul {// :a :b} :b}}}}
-> {def %%                             
 {lambda {:x :y}
  {subtract :x {mul {// :x :y} :y}}}}

'{def gcd
 {lambda {:a :b}
  {{{iszero? :b} 
   {kons {lambda {:a :b} :a}
         {lambda {:a :b} {gcd :b {%% :a :b}}}}} :a :b}}}
-> {def gcd
 {lambda {:a :b}
  {{{iszero? :b} 
   {kons {lambda {:a :b} :a}
         {lambda {:a :b} {gcd :b {%% :a :b}}}}} :a :b}}}

'{church {// five two}}
-> {church {// five two}}
'{church {%% five two}}
-> {church {%% five two}}

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

_p Let's play with the Towers of Hanoï:

{pre
'{def hanoi
 {lambda {:n :from :to :via}
  {{{iszero? :n}
   {kons {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}}}
-> {def hanoi
 {lambda {:n :from :to :via}
  {{{iszero? :n} {kons
   {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 four A B C}
-> {hanoi four A B C} 
}

_p Let's draw a Hilbert curve

{prewrap
'{def left
 {lambda {:d :n}
  {{{iszero? :n}
   {kons {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}}}
-> {def left
 {lambda {:d :n}
  {{{iszero? :n} {kons
   {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}}}
'{def right
 {lambda {:d :n}
  {{{iszero? :n}
   {kons {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}}}
-> {def right
 {lambda {:d :n}
  {{{iszero? :n} {kons
   {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}}}

'{left 10 one}
-> {left 10 one}
'{left 10 two}
-> {left 10 two}
'{left 10 three}
-> {left 10 three}
}

_p three sequences of words which can be used by a [[turtle graphic|/?view=hilbert]] tool - understanding the {code T+/-90} and {code M10} commands - to display three of the following Hilbert curves:
{center {img {@ src="data/hilbert_1.png" width="49%"}} {img {@ src="data/hilbert_2.png" width="49%"}}}

_p See also [[list2]].

_h2 6. Y-combinator

_p 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 {i definitions}. But a recursive function calls its name inside its body and we will rewrite it as an {i almost-recursive} one without any name's reference and call the function using some {i Y-combinator} acting as a fix point, a kind of bridge. Let's apply this process to the factorial function:

{pre
'{def Y {lambda {:f :n} {:f :f :n}}}
-> {def Y {lambda {:f :n} {:f :f :n}}}

'{def almost_FAC {lambda {:f :n}
  {{{iszero? :n}
   {kons {lambda {:f :n} one}
         {lambda {:f :n} {mul :n {:f :f {pred :n}}}}}} :f :n}}}
-> {def almost_FAC {lambda {:f :n}
  {{{iszero? :n} {kons
   {lambda {:f :n} one}
   {lambda {:f :n} {mul :n {:f :f {pred :n}}}}}} :f :n}}}

'{church {Y almost_FAC five}}
-> {church {Y almost_FAC five}}
}

_p We can {i compose} {code Y} and {code almost_FAC} into {code YFAC}:

{pre
'{def YFAC
 {lambda {:n}
  {{lambda {:f :n} {:f :f :n}}
   {lambda {:f :n}
    {{{iszero? :n}
     {kons {lambda {:f :n} one}
           {lambda {:f :n} {mul :n {:f :f {pred :n}}}}}} :f :n}} :n}}}
-> {def YFAC
 {lambda {:n}
  {{lambda {:f :n} {:f :f :n}}
   {lambda {:f :n}
    {{{iszero? :n} {kons
     {lambda {:f :n} one}
      {lambda {:f :n} {mul :n {:f :f {pred :n}}}}}} :f :n}} :n}}}

'{church {YFAC five}}
-> {church {YFAC five}}
}

_p and even forget the name {code YFAC}, building an IIFE:

{pre
'{church
 {{lambda {:n}
  {{lambda {:f :n} {:f :f :n}}
   {lambda {:f :n}
    {{{iszero? :n}
     {kons {lambda {:f :n} one}
           {lambda {:f :n} {mul :n {:f :f {pred :n}}}}}} :f :n}} :n}} five}}
-> {church
 {{lambda {:n}
  {{lambda {:f :n} {:f :f :n}}
   {lambda {:f :n}
    {{{iszero? :n} {kons
     {lambda {:f :n} one}
      {lambda {:f :n} {mul :n {:f :f {pred :n}}}}}} :f :n}} :n}}
 five}}
}

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

_h2 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!}

_ul 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.

_ul Thanks to a reduced set of functions, {code [cons, car, cdr]}, {b pairs} bring mutable states storing the intermediate and final values.

_p A perfect example of the equivalence of code and data. {i Homoiconicity} as they say!

_p {b Note 1}: every results in this page, even the last value {code 10! = 3628800}, are {b 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.

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

_p {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.

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

_p {i Don't blame me, I'm joking.}

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

_h2 references

_ul [[A Tutorial Introduction to the Lambda Calculus (Raul Rojas)|http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf]]
_ul [[The Lambda Calculus (Don Blaheta)|http://cs.brown.edu/courses/cs173/2001/Lectures/2001-10-25.pdf]]
_ul  [[λ-calculus (wikipedia)|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]], (André van Meulebrouck)
_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 [[what-is-lambda-calculus-and-why-should-you-care|https://zeroturnaround.com/rebellabs/what-is-lambda-calculus-and-why-should-you-care/]]
_ul [[Show HN: λ-calculus revisited|https://news.ycombinator.com/item?id=22222682]]
_ul [[SHEN|http://www.schoolofinternalalchemy.com/]]
_ul ... and some others on the web!

{style 
body { background:#ccc; }
pre { box-shadow:0 0 8px #000; padding:5px; background:#ffe; }
}

_img http://www.marktarver.com/tree.png
{center {i From [[Mark Tarver|http://www.marktarver.com/]]}}