lambdaway :: simply

5 | list | login |load

| |

{{block}
;;{uncover data/simplet.jpg 100 800 A Turing complete language from scratch.}

;; _h1 [[simple minds|?view=lambda_calculus]]

;; _h1 a side glance at λ-calculus
_h1 λ-calculus at a glance

_p The {b [[λ-calculus|?view=lambda_calculus]]} created in the 30s by Alonzo Church, ten years before the era of computers, is a small formal language theoretically allowing to build any algorithm one can think of. As any other language its implementation on a computer supposes an underlying language which itself is built on a lower one until the bare metal of the computer. Web browsers come with a rich set of tools, (HTML, CSS, DOM, JAVASCRIPT,...) on which I have built a small overlay, the {b lambdaway} project, proposing an IDE, {b lambdatank}, and a programming language, {b lambdatalk}.

_p Here I will introduce a small version of λ-calculus, using lambdatalk itself reduced to its minimum and allowing all code examples to be tested and computed in real-time in this wiki page.

_h2 definition

_p At the lowest level a [[lambdatalk|?view=start]] code is made of {b words} and {b expressions}, where

{pre
- a {b word} is any group of {b characters} except spaces and curly braces, '{}
    for instance: james, bond, 123, #f00, :a, :b, ...
- an {b expression} is made of {b abstractions}, {b definitions} and {b applications},
    - an {b abstraction} is defined as '{lambda {words} expression}
    - a {b definition} is defined as '{def word expression}
    - an {b application} is defined as '{abstraction expression}
}

_h2 evaluation

_p {b words} and {b expressions} are evaluated according to these rules

{pre
- a word is not evaluated,
- an abstraction is evaluated to a word, bound to a JS 
  anonymous function added to a dictionary, initially empty,
- a definition is evaluated to a word, from inside out,
- an application is evaluated to words, from inside out,
- abstractions and definitions are evaluated before applications.
}

_p In the followings I will give minimal explanations on lambdas and show how some arithmetic can be built from scratch to compute the factorial of a number, avoiding the use of the concept of recursion (and Y-combinators) discussed elsewhere, for example [[here|?view=lambda_calculus]]. More details are to be found starting here [[homepage|?view=start]].

_p {b Note:} This wiki page is a lambdatalk program evaluated in less than 20ms on my MacBook Air, iPad Pro, and smartphone. This page in large format can be comfortably consulted on any screens, wide and narrow, just use zooms +/- or dblclicks and sliders and fingers, it's easy and safe.

}

{{block}
_h1 lambdas & defs

_p Everything starts with a {b text rewriting command} like this one

{pre
{b replace} {u a} & {u b}
     {b in} My name is {u b}, {u a} {u b}.
     {b by} James & Bond
}

_p immediately translated into a {b code} understandable by lambdatalk:

{pre
'{{lambda {:a :b} 
          My name is :b, :a :b.
         } James Bond}
-> {{lambda {:a :b} My name is :b, :a :b.} James Bond} 
}

_p where {b lambda} is for {b replace}, well balanced curly braces replace the {b &, in, by} conjunctions and underlined words have been prefixed by a special character, ":", enlighting them as variables.

_p Because such expressions, sometimes called {b IIFE}s ({i Immediately Invoked Function Expressions}), are rather hard to handle, it's a good practice to split them into two steps, giving the lambda expression a name and calling it later.

{pre
1: '{def HI 
    {lambda {:a :b} My name is :b, :a :b.}
   }
   -> {def HI {lambda {:a :b} My name is :b, :a :b.}}

2: '{HI James Bond}
   -> {HI James Bond} 
}

_p And that's it, using {b lambdas & defs} we have what is required to build everything we want.

_h2 function's behaviour

_p We have just defined {b HI} as a function waiting for two words, {b :a :b}. Let's analyze its behaviour when it is called on a variable number of words.

_ul 1) zero word: 
{pre
'{HI}
-> {HI}  
}
_p It's under another reference the same function {code '{lambda {:a :b} My name is :b, :a :b.}}, still waiting for two values
_ul 2) one word: 
{pre
'{HI James}
-> {HI James}  
}
_p It's the reference of a new function, {code '{lambda {:b} My name is :b, James :b.}}, memorising James and waiting for the missing value.

_ul 3) two words:
{pre
'{HI James Bond}
-> {HI James Bond} 
} 
_p It's the awaited result.

_ul 4) more words: 
{pre
'{HI Antoine de Saint Exupery}
-> {HI Antoine de Saint Exupery}  
}
_p The first argument, :a, got the first value, "Antoine", the second argument, :b, got the rest, "de Saint Exupery".

_p In short, technically speaking, functions accept {i de facto} a number of values lesser, equal or greater then the number of its arguments. Twinned with the IIFE mechanism, this powerful behaviour will help to workaround the lack of {b closures}, the fact that functions are black boxes knowing nothing of the context and can't have {i free variables}, excepted the global dictionary where are stored the user defined names. 
}

