lambdaway :: lambda

1 | list | login |load

| |

_h1 (λ-calculus {sup {i (revisited for dummies {sup (like me)})}})

{{block}
;; {uncover http://lambdaway.free.fr/workshop/data/brussels/nef.jpg 100 500 
;; A deeply nested composition of catenaries, approximated by parabolas.{br}
;; The Sagrada Familia in Barcelona, Antonio Gaudi architect.}

_h2 introduction

_p The λ-calculus ([[lambda calculus|http://en.wikipedia.org/wiki/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 a "quasi BNF" definition of λ-calculus: 
{div {@ style="font:normal 3.0em courier new; text-align:center;"}
e := x|λy.f|gh
}

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

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

_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 
λy.f    will be written   (λ (y) f) 
gh      will be written   (g h)
;; λy.f z  will be written   ((λ (y) f) z)
}

_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 [[coding]] for details.

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

_ul introduce the lambdatalk syntax
_ul define booleans and pairs
_ul define Church numbers
_ul introduce iteration
_ul introduce recursion
_ul introduce the Y-combinator

{hr}

_p See also some others explorations: 
_ul [[short|?view=lambda_calculus_short]] (Church numerals and iteration)
_ul [[Lambda calculus facts for kids|?view=lc_french]] (from [[kiddle|https://kids.kiddle.co/Lambda_calculus]])
_ul [[simply]] (a very basic one)
_ul [[λ-calculus using binary numbers of variable length |?view=oops6]]
_ul [[coding]] (the kernel of lambdatalk)
}

{{block}
_h2 1. λ-talk syntax

_p A λ-talk valid expression is made of:

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

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

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

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

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

_p More generally {b '{{lambda {words} expression} expression}} is an {i Immediately Invoked Function expression}, an {b IIFE}. The inner expression {b '{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 {b '{function_ref expression}} - is a {i nested form} called {b application} evaluated from inside out.

_h3 '{lambda {words} expression}

_p {b λ-talk} is implemented so that
_ul 1) {b words} are {b not evaluated}, they are simply skipped by the evaluator, 
_ul 2) {b applications} are normal forms evaluated {b from inside out} to a word or a sequence of words, 
_ul 3) {b lambdas} are special forms evaluated to a single word - a function's reference added to a dictionary, initially empty - and follow these 3 rules:
_ul20 3.1) called on a number of words {b lesser} than the number of arguments, a lambda memorizes the given words and returns a new lambda waiting for missing words,
_ul20 3.2) called on a number of words {b equal} to the number of arguments a lambda returns a word or a sequence of words,
_ul20 3.3) called on a number of words {b greater} than the number of arguments, the last one gets the exceeding words and the lambda returns a word or a sequence of words.
_ul 4) {b lambdas} are evaluated {b first}, {b applications} are evaluated {b last}.

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

_h3 '{def name expression}

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

{pre
1) {b abstraction}: give a name to the anonymous function,

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

2) {b application}: and apply it to different words.

'{SWAP hello world}
-> {SWAP hello world}
}

_p {b Note:} λ-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 and accept {i de facto} a number of values {b lesser or greater} than the number of arguments.

_p More can ne seen in this page [[coding]].
}

{{block}
_h2 2. booleans & pairs

_p Booleans don't exist, let's build them

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

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

_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
[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]))
}

_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 [{b cons, car, cdr}] as [{b 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 TRUE}}} 
-> {def kar  {lambda {:p} {:p TRUE}}}
'{def kdr {lambda {:p} {:p FALSE}}}  
-> {def kdr {lambda {:p} {:p FALSE}}}
}

_p Testing:

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

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

{{block}
_h2 3. Church numbers

_p In pure λ-calculus natural numbers don't exist. Alonzo Church defined [{b 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 {b 720} should be displayed! So - {i forgetting that we are not allowed to use any javascript number and operator} - we define a function, {b church}, translating these strange sequences into a readable decimal number:

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

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

_p {b Note:} Church numbers are iterators {b per se} so, for instance, we could build a function iterating n times a word 
{prewrap
    '{def iterate
 {lambda {:n :a}
  {{:n {{lambda {:a :x} :a :x} :a}} .}}}
-> {def iterate
 {lambda {:n :a}
  {{:n {{lambda {:a :x} :a :x} :a}} .}}}

'{iterate five hello}
-> {iterate five hello}

}

_p We will exploit this property in the next section.

