lambdaway :: fr2c

1 | list | login |load

| |

_h1 funny things with lambdas

{{block}
;; {uncover https://figurinepop.com/public/agnes1_2.jpg 100 800 Agnes loves [[rewriting systems|https://en.wikipedia.org/wiki/Rewriting]].}

_h2 introduction

_p The following [[λ-calculus|https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-Lambda-Calculus-Notes.pdf]] fundamental expression

{h2 λw.x w}

_p rewritten using the lambdatalk syntax

{h2 '{{lambda {w} x} w}}

_p where {b w} is any word and {b x} is any expression, can be considered as a simple {b [[term rewriting|https://en.wikipedia.org/wiki/Rewriting]] process}. In this first example

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

_p it's easy to understand that this expression is just a "stenographic/cryptic" way to say

{center 
« Please replace {b :a} by {b Bond} in "{b My name is :a, James :a.}" »
}

_p This second example with two words to replace

{pre
'{{lambda {:a :b} 
           My first name is :a and my second name is :b.
         } James Bond}
-> {{lambda {:a :b} My first name is :a and my second name is :b.} James Bond}
}

_p is no more difficult to understand. Finally it's easy to see that this last expression

{pre
'{{lambda {:a :b} :b :a} James Bond}
-> {{lambda {:a :b} :b :a} James Bond} 
}

_p {b swaps} two words, just saying {b « Please replace :a and :b in ":b :a" by James and Bond » } where conjunctions like {b by, and, in} have been replaced by a well balanced set of curly braces, {b '{}}, and the verb {b replace} has been renamed {b lambda} for historical reasons.

_p And so what?
}

{{block}
_h2 on the way to code

_p In order to make this swapping process easier to read and write, we will split it into two steps:

_ul 1) let's call {b SWAP} the inner expression:

{pre 
'{def SWAP {lambda {:a :b} :b :a}}
-> {def SWAP {lambda {:a :b} :b :a}}
}
_ul 2) let's rewrite the entire expression using this name: 
{pre 
'{SWAP James Bond}
-> {SWAP James Bond} 
}

_p We just have built a function, {b SWAP}, and have applied it to two words. 
_p That's all! 
_p Welcome in the wonderful land of programming! The true amazing discovery is that with such a very simple process we can build a true programming language, full of {b data & control structures}, booleans, pairs, lists, recursion, numbers, ..., everything you can imagine.
}

{{block}
_h2 booleans & pairs

_p Fasten your seat belts, let's go without too many explanations, see [[coding]] if you need them, be aware that all code in this page is active and can be understood by editing/testing it.

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

'{def PAIR {lambda {:a :b :c} {:c :a :b}}} 
-> {def PAIR {lambda {:a :b :c} {:c :a :b}}}
'{def LEFT {lambda {:c} {:c TRUE}}}
-> {def LEFT {lambda {:c} {:c TRUE}}}
'{def RIGHT {lambda {:c} {:c FALSE}}}
-> {def RIGHT {lambda {:c} {:c FALSE}}}
'{def P.DISP {lambda {:p} ({LEFT :p} {RIGHT :p})}}
-> {def P.DISP {lambda {:p} ({LEFT :p} {RIGHT :p})}}

'{def P {PAIR a b}}
-> {def P {PAIR a b}}
'{LEFT {P}}
-> {LEFT {P}}
'{RIGHT {P}}
-> {RIGHT {P}}
'{P.DISP {P}}
-> {P.DISP {P}}

'{def NIL {lambda {:a} TRUE}}
-> {def NIL {lambda {:a} TRUE}}
'{def NIL? {lambda {:c} {:c {lambda {:a :b} FALSE}}}}
-> {def NIL? {lambda {:c} {:c {lambda {:a :b} FALSE}}}}

'{NIL? NIL}
-> {NIL? NIL}
'{NIL? {P}}
-> {NIL? {P}}
}

_p Note that the {b PAIR} function waits for three values and gets only two. This is partial application. The result is a function waiting for the missing one. In lambdatalk lambdas can't have free variables (no closure) but they can be de facto partially called. See [[coding]] for more explanations.
}

{{block}
_h2 lists

_p A {b list} is a pair whose left term is à word and the right term is a pair or NIL.

{pre
'{def L {PAIR a {PAIR b {PAIR c {PAIR d NIL}}}}}
}

_p Because defining lists this way is boring we will use for convenience a function coming from lambdatalk, see note ***.

{pre
'{def L.NEW        // see note *** 
 {lambda {:s}
  {PAIR {S.first :s}
   {if {S.empty? {S.rest :s}}
    then NIL 
    else {L.NEW {S.rest :s}}}}}}  
-> {def L.NEW
 {lambda {:s}
  {PAIR {S.first :s}
   {if {S.empty? {S.rest :s}}
    then NIL 
    else {L.NEW {S.rest :s}}}}}}

'{def L {L.NEW a b c d}}
-> {def L {L.NEW a b c d}}
}

_p Now let's go back to the restricted area. A list is a recursive data structures. We will display its elements using recursion

{pre
'{def L.DISP    // display a list
 {def L.DISP.r
  {lambda {:l}
   {{IF {NIL? {RIGHT :l}}
    {lambda {:l} {LEFT :l}}
    {lambda {:l} {LEFT :l} {L.DISP.r {RIGHT :l}}}} :l}}}
 {lambda {:l}
  ({L.DISP.r :l})}}
-> {def L.DISP
 {def L.DISP.r
  {lambda {:l}
   {{IF {NIL? {RIGHT :l}}
    {lambda {:l} {LEFT :l}}
    {lambda {:l} {LEFT :l} {L.DISP.r {RIGHT :l}}}} :l}}}
 {lambda {:l}
  ({L.DISP.r :l})}}

'{L.DISP {L}}
-> {L.DISP {L}}
}

