lambdaway :: the_roots_of

1 | list | login |load

| |

_h1 the roots of coding

{{block}
_h2 introduction

_p [[Alan Kay|https://en.wikipedia.org/wiki/Alan_Kay]] is quoted as saying, after reading John McCarthy’s LISP-1.5 manual: « {i that was the big revelation to me […] when I finally understood that the half page of code on the bottom of page 13 of the Lisp 1.5 manual was Lisp in itself. These were “{b [[Maxwell’s Equations|?view=maxwell]] of Software!}” This is the whole world of programming in a few lines that I can put my hand over.} » See [[1|https://michaelnielsen.org/ddi/lisp-as-the-maxwells-equations-of-software/]], [[2|https://www.gnu.org/software/mes/manual/html_node/LISP-as-Maxwell_0027s-Equations-of-Software.html]], ...

{uncover https://upload.wikimedia.org/wikipedia/commons/c/cd/James_Clerk_Maxwell_Statue_Equations.jpg 100 650 [[The Maxwell's equations|?view=maxwell]]}

_p In my (humble) opinion and more generally, I think that the roots of coding can be built on a more simple foundation, a simple {b text rewriting} process.

_p In other words I think that the traditional approach to the art of coding is more than questionable. When Alan Kay and Paul Graham see "the Maxwell's Equations" in the hundred or so lines of code defining the {b LISP eval()} function, I think they are making a mistake. Whatever the beauty of the meta-circularity of the thing it does not seem to me to be wise to see it as the alpha and omega of the art of coding. I am now convinced that {b LISP} is not the right basis and that we must go back to its ancestor, the {b lambda-calculus}, to find it.

_p But it is still necessary not to remain with the academic reading over and over again reproduced by too smart logicians. I think we should go back to the very basis of this formal language, a simple text replacement process boosted by a judicious notation. And keep only the prefixed parenthetical syntax of LISP in its most universal form.

_p In this spirit a small homemade language, {b lambdatalk }, allows to conduct a simple and unshaded exploration of the fundamental concepts of all languages:

_ul 1. words as basic data
_ul 2. functions as basic operators
_ul 3. booleans and the concept of switching
_ul 4. pairs and the concept of data aggregation
_ul 5. lists and the concept of recursive structure
_ul 6. recursion as the mother of all algorithms.

_p Upon these bricks can be built an infinite world of algorithms understandable by a 13 years old child. In the present document we will show how the game called {b [[the Towers of Hanoi|https://en.wikipedia.org/wiki/Tower_of_Hanoi]]} can be solved using only a {b cascade of lambdas}, at the {b λ-calculus} level.

_p Let's go.
}

{{block}
_h2 1) the roots of lisp

_p First, what about the {i few lines} seen by Alan Kay as the “{b Maxwell’s Equations of Software!}”, the core of the universe of computing?
_p This is how [[Paul Graham|http://www.paulgraham.com/rootsoflisp.html]] builds the {b eval} function from a reduced set of seven primitives: "{u quote, atom, eq, cons, car, cdr & cond}":

{pre
; The Lisp defined in McCarthy's 1960 paper, translated into CL.
; Assumes only quote, atom, eq, cons, car, cdr, cond.
; Bug reports to lispcode@paulgraham.com.

(defun {b eval}. (e a)
  ({u cond}
    (({u atom} e) ({b assoc}. e a))
    (({u atom} ({u car} e))
     ({u cond}
       (({u eq} ({u car} e) 'quote) ({b cadr} e))
       (({u eq} ({u car} e) 'atom)  ({u atom}   ({b eval}. ({b cadr} e) a)))
       (({u eq} ({u car} e) 'eq)    ({u eq}     ({b eval}. ({b cadr} e) a)
                                    ({b eval}. ({b caddr} e) a)))
       (({u eq} ({u car} e) 'car)   ({u car}    ({b eval}. ({b cadr} e) a)))
       (({u eq} ({u car} e) 'cdr)   ({u cdr}    ({b eval}. ({b cadr} e) a)))
       (({u eq} ({u car} e) 'cons)  ({u cons}   ({b eval}. ({b cadr} e) a)
                                    ({b eval}. ({b caddr} e) a)))
       (({u eq} ({u car} e) 'cond)  ({b evcon}. ({u cdr} e) a))
       ('t ({b eval}. ({u cons} ({b assoc}. ({u car} e) a)
                        ({u cdr} e))
                  a))))
    (({u eq} ({b caar} e) 'label)
     ({b eval}. ({u cons} ({b caddar} e) ({u cdr} e))
            ({u cons} ({b list}. ({b cadar} e) ({u car} e)) a)))
    (({u eq} ({b caar} e) 'lambda)
     ({b eval}. ({b caddar} e)
            ({b append}. ({b pair}. ({b cadar} e) ({b evlis}. ({u cdr} e) a))
                     a)))))
}

_p with the following helper functions

{pre
(defun {b assoc}. (x y)
  ({u cond} (({u eq} ({b caar} y) x) ({b cadar} y))
        ('t ({b assoc}. x ({u cdr} y)))))

(defun {b evcon}. (c a)
  ({u cond} (({b eval}. ({b caar} c) a)
         ({b eval}. ({b cadar} c) a))
        ('t ({b evcon}. ({u cdr} c) a))))

(defun {b append}. (x y)
  ({u cond} (({b null}. x) y)
        ('t ({u cons} ({u car} x) ({b append}. ({u cdr} x) y)))))

(defun {b evlis}. (m a)
  ({u cond} (({b null}. m) '())
        ('t ({u cons} ({b eval}.  ({u car} m) a)
                  ({b evlis}. ({u cdr} m) a)))))

(defun {b pair}. (x y)
  ({u cond} (({b and}. ({b null}. x) ({b null}. y)) '())
        (({b and}. ({b not}. ({u atom} x)) ({b not}. ({u atom} y)))
         ({u cons} ({b list}. ({u car} x) ({u car} y))
               ({b pair}. ({u cdr} x) ({u cdr} y))))))

(defun {b null}. (x)
  ({u eq} x '()))

(defun {b list}. (x y)
  ({u cons} x ({u cons} y '())))

(defun {b and}. (x y)
  ({u cond} (x ({u cond} (y 't) ('t '())))
        ('t '())))

(defun {b not}. (x)
  ({u cond} (x '())
        ('t 't)))

(defun {b caar}. (x)
  ({u car} ({u car} x)))

(defun {b cadr}. (x)
  ({u car} ({u cdr} x)))

(defun {b caddr}. (x)
  ({u car} ({u cdr} ({u cdr} x))))

(defun {b caddar}. (x)
  ({u car} ({u cdr} ({u cdr} ({u car} x)))))
}

_p Well, that's not easy things! 
_p Could we make it any simpler?
_p I think so.
}

{{block}
_h2 2) text rewriting

_p I think that the roots of coding can be built on a more simple foundation, a simple {b text rewriting} process. For instance anyone can understand that this command

{pre
{b replace} :a and :b
     {b in} My first name is :a and my second is :b.
     {b by} James and Bond
}

_p should lead to this answer "{b My first name is James and my second is Bond.}"

_h3 2.1) lambdas
_p A general form for a text rewriting process could be

{pre
{b replace} :words
     {b in} some expression containing :words
     {b by} words
}

_p which is interesting to rewrite in a short Lispsish prefixed parenthesized form

{pre 
'{{lambda {:words} expression} words}
}

_p where for historical reasons {b lambda} is for {b replace} and the balanced set of curly braces replace the {b in, by, and} conjunctions. This strange syntax has two advantages:
_ul 1) it's rather easy to write an evaluator installed in a wiki returning the answer,
_ul 2) it will be a matter of "algebra" to combine several replacements leading to a full programming language.

_p And so, writing

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

_p will be evaluated to "{b My first name is James and my second is Bond.}", as expected.

_p {b That's all!}

_p The foundations of our language - let's call it {b lambdatalk} - are settled, we need nothing more. But {b OK!} it's a bit terce and should be difficult to use in real life, deep combinations of replacements would be unreadable. 
_p We need {b syntactic sugar}!

_h3 2.2) def

_p The special form {b '{lambda {:words} expression}} is the heart of the text replacement process and could be used alone everytime. In order to write and read code in a more pleasant way, we introduce a second special form to {b def}ine names bounded to expressions

{pre 
'{def name expression}
}

_p Using {b def} we can split the previous command into two steps:

_p 1) we give a name to the inner expresion, say {b HI}: 
{pre 
'{def HI
 {lambda {:a :b} 
   My first name is :a and my second is :b.
}}
-> {def HI
 {lambda {:a :b} 
   My first name is :a and my second is :b.
}}
}

_p 2) and we just replace the inner expression by {b HI}

{pre
'{HI James Bond}
-> {HI James Bond}
}

_p Welcome in the {b land of coding}, you just have built a {b function}, you have applied it to two words and you can do it again and again:

{pre
'{HI Ward Cunningham}
-> {HI Ward Cunningham}

'{HI Harry Potter}
-> {HI Harry Potter}

'{HI Monica Bellucci}
-> {HI Monica Bellucci}

...
}

_p Never forget the lambda expression under the names. Names are nothing but useful {b aliases} hiding complexity. It's called {b abstraction}. Coding is to build layers of abstractions and to play with.

_h3 2.3) one more thing

_p You may have wondered why {b function's arguments} - also called variables - are prefixed with a colon. This is a useful convention highlighting variables inside a sentence. But not only. Let's rewrite the {b HI} function without using this convention

{pre 
'{def HI'
 {lambda {a b} 
   My first name is a and my second is b.
}}
-> {def HI'
 {lambda {a b} 
   My first name is a and my second is b.
}}

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

_p {b Oooops!} Do you understand what the problem is? Yes, remember that it's nothing but a text rewriting process, every occurences of the {b a} character have been replaced by {b James} ... and it's not what we want. Prefixing arguments with a colon - or any other rarely used character, &, §, #,...  - is a way to fix the problem.

_p In programming languages it is not common to mark function variables in this way, but there is a counterpart: {b words and sentences must be protected}. Compare the same sentence written using lambdatalk and Javascript:

{pre
Lambdatalk:  My first name is :a and my second is :b.             
Javascript: "My first name is " + a + " and my second is " + b + "."
        or: `My first name is $'{a} and my second is $'{b}.`
}

_p In fact lambdatalk reverses the system, variables are marked and sentences are not, making easy concatenations between words and variables. Using lambdatalk text can be written as it is!

_p Now we have everything we need to explore the foundations of a programming language.

}

{{block}

_h2 3) booleans & pairs

_p Using exclusively the two {b lambda & def} special forms, we define eight useful {b basic functions} dealing with the inevitable {b booleans} and a powerful data structure, {b pairs}.

_h3 3.1) booleans
{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 Take the time to replace names by their lambda expressions and just {b do} the replacements, for example:

{pre
0: '{IF TRUE yes no}
1: '{{lambda {:a :b :c} {:a :b :c}} {lambda {:a :b} :a} yes no}
2: '{{lambda {:a :b} :a} yes no}
3: yes
}

_p Note how {b :a} has been replaced by the {b '{lambda {:a :b} :a}} function, {b :b} by {b yes} and {b :c} by {b no}.

_h3 3.2) pairs

{pre
'{def CONS {lambda {:a :b :c} {:c :a :b}}}             
-> {def CONS {lambda {:a :b :c} {:c :a :b}}}
'{def CAR {lambda {:c} {:c TRUE}}}                     
-> {def CAR {lambda {:c} {:c TRUE}}}
'{def CDR {lambda {:c} {:c FALSE}}}                    
-> {def CDR {lambda {:c} {:c FALSE}}}

'{def JB {CONS James Bond}}
-> {def JB {CONS James Bond}}
'{CAR {JB}}
-> {CAR {JB}}
'{CAR {JB}}
-> {CAR {JB}}
}

_p Once more take the time to replace names by their lambda expressions and just {b do} the replacements, for example:

{pre
0: '{CAR {JB}}
1: {{lambda {:c} {:c TRUE}} {CONS James Bond}}
2: '{{lambda {:c}
    {:c {lambda {:a :b} :a}}} {{lambda {:a :b :c} {:c :a :b}} James Bond}}
3: '{{lambda {:c} 
    {:c {lambda {:a :b} :a}}}  {lambda {:c} {:c James Bond}}}
4: '{{lambda {:c} {:c James Bond}} {lambda {:a :b} :a}}
5: '{{lambda {:a :b} :a} James Bond}
6: James
}

_p Yes, it's not so easy, the more tricky part being when

{pre
'{{lambda {:a :b :c} {:c :a :b}} James Bond}  // '{CONS James Bond}
}

_p is replaced by

{pre
'{lambda {:c} {:c James Bond}}
}

_p This is a good example of {b partial application}:

{pre
0: '{{lambda {:a :b :c} {:c :a :b}} James Bond}
1: '{{lambda {   :b :c} {:c James :b}}    Bond}  // :a got James
2: '{{lambda {      :c} {:c James Bond}}      }  // :b got Bond
3: '{lambda {:c} {:c James Bond}}                // :c is still unknown
}

_p So the result is a new function waiting for the missing one, and the rest is still the same text replacement process, which should have become familiar to you by now.

_h3 3.3) to be or not to be a pair

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

'{ISNIL NIL}
-> {ISNIL NIL}
'{ISNIL {JB}}
-> {ISNIL {JB}}
}

_p I leave you the pleasure to test this code by yourself.

_p Finally, remember the seven primitives {i coming from nowhere}: "{b quote, atom, eq, car, cdr, cons, & cond}" as the foundations of LISP. And note that the eight functions we have defined, {b TRUE, FALSE, IF, CONS, CAR, CDR, NIL, ISNIL}, are exclusively built on {b lambdas} and {b defs} and are small and simple. Once again, this is nothing but simple text rewriting.

_p It's time to solve the {b Towers of Hanoi}.
}

{{block}
_h2 4) lists

_p A {b list} is a pair whose left term is a word and the right term is a pair or {b NIL}. Using the previous bricks we can quickly define a {b list}

{pre
'{def LIST
 {CONS hello
  {CONS brave
   {CONS new
    {CONS world NIL}}}}}
-> {def LIST {CONS hello {CONS brave {CONS new {CONS world NIL}}}}}
}

_p and build a function to display it

{pre
'{def DISP
 {lambda {:l}
  {{IF {ISNIL :l}
   {lambda {:l} }
   {lambda {:l} {CAR :l} {DISP {CDR :l}}}} :l}}}
-> {def DISP
 {lambda {:l}
  {{IF {ISNIL :l}
   {lambda {:l} }
   {lambda {:l} {CAR :l} {DISP {CDR :l}}}} :l}}}

'{DISP {LIST}}
-> {DISP {LIST}}
}

_p {b That's all}. See detailled explanations in [[coding]], section {b recursion}.

_p We have quickly built a recursive control structure which is at the core of coding, {b recursion}. Defining and displaying a list is the first example of recursion. More examples can be seen in the [[coding]] page, from arithmetic to the Towers of Hanoï.

_h3 The Towers of Hanoi, what's that?

{uncover https://upload.wikimedia.org/wikipedia/commons/8/8d/Iterative_algorithm_solving_a_6_disks_Tower_of_Hanoi.gif 200 200}

_p Imagine a set of {b 6} disks of decreasing size stacked on a rod. The game consists in deplacing each disk to a second rod via a third one in respect of the following rule, "{b never put a disk on a smaller one}". The code is built on a doubly recursive function, don't worry for now if you don't understand details.

{pre
'{def HANOI          
 {lambda {:n :from :to :via}
  {{IF {ISNIL :n}
   {lambda {:n :from :to :via} }
   {lambda {:n :from :to :via}
    {HANOI {CDR :n} :from :via :to}
      {br} move {CAR :n} from tower :from to tower :to 
    {HANOI {CDR :n} :via :to :from} }}
   :n :from :to :via}}}
-> {def HANOI          
 {lambda {:n :from :to :via}
  {{IF {ISNIL :n}
   {lambda {:n :from :to :via} }
   {lambda {:n :from :to :via}
    {HANOI {CDR :n} :from :via :to}
      {div} move {CAR :n} from tower :from to tower :to 
    {HANOI {CDR :n} :via :to :from} }}
   :n :from :to :via}}}
}

_p The set of disks is defined as a list of words, {b Disk_1, Disk_2, ...}

{pre
'{def DISKS
 {CONS Disk_1
  {CONS Disk_2
   {CONS Disk_3
    {CONS Disk_4
     {CONS Disk_5 
      {CONS Disk_6 NIL}}}}}}}
-> {def DISKS
 {CONS Disk_1
  {CONS Disk_2
   {CONS Disk_3
    {CONS Disk_4
     {CONS Disk_5 
      {CONS Disk_6 NIL}}}}}}} 
}

_p And writing 
{pre
'{HANOI {DISKS} A B C}
}

_p displays the long sequence of moves

{pre
{HANOI {DISKS} A B C}
}

_p With 6 disks we have {b 2{sup 6}-1 = {- {pow 2 6} 1}} moves. With {b 64} disks this function would write {b 2{sup 64}-1 = 18446744073709551615} moves, a very very big number, a taste of infinite. If the legend were true, and if the priests were able to move disks at a rate of one per second, using the smallest number of moves, it would take them roughly {b 585 billion years to finish}, which is about 42 times the current age of the universe.

_p Recursion is great, isnt'it?

_p In this page we won't go further, and in order not to lose touch with the basics, the {b rewriting text} process, we have to come back to the fundamentals, thanks to a very simple function, the {b Y combinator}.
}

{{block}
_h2 5) back to lambda

_p The goal is to rewrite the expression {b '{HANOI {DISKS} A B C}} as a nested composition of lambdas, replacing all names by their lambda expressions.

_p First we rewrite the {b HANOI} function as {b AHANOI}, a function with a new argument, {b :g}, acting as a {b fixed point}, keeping the function's name all along its life.

{pre
'{def AHANOI                   // stands for "almost recursive HANOI"
 {lambda {:g :n :from :to :via} the
  {{IF {ISNIL :n}
   {lambda {:g :n :from :to :via} }
   {lambda {:g :n :from :to :via}
    {:g :g {CDR :n} :from :via :to}
      {br} move {CAR :n} from tower :from to tower :to 
    {:g :g {CDR :n} :via :to :from} }}
   :g :n :from :to :via}}}
-> {def AHANOI          
 {lambda {:g :n :from :to :via}
  {{IF {ISNIL :n}
   {lambda {:g :n :from :to :via} }
   {lambda {:g :n :from :to :via}
    {:g :g {CDR :n} :from :via :to}
      {br} move {CAR :n} from tower :from to tower :to 
    {:g :g {CDR :n} :via :to :from} }}
   :g :n :from :to :via}}}
}
_p Note that the functions's body doesn't contain anymore the function's name.

_p Then we define a very simple function, the {b Y combinator}, doubling the input and acting as a bridge
{pre
'{def Y {lambda {:f} {:f :f}}}
-> {def Y {lambda {:f} {:f :f}}}
}

_p Now, replacing {b HANOI} by a combination of {b Y} and {b HANOI}, {b '{Y AHANOI}}

{pre
'{{Y AHANOI} {DISKS} A B C}
->
move Disk_6 from tower A to tower C  
move Disk_5 from tower A to tower B  
move Disk_6 from tower C to tower B  
move Disk_4 from tower A to tower C
...
}

_p generates the same {b 63} moves, as expected.

_p The last step is to replace all names in {b '{{Y AHANOI} {DISKS} A B C} } by their lambda expressions - {b Y, AHANOI, DISKS} and {b IF, ISNIL, CAR, CDR, LIST} and {b CONS, NIL, TRUE, FALSE} - and get to the following {b cascade of lambdas}

{pre
'{{{lambda {:g} {:g :g}}
   {lambda {:g :n :from :to :via}
  {{{lambda {:a :b :c} {:a :b :c}}
    {{lambda {:c} {:c 
      {lambda {:a :b} 
       {lambda {:a :b} :b}}}} :n}
        {lambda {:g :n :from :to :via} }
         {lambda {:g :n :from :to :via} {:g :g 
         {{lambda {:c} {:c 
           {lambda {:a :b} :b}}} :n} :from :via :to} {br} move
           {{lambda {:c} {:c
             {lambda {:a :b} :a}}} :n} from tower :from to tower :to {:g :g 
             {{lambda {:c} {:c
               {lambda {:a :b} :b}}} :n} :via :to :from} }} :g :n :from :to :via}}}
               {{lambda {:a :b :c} {:c :a :b}} Disk_1
               {{lambda {:a :b :c} {:c :a :b}} Disk_2
               {{lambda {:a :b :c} {:c :a :b}} Disk_3
               {{lambda {:a :b :c} {:c :a :b}} Disk_4
               {{lambda {:a :b :c} {:c :a :b}} Disk_5 
               {{lambda {:a :b :c} {:c :a :b}} Disk_6 
                {lambda {:a :b} :b}}}}}}} A B C} 
}

_p We can understand that all that stuff is nothing but a deep combination of text rewritings and, in order to be more convinced, you could carefully replace all {b lambdas} by the verb {b replace}, replace the set of balanced curly braces by the "{b by, in and}" conjuctions and {b do without any computer} but {b laboriously by yourself} the long sequence of moves.

;; _p Now I am sure that you can see lots of lambdas surfing on this breaking wave.

_img https://upload.wikimedia.org/wikipedia/commons/a/a5/Tsunami_by_hokusai_19th_century.jpg
 
}

{{block}
_h2 conclusion

_p Let us remember that {b LISP} is the descendant of a formal language, the {b λ-calculus}, created in the 1930s by Alonzo Church and built on three rules that can be expressed as follows:
{div {@ style="text-align:center; font:bold 2.0em papyrus"}
x := w | λw.x | xx
}
_p This cryptic expression has made generations of computer science students tremble. However, this language gave us the basis of the expression we used as a starting point in this document

{div {@ style="text-align:center; font:bold 1.5em papyrus"}
λw.x w  ->  '{{lambda {:words} expression} words} -> words
}

_p And more easily than following LISP, we have sketched three fundamentals concepts in coding, {b booleans, pairs & recursive data/control structures}. We have discovered that coding is nothing but a smart text rewriting process. It's understandable by anyone and this is a {b wondeful surprise}, at least for me.

_p More can be seen in [[coding]] and [[rewriting as coding|?view=oops]].

_p Please feel free to test any code in this page, just open the page editor (clicking "maxwell_equations" in the right part of the pages's title) and modify everything you want. And if the page locks, just refresh it.

_p {i Alain Marty |2021/12/06 | [[HN|https://news.ycombinator.com/item?id=43192243]]}
}

{{hide}
{def block 
  div {@ style="display:inline-block; width:700px; 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:5200px; 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; }
h3 { font-size:1.5em; }
p { font-size:1.2em; }
u { color:#ff0; text-decoration:none; }
}