lambdaway :: lambda

2 | list | login |load

| |

_img http://lambdaway.free.fr/workshop/data/brussels/nef.jpg
{center {i A deeply nested composition of catenaries, approximated by parabolas.{div}
The Sagrada Familia in Barcelona, Antonio Gaudi architect.}}

_h1 the λ-calculus (see [[updated version|?view=lambda_calculus2]])

_p 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 {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|fg
}

_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 "e" is a valid λ-term, 
                then "λx.e" is a valid λ-term,
3. application: if "f" and "g" are both valid λ-terms, 
                then "fg" 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 So a church number {b N} is an {b iterator} applying {b N} times a function {b f} to some initial value {b x}. In order to display a church number {b N} as a natural number we define a function, {b church}, applying a function incrementing N times an initial value 0. Note that this function doesn't belong to the reduced set of the λ-calculus set and is used for display purpose only.

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

'{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 :x} {:n {:m :f} :x}}}
-> {def mul {lambda {:n :m :f :x} {:n {:m :f} :x}}}
'{def power {lambda {:n :m :f :x} {{:m :n :f} :x}}}
-> {def power {lambda {:n :m :f :x} {{:m :n :f} :x}}}  
}

_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}}      // 55ms
6!  = '{church {fac {add three three}}}  -> 720      // 64ms 
7!  = '{church {fac {add three four}}}   -> 5040     // 167ms 
8!  = '{church {fac {add four four}}}    -> 40320    // 950ms 
9!  = '{church {fac {mul three three}}}  -> 362880   // 8700ms 
10! = '{church {fac {add five five}}}     -> 3628800 // 94600ms
}

_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}
     {div} 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="http://lambdaway.free.fr/lambdaspeech/data/hilbert_1.png" width="49%"}} {img {@ src="http://lambdaway.free.fr/lambdaspeech/data/hilbert_2.png" width="49%"}}}

_p See also [[fromroots2canopy]].

_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} {:f :f}}}
-> {def Y {lambda {:f} {:f :f}}}

'{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} {:f :f}}
   {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} {:f :f}}
   {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:

{prewrap
'{church
 {{lambda {:n}
  {{{lambda {:f} {:f :f}}
   {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} {:f :f}}
   {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 [[pablo rauzy|https://www.irif.fr/~carton/Enseignement/Complexite/ENS/Redaction/2009-2010/pablo.rauzy.pdf]]
_ul [[lambda-calculus-in-javascript|https://medium.com/openmindonline/lambda-calculus-in-javascript-1ee947cadb21]]
_ul [[https://glebec.github.io/lambda-talk/|https://glebec.github.io/lambda-talk/]]
_ul [[Ycombinator|https://mvanier.livejournal.com/2897.html]]

_ul [[https://speakerdeck.com/glebec/lambda-calc-talk-smartly-dot-io-version|https://speakerdeck.com/glebec/lambda-calc-talk-smartly-dot-io-version]]
_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/]]}}