_p Note how we have introduced lazyness via lambdas. Using this pattern we will reverse a list. concatenate two lists and more.

{pre
'{def L.REV    // reverse a list
 {def L.REV.r
  {lambda {:a :b}
   {{IF {NIL? :a}
    {lambda {:a :b } :b}
    {lambda {:a :b}
     {L.REV.r {RIGHT :a} {PAIR {LEFT :a} :b}}}} :a :b}}}
 {lambda {:l}
  {L.REV.r :l NIL}}}
-> {def L.REV
 {def L.REV.r
  {lambda {:a :b}
   {{IF {NIL? :a}
    {lambda {:a :b } :b}
    {lambda {:a :b}
     {L.REV.r {RIGHT :a} {PAIR {LEFT :a} :b}}}} :a :b}}}
 {lambda {:l}
  {L.REV.r :l NIL}}}

'{L.DISP {L.REV {L}}}
-> {L.DISP {L.REV {L}}}

'{def L.CONCAT    // concatenate two lists
 {lambda {:a :b}
  {{IF {NIL? :a}
   {lambda {:a :b} :b}
   {lambda {:a :b}
    {PAIR {LEFT :a} {L.CONCAT {RIGHT :a} :b}}} } :a :b}}}
-> {def L.CONCAT
 {lambda {:a :b}
  {{IF {NIL? :a}
   {lambda {:a :b} :b}
   {lambda {:a :b}
    {PAIR {LEFT :a} {L.CONCAT {RIGHT :a} :b}}} } :a :b}}}

'{def A {L.NEW 1 2 3}} // yes some words can be numbers, 1+1=2
-> {def A {L.NEW 1 2 3}} = {L.DISP {A}}
'{def B {L.NEW 4 5 6}} 
-> {def B {L.NEW 4 5 6}} = {L.DISP {B}}
'{L.DISP {L.CONCAT {A} {B}}}
-> {L.DISP {L.CONCAT {A} {B}}}

'{def L.MAP
  // map a function to each term of a list, 
  // return a list
  {lambda {:f :a}
   {{IF {NIL? :a}
    {lambda {:f :a} NIL}
    {lambda {:f :a} {PAIR {:f {LEFT :a}}
                    {L.MAP :f {RIGHT :a}}}}} :f :a}}}
-> {def L.MAP
  {lambda {:f :a}
   {{IF {NIL? :a}
    {lambda {:f :a} NIL}
    {lambda {:f :a} {PAIR {:f {LEFT :a}} {L.MAP :f {RIGHT :a}}}}} :f :a}}}

'{L.DISP {L.MAP sqrt {B}}}
-> {L.DISP {L.MAP sqrt {B}}}    // √4, √5, √6
'{L.DISP {L.MAP {lambda {:i} {pow 2 :i}} {B}}}
-> {L.DISP {L.MAP {lambda {:i} {pow 2 :i}} {B}}}    // 2^4, 2^5, 2^6
 
'{def L.REDUCE    
  // return the application of a function 
  // to each elements of a list
  {lambda {:f :z :a}
   {{IF {NIL? :a}
    {lambda {:f :z :a} :z}
    {lambda {:f :z :a} {:f {LEFT :a}
                           {L.REDUCE :f :z {RIGHT :a}}}}}
             :f :z :a}}} 
-> {def L.REDUCE
  {lambda {:f :z :a}
   {{IF {NIL? :a}
    {lambda {:f :z :a} :z}
    {lambda {:f :z :a} {:f {LEFT :a} {L.REDUCE :f :z {RIGHT :a}}}}} :f :z :a}}}

'{L.REDUCE + 0 {B}}   // equivalent to 0+4+5+6
-> {L.REDUCE + 0 {B}}
'{L.REDUCE * 1 {B}}   // equivalent to 1*4*5*6
-> {L.REDUCE * 1 {B}}
}

