lambdaspeech :: nutshell

2 | list | login |load

| |

_img http://epsilonwiki.free.fr/portail/data/code_mineur.jpg

_h1 the power of substitution in a nutshell

_p Following [[wikipedia|https://en.wikipedia.org/wiki/Lambda_calculus]], « {i the λ-calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation that can be used to simulate any Turing machine. It was first introduced by mathematician Alonzo Church in the 1930s as part of his research of the foundations of mathematics. } » A quick and clear introduction to λ calculus can be seen in  [[Raul Rojas|https://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf]].

_p '{lambda talk}, the programming language used in this wiki, is a foreign dialect of λ calculus. In this page we will stay at the lowest level of '{lambda talk}, in the infrastructure, without any primitive, any syntactic sugar, focusing on "{i the power of substitution}".

_h2 1. syntax & evaluation

_p Following λ calculus, we will define '{lambda talk} expressions on a reduced set of rules, {i words, abstractions} and {i applications}:

{pre
expression := word: [^\s{}]*, any chars except spaces and curly braces
           | abstraction: '{lambda {word*} expression}
           | application: '{expression expression}
}

{blockquote

_h3 details you can skip at first reading.

_p Imagine these expressions written sequentially on a long "stripe". A window - based on regular expressions created by Stefen Coole Kleene in the 1950s - goes back and forth and evaluates them, step by step, until all expressions have been replaced by words. A kind of {i Turing Machine}.

_p The implementation of '{lambda talk} insures that expressions are evaluated following these rules:

_ul words are evaluated to themselves,
_ul abstractions are evaluated before applications and at runtime, create an anonymous function added to a dictionary and return its reference,
_ul applications are evaluated from inside out and return sequences of words,
_ul the dictionary is supposed initially empty.

_p Anonymous functions, called lambdas, created by abstractions have the following behaviour:
_ul they can be used as arguments, as return values and can be nested,
_ul called with a number of values equal to the number of arguments, a lambda returns a value,
_ul called with a number of values lesser the number of arguments, a lambda memorizes them and returns a new lambda waiting for the missing ones, allowing currying and partial application,
_ul called with a number of values greater the number of arguments, the last argument gets extra values and the lambda returns a value, allowing variadicity.

_p The environment in which works a lambda is defined by its list of arguments. Lambdas have no free variables getting their values from an outer lambda. When needed, outer lambda's values must be redefined in the inner lambda's list of arguments. Currying and partial application can be used as a workaround to the lack of closure.
}

_h2 2. what can be done with so little?

_p We can replace words in a sentence, for instance swap words

{pre
'{{lambda {x y} bla bla y x bla bla} hello world}
-> {{lambda {x y} bla bla y x bla bla} hello world}
}

_p Lambdas can be nested, we can swap and capitalize

{pre
'{{lambda {h w}                     
 {{lambda {x y} bla bla y x bla bla} 
  hello world}}
  H W}
-> {{lambda {h w} {{lambda {x y} bla bla y x bla bla} hello world} } H W}
}

_p We can group 2 words and select each

{pre
'{{lambda {z}           
 {z {lambda {x y} x}}}
  {{lambda {x y z}
   {z x y}}            Hello World
}}
-> {{lambda {z}
 {z {lambda {x y} x}}}
  {{lambda {x y z}
   {z x y}}
    Hello World}}

'{{lambda {z}              
 {z {lambda {x y} y}}}
  {{lambda {x y z}
   {z x y}}            Hello World
}}
-> {{lambda {z}
 {z {lambda {x y} y}}}
  {{lambda {x y z}
   {z x y}}
    Hello World}}
}

_p Lambdas can be {i very deeply} nested and we can build a list and recursively display its elements

{pre 
'{{lambda {k}                   
 {{lambda {f k} {f f k}}
  {lambda {f k}
   {{{{lambda {z} {z
    {{lambda {x y} x}
     {lambda {z} {z
      {lambda {x y} y}}}}
       {lambda {z} {z
        {lambda {x y} x}}}}} k}
         {{lambda {x y z} {z x y}}
          {lambda {f k} }
           {lambda {f k}
            {{lambda {z} {z 
             {lambda {x y} x}}} k} {f f 
              {{lambda {z} {z 
               {lambda {x y} y}}} k}} } }} f k}} k}} 
                {{lambda {x y z} {z x y}} hello
                {{lambda {x y z} {z x y}} brave
                {{lambda {x y z} {z x y}} new 
                {{lambda {x y z} {z x y}} world
                 {lambda {x y} y}}}}}}