_p See also [[OnTheRepresentationOfDataInLambdaCalculus.pdf|https://personal.cis.strath.ac.uk/guillaume.allais/OnTheRepresentationOfDataInLambdaCalculus.pdf]]
}

{{block}
_h2 3. iteration {sup (1)}

_p So, a Church number {b N} iterates {b N} times the application of a function {b f} on a variable {b x}. This definition gives the basis of a first set of operators, [{b 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}}

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

{{block}
_h2 4. iteration {sup (2)}

_p Building "opposite" functions like {b 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 {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 {b pred.pair} gets a pair {b [a,a]} and returns a pair {code [a,a+1]} ; {b pred} computes {b n} iterations of {b pred.pair} starting on the pair {b [0,0]}, leading to the pair {b [n-1,n]} and  returns the first, {b 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 {b 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}}
}

_h3 the factorial

_p The factorial function {b 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 choose an iterative approach similar to the approach used to build the {b pred} operator. The following definition given in λ-calculus:

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

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

_p Translated in λ-talk:

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

_p we can test:

{pre
2!  = '{church {ifac two}}                -> {church {ifac two}}
3!  = '{church {ifac three}}              -> {church {ifac three}}
4!  = '{church {ifac four}}               -> {church {ifac four}}
5!  = '{church {ifac five}}               -> {church {ifac five}}      // 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
}

_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 {b '{ifac five}} could be written replacing names, [{b 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! 
}

{{block}
_h2 5. recursion {sup (1)}

_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, {b '{zero? number}} returning {b TRUE} if the number is {b zero} else {b FALSE}:

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

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

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

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

_p leading to, without explanations:

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

'{church {rfac five}}
-> {church {rfac five}}

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

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

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

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

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

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

_p This is a {b tail recursive} version

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

'{church {trfac one five}}
-> {church {trfac one five}}

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

_p So, {b trfac} is twice as fast as {b rfac} and {b 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|?view=oops6]] breaks the glass ceiling.  
}

{{block}

_h2 6. recursion {sup (2)}

_p Let's explore some new algorithms

_h3 div, mod & gcd

{pre

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

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

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

'{church {divide five two}}
-> {church {divide five two}}
'{church {mod five two}}
-> {church {mod five two}}

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

_h3 fibonacci

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

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

_h3 the Towers of Hanoï

{pre
'{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}}}
-> {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}
     {div} move disc {church :n} from tower :from to tower :to 
    {hanoi {pred :n} :via :to :from} }}
   :n :from :to :via}}}
}

_p Testing

{pre
'{hanoi four A B C}
-> {hanoi four A B C} 
}

_h3 the Hilbert curve

{prewrap
'{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}}}
-> {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}}}
'{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}}}
-> {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}}}
}

_p Testing

{prewrap
'{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 {b T+/-90} and {b M10} commands - to display the first three of the following Hilbert curves:
_img data/IMG_0300.png 
_img data/IMG_0301.png

_p See also [[fromroots2canopy]] or [[coding]].
}

{{block}
_h2 7. 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 {b almost-recursive} one, {b arfac}, without any name's reference and call the function using some {b Y}-combinator acting as a  bridge. Let's apply this process to the factorial function:

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

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

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

_p We can {i compose} {b Y} and {b arfac} into {b Yarfac}:

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

'{church {Yarfac five}}
-> {church {Yarfac five}}
}

_p and even forget the name {b Yarfac}, building an IIFE:

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

_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 4. In a pure λ-calculus style!
_p See also [[mockingbird|http://raganwald.com/2018/09/03/mockingbirds-sage-birds-and-widowbirds.html]] and [[stackoverflow|https://stackoverflow.com/questions/46820404/non-recursive-lambda-calculus-factorial-function]]

_p This is a variant of {b Y} avoiding duplication of {b :f} in the body of {b arfac}
{pre
'{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}}}}
-> {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}}}}

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

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

_p A matter of choice.

}

{{block}
_h2 conclusion

_p We have seen that, using nothing but Church numbers and pairs, we can compute {b 1*2*3*4*5*...}. No {b booleans}, no {b if then else} control structure, no {b loop} structure or any magic {b 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 {b 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, {b [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 {b 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 {b walk(tree(token(str)))} evaluation approach and is based on a single {i regular expression}, {b /\'{([^\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, on 2021/11/10 and on 2024/0727}
}

{{block}
_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 [[https://medium.com/@axdemelas/lambda-calculus-with-javascript|https://medium.com/@axdemelas/lambda-calculus-with-javascript-897f7e81f259]]
_ul ... and some others on the web!
_ul [[HN|https://news.ycombinator.com/item?id=29185764]] | [[HN|https://news.ycombinator.com/item?id=33839383]] | [[HN|https://news.ycombinator.com/item?id=33897841]] | [[HN-20240727|https://news.ycombinator.com/item?id=41087170]] | [[reddit/lambdacalculus|https://www.reddit.com/r/lambdacalculus/comments/1edj9wo/lambda_calculus_revisited_for_dummies_like_me/]]}

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

{macro \/\/\s([^\n]*)\n to <span style="color:yellow">// €1<br></span>}

{{hide}
{def block 
  div {@ style="display:inline-block; width:600px; vertical-align:top; padding:20px; "}}
}

{style 
body { background:#444; } 
#page_frame { border:0; background:#444; width:600px; margin-left:0; }
#page_content { background:transparent; color:#fff; border:0; width:7200px; box-shadow:0 0 0; font-family: optima; }
.page_menu { background:transparent; color:#fff; }
a { color:#f80; }
pre { box-shadow:0 0 8px #000; padding:5px; background:#444; color:#fff; font:normal 1.0em courier; }
b { color:cyan; }
h1 { font-size:4.0em; margin-left:0; }
h2 { font-size:3.0em; margin-left:0; text-align:center; }
h3 { font-size:1.5em; margin-left:0; text-align:center; } 
}