{{block}
_h1 a few steps in arithmetic

_p At this level numbers don't exist, nothing else exists than words and functions in our toolbox, we have to build everything.

_h3 numbers

_p After Alonzo Church, the father of {b λ-calculus} we define a number {b n} as an {b iterative function} applying {b n} times some function {b f} to some value {b x}

{pre
n := '{lambda {:f :x} {:f {:f ......... {:f {:f :x}}}}}
                      :f applied n times .. to :x
}

_p So we could write the set of numbers this way

{pre
0: '{lambda {:f :x} :x}
1: '{lambda {:f :x} {:f :x}}
2: '{lambda {:f :x} {:f {:f :x}}}
3: '{lambda {:f :x} {:f {:f {:f :x}}}}

... and so on
}

_p Practically we give a name to the first number, {b ZERO} and we define a function, {b SUCC}, to compute the successor of any number

{pre
'{def ZERO {lambda {:f :x} :x}}   // apply zero time
-> {def ZERO {lambda {:f :x} :x}}
                              :f one more time
'{def SUCC {lambda {:n :f :x} {:f {:n :f :x}}}}
-> {def SUCC {lambda {:n :f :x} {:f {:n :f :x}}}}                           :n times :f to :x

'{def ONE {SUCC ZERO}} 
-> {def ONE {SUCC ZERO}}
'{def TWO {SUCC {ONE}}}
-> {def TWO {SUCC {ONE}}}
'{def THREE {SUCC {TWO}}} 
-> {def THREE {SUCC {TWO}}}

... and so on
}

_p Displaying the value of a number requires some thought. Simply writing {b '{THREE}} displays the reference of the function associated to this number, {b {THREE}}, which is not very meaningful. The idea is to build a function that will "apply" {b THREE} to two well-chosen values to produce a readable result. So we choose to define a function {b CHURCH} displaying numbers as dots "{b •}" prefixed by the "{b #}" character

{pre
'{def CHURCH {lambda {:n} {:n {lambda {:x} :x•} #}}}
-> {def CHURCH {lambda {:n} {:n {lambda {:x} :x•} #}}}

'{CHURCH {ZERO}} 
-> {CHURCH {ZERO}} 
'{CHURCH {ONE}} 
-> {CHURCH {ONE}}
'{CHURCH {TWO}}
-> {CHURCH {TWO}}
'{CHURCH {THREE}}  
-> {CHURCH {THREE}}
}

_p To go further and faster in the construction of the infinite set of natural numbers we define two fundamental operations, addition and multiplication.

_h3 addition and multiplication

;; _p Remember that {b THREE} is equivalent to {b '{lambda {:f :x} {:f {:f {:f :x}}}}}, and this iterative behaviour will be used to build {b ADD & MUL} adding and multiplying two numbers.

_p We add TWO and THREE applying two times the SUCC operator to THREE, ie {b '{{2 SUCC} 3}}

{pre
'{def ADD {lambda {:n :m} {{:n SUCC} :m}}}  
-> {def ADD {lambda {:n :m} {{:n SUCC} :m}}}                   // apply n times SUCC to m

'{def FIVE {ADD {TWO} {THREE}}} 
-> {def FIVE {ADD {TWO} {THREE}}}
'{CHURCH {FIVE}}
-> {CHURCH {FIVE}}    // five dots
}

_p We multiply TWO and THREE applying two times the addition of THREE and THREE starting at ZERO, ie {b '{2 {ADD 3} 0}}

{pre
'{def MUL {lambda {:n :m} {{:n {ADD :m}} {ZERO}}}}  
-> {def MUL {lambda {:n :m} {{:n {ADD :m}} {ZERO}}}}                   // apply n times '{ADD :m} to ZERO

'{def SIX {MUL {TWO} {THREE}}} 
-> {def SIX {MUL {TWO} {THREE}}} 
'{CHURCH {SIX}}
-> {CHURCH {SIX}}    // six dots
}

_h3 iteration

_p The goal is to compute the product of numbers from 1 to n, the {b factorial}. One way is to follow this process

{pre
[1 , 1]     = [1 , 1]
[2 , 2*1]   = [2 , 2]
[3 , 3*2]   = [3 , 6]
[4 , 4*6]   = [4 , 24]
[5 , 5*24]  = [5 , 120]
[6 , 6*120] = [6 , 720] -> the factorial of 6 is 720
}

_p We must first find a way to aggregate words, and we define three functions, {b PAIR, LEFT, RIGHT}, to build pairs of two words and get back the left and the right ones.

{prewrap
'{def PAIR {lambda {:a :b :c} {:c :a :b}}}
-> {def PAIR {lambda {:a :b :c} {:c :a :b}}}
'{def LEFT {lambda {:c} {:c {lambda {:a :b} :a}}}}
-> {def LEFT {lambda {:c} {:c {lambda {:a :b} :a}}}}
'{def RIGHT {lambda {:c} {:c {lambda {:a :b} :b}}}}
-> {def RIGHT {lambda {:c} {:c {lambda {:a :b} :b}}}}

'{LEFT {PAIR 123 456}}
-> {LEFT {PAIR 123 456}}
'{RIGHT {PAIR 123 456}}
-> {RIGHT {PAIR 123 456}} 
}

_p Note that the {b PAIR} function is defined with 3 variables, {b :a, :b, :c} and is given only 2 values, {b 123 & 456}. It's a partial application whose result is a new function of one argument, {b :c}, storing the given values in it's body, {b '{lambda {:c} {:c 123 456}}}, and waiting for the missing one. I leave it to your sagacity to trace the call of the function {b LEFT} on the pair until the final result, {b 123}.

_p We can now build the factorial in two steps:
_ul 1) FAC.pair gets a pair p = [a,b] and returns a pair [a+1,a*b]. 
_ul 2) FAC computes n iterations of FAC.pair starting on the pair [1,1], leading to the pair [n,1*2*3*...*n] and returns the right term which is n!.

_p leading to this lambdatalk code

{pre
'{def FAC.pair
 {lambda {:p}
  {PAIR {SUCC {LEFT :p}}
        {MUL {LEFT :p} {RIGHT :p}}}}}    // [a,b] -> [a+1,a*b]
-> {def FAC.pair
  {lambda {:p} {PAIR {SUCC {LEFT :p}}
                     {MUL {LEFT :p} {RIGHT :p}}}}}

'{def FAC
 {lambda {:n}  
  {RIGHT
   {:n FAC.pair {PAIR {ONE} {ONE}}}}}} 
-> {def FAC
 {lambda {:n}  
  {RIGHT
   {:n FAC.pair {PAIR {ONE} {ONE}}}}}} 
}

_p and we can now compute the factorial of a number

{prewrap
'{CHURCH {FAC {SIX}}}  
-> #•••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••••• 
}

_p Yes there are {b 720} dots. Even if this notation is very primitive and limited to small natural numbers, it has the merit to use neither number nor predefined operator. It is only a matter of words and functions that we have learned to count.

_p {b Note:} You could see [[λ-calculus using binary numbers of variable length|?view=oops6]] for a more efficient implementation of numbers, as lists of booleans.

}

{{block}
_h1 back to lambdas

_p Finally we can replace names by their lambda expressions and get the same result using lambdas only

{pre
'{{lambda {:n} {:n 
  {lambda {:x} :x•} #}}  
  {{lambda {:n}  
   {{lambda {:c} {:c 
     {lambda {:a :b} :b}}} {{:n 
      {lambda {:p}
      {{lambda {:a :b :c} {:c :a :b}} 
       {{lambda {:n :f :x} {:f {:n :f :x}}}
        {{lambda {:c} {:c 
          {lambda {:a :b} :a}}} :p}}
          {{lambda {:n :m :f :x} {:n {:m :f} :x}} 
           {{lambda {:c} {:c 
             {lambda {:a :b} :a}}} :p} 
             {{lambda {:c} {:c 
               {lambda {:a :b} :b}}} :p}}}}}
               {{lambda {:a :b :c} {:c :a :b}}
                 {lambda {:f :x} {:f :x}} 
                  {lambda {:f :x} {:f :x}}}}}} 
                   {lambda {:f :x} {:f {:f {:f {:f {:f {:f :x}}}}}}}}}

{center 6! = 720}
}

_p A gem of arithmetic in a beautiful frozen cascade of lambdas, illustrating the power of this simple idea: defining numbers as {b iterators} allows to build algorithms behaving as static nested functions. No loop, no recursive process, just nested structures as are, for instance, the logic gates in a computer, just interconnected arrays of static gates through which tides of bits percolate.

_p Finally needing nothing but words, abstractions, applications flying on an empty dictionary.

_p The trip can [[begin|?view=start]]...

{uncover data/amelie_poulain.jpg 100 700 Amélie Poulain loves the lambada.}

_p {i alain marty | 2022/12/22 - 2023/01/05} | [[HN|https://news.ycombinator.com/edit?id=35648568]]
}

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

{style 
@font-face {
  font-family: 'Quicksand';
  src: url(data/quicksand.woff) format('woff');
}

body { background:#fff; }  
#page_frame { border:0; background:transparent; width:600px; margin-left:0; }
#page_content { 
 background:transparent; color:#000; border:0; width:3000px; box-shadow:0 0 0; 
 font:normal 1.1em Quicksand, optima;  
 }

pre { box-shadow:0 0 0px #000; padding:10px; background:#eee; }
}