-> {{lambda {k}
 {{lambda {f k} {f f k}}
  {lambda {f k}
   {{{{lambda {z} {z
    {{lambda {x y} x}
     {lambda {z} {z
      {lambda {x y} y}}}}
       {lambda {z} {z
        {lambda {x y} x}}}}} k}
         {{lambda {x y z} {z x y}}
          {lambda {f k} }
           {lambda {f k}
            {{lambda {z} {z 
             {lambda {x y} x}}} k} {f f 
              {{lambda {z} {z 
               {lambda {x y} y}}} k}} } }} f k}} k}} 
                {{lambda {x y z} {z x y}} hello
                {{lambda {x y z} {z x y}} brave
                {{lambda {x y z} {z x y}} new 
                {{lambda {x y z} {z x y}} world
                 {lambda {x y} y}}}}}}
}

_p Well, at this point, for so little, {i it can't be said that life is easy}!

_h2 3. introducing names

_p In order to make things easier, we introduce {code '{def word expression}}, a second abstraction allowing to give a name to any expression and anonymous functions. For instance:

{pre
'{def HI Hello World} 
-> {def HI Hello World}
HI, I just say '{HI} 
-> HI, I just say {HI}

'{def SWAP {lambda {x y} y x}} 
-> {def SWAP {lambda {x y} y x}}
'{SWAP Hello World} 
-> {SWAP Hello World}

'{def letter {lambda {:name :city}
Dear :name
 It was a pleasure to see you in :city
 Best regards
 Alain
}}
-> {def letter {lambda {:name :city}
Dear :name
 It was a pleasure to see you in :city
 Best regards
 Alain
}}

'{letter Colette Villeneuve de la Raho} ->
 
{letter Colette Villeneuve de la Raho}

}

_p Now we can build a set of 8 useful functions:

{pre
'{def | {lambda {x y} x}}          -> {def | {lambda {x y} x}}          // true
'{def ø {lambda {x y} y}}          -> {def ø {lambda {x y} y}}          // false
'{def [] {lambda {x y z} {z x y}}} -> {def [] {lambda {x y z} {z x y}}}         // pair
'{def [ {lambda {z} {z |}}}        -> {def [ {lambda {z} {z |}}}          // left
'{def ] {lambda {z} {z ø}}}        -> {def ] {lambda {z} {z ø}}}          // right
'{def ? {lambda {z} {z {| ]} [}}}  -> {def ? {lambda {z} {z {| ]} [}}}          // iszero?
'{def ¿ {lambda {z} {z {| [} ]}}}  -> {def ¿ {lambda {z} {z {| [} ]}}}          // isnotzero?
'{def Y {lambda {f k} {f f k}}}    -> {def Y {lambda {f k} {f f k}}}          // Y combinator
}

_p And begin our exploration.

_h2 4. booleans

_p Note that the {code |} and {code ø} functions use to be called {code true} and {code false}. Let's define 3 other boolean functions, {code [&& || !=]}, ie {code [AND OR NOT]}:

{pre
'{def && {lambda {x y} {x y ø}}} -> {def && {lambda {x y} {x y ø}}}
'{&& | |} -> {&& | |}
'{&& | ø} -> {&& | ø}
'{&& ø |} -> {&& ø |}
'{&& ø ø} -> {&& ø ø}

'{def || {lambda {x y} {x | y}}}  -> {def || {lambda {x y} {x | y}}}
'{|| | |} -> {|| | |}
'{|| | ø} -> {|| | ø}
'{|| ø |} -> {|| ø |}
'{|| ø ø} -> {|| ø ø}

'{def != {lambda {x} {x ø |}}}   -> {def != {lambda {x} {x ø |}}}
'{!= |} -> {!= |}
'{!= ø} -> {!= ø}

'{def IF {lambda {z x y} {z x y}}}  -> {def IF {lambda {z x y} {z x y}}}  
'{IF | [ ]}  -> {IF | [ ]}
'{IF ø [ ]}  -> {IF ø [ ]}  
}

_h2 5. pairs

_p We have already defined the data structure {code pair} with its constructor, {code []} and two accessors {code [} & {code ]}

{pre
'{def P {[] hello world}} -> {def P {[] hello world}}

'{[ {P}} -> {[ {P}}
'{] {P}} -> {] {P}}
}

_p Remember that {code []} is waiting for 3 values and gets only 2. It's a partial application returning a function waiting for the missing one {code '{lambda {z} {z hello world}}}. So, the application of {code [} or {code ]} will select {b hello} or {b world}. Another way to create closures...

_h2 6. lists

_p Nesting {code pairs} we build lists

{pre
'{def L {[] hello {[] brave {[] new {[] world ø}}}}}
-> {def L {[] hello {[] brave {[] new {[] world ø}}}}}
}

_p Each item of the list can be accessed and successive rest of the list tested