_p We used numbers in some examples and they are supposed to be defined elsewhere as lambda expressions. See [[coding]] to see how.
}

{{block}
_h2 sort

_p As a last and useful example we choose the insertion sort algorithm. See [[sort]].

{center
{pre
[3,4,2,5,9,1,2] []
[4,2,5,9,1,2]  [3]
[2,5,9,1,2]  [3,4]
[5,9,1,2]  [2,3,4]
[9,1,2]  [2,3,4,5]
[1,2]  [2,3,4,5,9]
[2]  [1,2,3,4,5,9]
[] [1,2,2,3,4,5,9]
}}

_p leading to

{prewrap
'{def LT?  // see note ***
 {lambda {:a :b} 
  {if {< :a :b} then TRUE else FALSE}}}
-> {def LT? {lambda {:a :b} {if {< :a :b} then TRUE else FALSE}}}

'{def L.INSERT
 {lambda {:x :l} 
  {{IF {NIL? :l} 
   {lambda {:x :l} {PAIR :x NIL}}
   {lambda {:x :l} 
    {{lambda {:x :l}
     {{IF {LT? :x {LEFT :l}} 
      {lambda {:x :l} {PAIR :x :l} }
      {lambda {:x :l} {PAIR {LEFT :l}
                      {L.INSERT :x {RIGHT :l}}}}
   } :x :l}
   } :x :l}}
   } :x :l}}} 
-> {def L.INSERT
 {lambda {:x :l} 
  {{IF {NIL? :l} 
   {lambda {:x :l} {PAIR :x NIL}}
   {lambda {:x :l} 
    {{lambda {:x :l}
     {{IF {LT? :x {LEFT :l}} 
      {lambda {:x :l} {PAIR :x :l} }
      {lambda {:x :l} {PAIR {LEFT :l} {L.INSERT :x {RIGHT :l}}}}
   } :x :l}
   } :x :l}}
   } :x :l}}}

'{def L.SORT    // sort a list of numbers in increasing order
 {lambda {:l} 
  {{IF {NIL? :l} 
   {lambda {:l} NIL} 
   {lambda {:l} 
    {L.INSERT {LEFT :l} {L.SORT {RIGHT :l}}}}} :l}}}
-> {def L.SORT
 {lambda {:l} 
  {{IF {NIL? :l} 
   {lambda {:l} NIL} 
   {lambda {:l} 
    {L.INSERT {LEFT :l} {L.SORT {RIGHT :l}}}}} :l}}}
}

_p Testing on a list of 100 randomly generated natural numbers

{prewrap
'{def NUMBERS 
 {S.reduce 
  {lambda {:l :i}
   {PAIR {round {* {random} 1000}} :l}} 
    NIL {S.serie 1 100}}}
-> {def NUMBERS 
 {S.reduce 
  {lambda {:l :i}
   {PAIR {round {* {random} 1000}} :l}} 
    NIL {S.serie 1 100}}}

'{L.DISP {NUMBERS}} 
-> {L.DISP {NUMBERS}}

'{L.DISP {L.SORT {NUMBERS}}}
-> {L.DISP {L.SORT {NUMBERS}}}
 
}
}

{{block}
_h2 conclusion

_p  Very quickly we could build a small set of functions allowing to sort an array of random numbers. Mainly using the only replace process initially defined as

{h2 '{{lambda {w} x} w}}

_p Funny, isnt'it? For detailed explanations see the page [[coding]] ... where you will discover a {b true} functional programming language. Using lambdatalk you could rewrite the {b sort} algorithm more easily:

{pre
'{def L.insert
 {lambda {:x :comp :l} 
  {if {nil? :l} 
   then {cons :x nil} 
   else {if {:comp :x {car :l}} 
   then {cons :x :l} 
   else {cons {car :l}
              {L.insert :x :comp {cdr :l}}}}}}}

'{def L.sort
 {lambda {:comp :l} 
  {if {nil? :l} 
   then nil 
   else {L.insert {car :l} :comp
                  {L.sort :comp {cdr :l}}}}}} 
}

_p My opinion is that coming back to the foundations is always useful to understand basic concepts like data and control structures, greadiness vs lazyness, recursion, closure vs unclosure, syntactic sugar and so on.

_p {i alain marty | 2021/11/08}

{hr}
_p {b Note ***:} {b L.NEW}, {b LT?} and {b NUMBERS} use lambdatalk primitives and are therefore outside the restricted scope of this page. Consider that they are optional and that they are only used here to avoid cluttering the page. See [[coding]].

_p [[HN|https://news.ycombinator.com/item?id=29158205]]
}

{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:5px; "}}
}

{style 
body { background:#444; } 
#page_frame { border:0; background:#444; width:600px; margin-left:0; }
#page_content { background:transparent; color:#fff; border:0; width:3800px; box-shadow:0 0 0; font-family:papyrus, 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; } 
}