lambdaway :: lambdacalc

2 | list | login |load

| |

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

_h1 lambda {sup (calc)}

_p A quick introduction to a tiny programming language, {b lambdacalc}, working in any web browser and reduced to {b words, abstractions, applications} & {b definitions}.

_h2 introduction

_p A lambdacalc 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, '{}
- 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}
}

_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,
- an application is evaluated to words, from inside out,
- a definition is evaluated to a word, from inside out,
- abstractions and definitions are evaluated before applications.
}

_p Note that abstractions are evaluated to JS anonymous functions stored in a dictionary supposed to be empty. No numbers, no arrays, nada. It's up to you to recreate everything from scratch.

_h2 first steps

{pre
- words       : james, bond, 123, #f00, :a, :b, ...

- abstraction : '{lambda {:a :b} :b :a}
                -> {lambda {:a :b} :b :a}     // the reference of an anonymous function

- definition  : '{def SWAP {lambda {:a :b} :b :a}}
               -> {def SWAP {lambda {:a :b} :b :a}}         // a name given to the anonymous function

- application : '{SWAP James Bond}
                -> {SWAP James Bond}           // the result of the application
}

_h2 IIFE

_p Here is an expression called an {b IIFE}, {b I}mmediately {b I}nvoked {b F}unction {b E}xpression, built on an abstraction and an application

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

_p This expression is preferably splitted into two parts

{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 Coding is building new named functions and applying them to words.

_h2 more on functions

_p {b HI} is a function waiting for two values, let's analyze its behaviour with different numbers of values

{pre
'{HI}                                         // no value
-> {HI} 
}

_p It's a new reference to the initial functionn '{lambda {:a :b} My name is :b, :a :b.}

{pre
'{HI James}                                   // only one values
-> {HI James}
}
  
_p It's the reference of a new function '{lambda {:b} My name is :b, James :b.}, memorizing the given value, {b James}, and waiting for the missing one.

{pre
'{HI James Bond}                              // two values
-> {HI James Bond}  
}

_p It's the awaited result.

{pre
'{HI Ludwig Mies van der Rohe}                // more than two values
-> {HI Ludwig Mies van der Rohe}  
}
_p Note that {b :a} got "Ludwig" and {b :b} got the last words, "Mies van der Rohe"

_p In lambdacalc functions accept {b naturally} any numbers of values, and it's useful.

_h2 pairs

_p As a useful application let's introduce the {b PAIR} function aggregating two words and {b LEFT} and {b RIGHT} accessing each of them.

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

'{def JB {PAIR James Bond}}
-> {def JB {PAIR James Bond}}

'{LEFT {JB}}
-> {LEFT {JB}}
'{RIGHT {JB}}
-> {RIGHT {JB}}
}

_p Note that {b '{PAIR James Bond}} is an example of partial application, {b PAIR} is waiting for 3 words and is given 2 only. The result is a function which will be given to {b LEFT} or {b RIGHT} to return {b James} or {b Bond}.

_h2 a few steps in arithmetic

_p The set of natural numbers is made of {b ZERO} and all its {b SUCC}essors. Following {b Alonzo Church} we write

{pre
'{def ZERO {lambda {:f :x} :x}}
-> {def ZERO {lambda {:f :x} :x}}

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

_p Because numbers are defined as functions, we need a function to display them, say as groups of dots {b •}

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

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

_p Note that {b THREE} could be also written as {b '{lambda {:f {:f {:f :x}}}}}, three times the application of some {b :f} function to some {b :x} value. Church numbers are {b iterators} {i per se} and we can use them to define the addition and the multiplication.

{pre
'{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 FIVE {ADD {TWO} {THREE}}} 
-> {def FIVE {ADD {TWO} {THREE}}}

'{def SIX {MUL {TWO} {THREE}}} 
-> {def SIX {MUL {TWO} {THREE}}}

'{CHURCH {FIVE}}
-> {CHURCH {FIVE}}
'{CHURCH {SIX}}
-> {CHURCH {SIX}}
}

_p Remember that lambdacalc doesn't know numbers, so we write them as dots, sorry.

_h2 factorial

_p Now let's consider the following process computing successive factorials

{pre
.                    a   b
[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]
[6 , 1*2*3*4*5*6] = [1 , 720] -> 6! = 720
and so on
}

_p Thanks to the {b PAIR} structure we can translate this process into code

{pre
'{def FAC.pair
 {lambda {:p}
  {PAIR {SUCC {LEFT :p}}
        {MUL {LEFT :p} {RIGHT :p}}
}}}
-> {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 Let's read:
_ul 1) the {b FAC.pair} function gets a pair {b p = [a,b]} and returns a pair {b p = [a+1,a*b]},

_ul 2) the FAC function computes {b n} iterations of FAC.pair starting on the pair [1,1], leading to the pair [n,n!] and finally returns the second, n!.

_p Finally {b FAC} and {b FAC.pair} can be joined in a unique function

{pre
'{def FAC
 {lambda {:n}  
  {RIGHT
   {{:n {lambda {:p}
         {PAIR {SUCC {LEFT :p}}
               {MUL {LEFT :p} {RIGHT :p}}}}}
        {PAIR {ONE} {ONE}}}}}}   
-> {def FAC
 {lambda {:n}  
  {RIGHT
   {{:n {lambda {:p}
         {PAIR {SUCC {LEFT :p}}
               {MUL {LEFT :p} {RIGHT :p}}}}}
        {PAIR {ONE} {ONE}}}}}}   
}

_p Here is the factorial of 6

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

_p Yes there are {b 720 dots}. Remember, lambdacalc doesn't know numbers, just words.

_h2 back to lambdas

_p Finally, we can forget names and, replacing them by their lambda expressions, we come back to a pure lambda expression for {b 6! = '{CHURCH {FAC {SIX}}}}

{pre
'{{lambda {:n} {:n 
  {lambda {:x} :x•} C}}  
  {{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}}}}}}}}}
}

_h2 conclusion

_p Nothing but words, abstractions, applications and an empty dictionary.

_p More can be seen in [[lambda_calculus]], [[the lambdaway project|?view=start]], [[coding]], ...

_p {i alain marty | 2023/01/01} | [[HN|https://news.ycombinator.com/item?id=34205084]]

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