{pre
'{[ {L}}             -> {[ {L}}     and test '{? {] {L}}}              -> {? {] {L}}}
'{[ {] {L}}}         -> {[ {] {L}}}     and test '{? {] {] {L}}}}          -> {? {] {] {L}}}}
'{[ {] {] {L}}}}     -> {[ {] {] {L}}}}       and test '{? {] {] {] {L}}}}}      -> {? {] {] {] {L}}}}}
'{[ {] {] {] {L}}}}} -> {[ {] {] {] {L}}}}}     and test '{? {] {] {] {] {L}}}}}}  -> {? {] {] {] {] {L}}}}}}
}

_h2 7. recursion

_p The previous sequence of selections and tests leads to a recursive algorithm

{pre
'{def D
 {lambda {z}
  {{{? z} {[]
   {lambda {z} }
   {lambda {z} {[ z} {D {] z}}}}} z}}}
-> {def D
 {lambda {z}
  {{{? z} {[]
   {lambda {z} }
   {lambda {z} {[ z} {D {] z}}}}} z}}}

'{D {L}} -> {D {L}}
}

_p Need some explanations?

{blockquote

_h3 details you can skip at first reading.

_p Let's explode and comment the recursive algorithm

{pre
'{def D                         // begin of def
 {lambda {z}                   // begin of lambda
  {                            // begin of force part
   {                           // begin of test part
    {? z}                      // test returning [ or ]
     {[]                       // begin of a pair
      {lambda {z}              // begin of lambda creating the left word
                               // does nothing and exit
      }                        // end of left lambda            
      {lambda {z}              // begin of lambda creating the right word
              {[ z}            // displays the list's first element
              {D {] z}}        // recurses on the list's rest
      }                        // end of right lambda
     }                         // end of pair
    }                          // end of test part
  z}                           // end of force part with z
 }                             // end of lambda
}                              // end of def 
}

_p The "plain" '{lambda talk} has a special form {b let} - a syntactic sugar - which help to trace the recursion:

{pre
'{def R
 {lambda {z}
  {let { {:one {lambda {z} }}
         {:two {lambda {z} {[ z} {R {] z}}}}
         {z z}   // z must be redefined, a kind of manual closure
       }
       {{{? z} {[] :one :two}} z}
}}}

if '{? z} = ] 
then '{{{? z} {[] :one :two}} z}
     -> '{{] {[] :one :two}} z} 
     -> '{:two z} 
     -> '{{lambda {z} {[ z} {R {] z}}} z}
     -> '{[ z} '{R {] z}}
     -> hello '{R {] z}}    // we got hello and call R again on the rest of the list

and so on until '{? z} = [ 
then '{{{? z} {[] :one :two}} z} 
     -> '{{[ {[] :one :two}} z} 
     -> '{:one z} 
     -> '{{lambda {z} } z}  // nothing to do
     -> stop
}

_p Recursion is a good example of how lambdas, hiding expressions from evaluation, help to introduce "laziness" in a by default "eager" evaluation process.
}

_h2 8. Y combinator

_p Notice that the expression {code '{D {L}}} and the last example given in section {b 2. what can be done with so little?} lead to the same value. They are equivalent expressions. We are going to show how we can go back from {code '{D {L}}} to an expression made exclusively of words and lambdas.

_ul 1. translate {code D} into an almost recursive algorithm

{pre
'{def AD                          
 {lambda {f k}
  {{{? k} {[]
   {lambda {f k} }
   {lambda {f k} {[ k} {f f {] k}}}}} f k}}}
-> {def AD
 {lambda {f k}
  {{{? k} {[]
   {lambda {f k} }
   {lambda {f k} {[ k} {f f {] k}}}}} f k}}}
}

_ul 2. and use the Y combinator {code '{def Y {lambda {f k} {f f k}}}}

{pre
'{Y AD {L}}                       
-> {Y AD {L}}
}

_ul 3. then compose {code Y} and {code AD}

{pre
'{def YD                     
 {lambda {k}
  {{lambda {f k} {f f k}}
   {lambda {f k}
    {{{? k} {[]
     {lambda {f k} }
     {lambda {f k} {[ k} {f f {] k}}}}} f k}} k}}}
-> {def YD 
 {lambda {k}
  {{lambda {f k} {f f k}}
   {lambda {f k}
    {{{? k} {[]
     {lambda {f k} }
     {lambda {f k} {[ k} {f f {] k}}}}} f k}} k}}}

'{YD {L}}
-> {YD {L}}
}

_ul 4. build an IIFE (Immediately Invoked Function Expression)

{pre
'{{lambda {k}                  
  {{lambda {f k} {f f k}}
   {lambda {f k}
    {{{? k} {[]
     {lambda {f k} }
     {lambda {f k} {[ k} {f f {] k}}}}} f k}} k}} {L}}
-> {{lambda {k}
  {{lambda {f k} {f f k}}
   {lambda {f k}
    {{{? k} {[]
     {lambda {f k} }
     {lambda {f k} {[ k} {f f {] k}}}}} f k}} k}} {L}}
}

_ul 5. and replace all names by their lambda expressions

{pre
'{{lambda {k}                 
 {{lambda {f k} {f f k}}
  {lambda {f k}
   {{{{lambda {z} {z
    {{lambda {x y} x}
     {lambda {z} {z
      {lambda {x y} y}}}}
       {lambda {z} {z
        {lambda {x y} x}}}}} k}
         {{lambda {x y z} {z x y}}
          {lambda {f k} }
           {lambda {f k}
            {{lambda {z} {z 
             {lambda {x y} x}}} k} {f f 
              {{lambda {z} {z 
               {lambda {x y} y}}} k}} } }} f k}} k}} 
                {{lambda {x y z} {z x y}} hello
                {{lambda {x y z} {z x y}} brave
                {{lambda {x y z} {z x y}} new 
                {{lambda {x y z} {z x y}} world
                 {lambda {x y} y}}}}}}
-> {{lambda {k}
 {{lambda {f k} {f f k}}
  {lambda {f k}
   {{{{lambda {z} {z
    {{lambda {x y} x}
     {lambda {z} {z
      {lambda {x y} y}}}}
       {lambda {z} {z
        {lambda {x y} x}}}}} k}
         {{lambda {x y z} {z x y}}
          {lambda {f k} }
           {lambda {f k}
            {{lambda {z} {z 
             {lambda {x y} x}}} k} {f f 
              {{lambda {z} {z 
               {lambda {x y} y}}} k}} } }} f k}} k}} 
                {{lambda {x y z} {z x y}} hello
                {{lambda {x y z} {z x y}} brave
                {{lambda {x y z} {z x y}} new 
                {{lambda {x y z} {z x y}} world
                 {lambda {x y} y}}}}}}
}

_p That's it!

_h2 9. and so what?

_p At this point we came back to the fundamentals, words, abstractions and applications. And we could go on building new data structures, beginning with natural numbers and a full set of arithmetic operators. This is figured in [[kiss]], [[paper|?view=factory_201902_paper]] and other pages.

_p Well, it's out of the scope of this page ... but just one more funny example! This is a double recursive algorithm, the {b Towers of Hanoï} game, using a list of four discs called "{b hello, brave, new & world}", {i without any arithmetic}:

{pre
'{def hanoi
 {lambda {:n :from :to :via}
  {{{? :n} {[] 
   {lambda {:n :from :to :via} }
   {lambda {:n :from :to :via}
    {hanoi {] :n} :from :via :to}
     {br} move disc {b {[ :n}} from tower :from to tower :to 
    {hanoi {] :n} :via :to :from} }}}
   :n :from :to :via}}}
-> {def hanoi
 {lambda {:n :from :to :via}
  {{{? :n} {[] 
   {lambda {:n :from :to :via} }
   {lambda {:n :from :to :via}
    {hanoi {] :n} :from :via :to}
     {br} move disc {b {[ :n}} from tower :from to tower :to 
    {hanoi {] :n} :via :to :from} }}}
   :n :from :to :via}}}

'{hanoi {L} A B C}
-> {hanoi {L} A B C}
}

_p Got it? Finally I just ask this question:

{center {i 
Is there a quicker - if not easier - way to introduce pairs, lists and recursion?{br}
And to share it on the web?
}}

_p Welcome in the '{lambda way} project.

_p Alain Marty ({i 2019/06/22})

{WATCH}

{style ;;
body { background:#8cc; }
.page_menu { background:transparent; }
#page_content { font:normal 1.0em optima; color:#800}
pre { box-shadow:0 0 8px #000; padding:5px; background:#ffe; }
blockquote { padding:0 5px; font:normal 0.6em courier; color:blue; }
}

{script ;;
 function HMS( w ) {
    var d = new Date(),
        h = d.getHours(),
        m = d.getMinutes(),
        s = d.getSeconds();
    document.getElementById('hours').style.width = (w/24*h) + 'px';
    document.getElementById('hours').innerHTML = h;
    document.getElementById('minutes').style.width = (w/60*m) + 'px';
    document.getElementById('minutes').innerHTML = m;
    document.getElementById('seconds').style.width = (w/60*s) + 'px';
    document.getElementById('seconds').innerHTML = s;
  }
setInterval( HMS, 1000, 600 );
}

{{hide}
 {def HMS {lambda {:hms :back :col}
  {div
   {@ id=":hms"
      style="width:0px; height:5px;
             text-align:right; padding-right:5px;
             background::back; color::col;
             line-height:0.4em;
             text-shadow:0 0 8px #000; font-weight:bold;"
}}}}

{def WATCH 
{div {@ style="box-shadow:0 0 8px #000;
               background:#444; 
               border:1px solid #fff;
               margin-bottom:10px;"}
{HMS hours #f00 #fff}
{HMS minutes #0f0 #fff}
{HMS seconds #00f #fff} 
}}
}