lambdaway :: hanoi4

5 | list | login |load

| |

_img https://upload.wikimedia.org/wikipedia/commons/thumb/e/e8/AnimeHanoiNB.gif/440px-AnimeHanoiNB.gif
 
_h1 [[hanoi]] | ... | hanoi4

_p The goal is to move n disks from A to B, one at a time and never a bigger disk upon a smaller one.

_h2 1) algorithm

_p The key idea is to suppose that the problem is solved for the upper disks:

{pre {@ style="margin-left:30px;"}
.    A            B            C

■|■           |            |     1) move the upper disks ...
   ■■|■■          |            |     ... from A to C
  ■■■|■■■         |            |
 ■■■■|■■■■        |            |
_____|____________|____________|_____

|            |           ■|■     2) move the lower disk ...
     |            |          ■■|■■    ... from A to B
     |            |         ■■■|■■■
 ■■■■|■■■■        |            |
_____|____________|____________|_____

|            |           ■|■     3) move the upper disks ...
     |            |          ■■|■■    ... from C to B
     |            |         ■■■|■■■
     |        ■■■■|■■■■        |
_____|____________|____________|_____

|           ■|■           |      4) done!
     |          ■■|■■          |
     |         ■■■|■■■         |
     |        ■■■■|■■■■        |
_____|____________|____________|_____
}

_p Now we can apply {b recursively} this process to the upper disks and just stop when there is no more disk. Here is the {b pseudo code}:

{pre
move disks from A to B via C
  if no disk
  then stop
  else move upperdisks from A to C
       move lowerdisk  from A to B
       move upperdisks from C to B
}

_h2 1) lambda{sup talk} code

_p Lambda{sup talk} comes with a {b if then else} special form and a {b pair} structure

{pre
'{P.lib}
-> {P.lib}
}

_p allowing to write the following simple double recursive function

{pre
'{def hanoi
 {lambda {:a :b :c :list :a :b :c}
  {if {not {P.pair? :list}}
   then     // nothing
   else {hanoi {P.right :list} :a :c :b}
        {div}move {P.left :list}
             from :a 
               to :b
        {hanoi {P.right :list} :a :c :b}
}}}  
-> {def hanoi
 {lambda {:list :a :b :c}
  {if {not {P.pair? :list}}
   then 
   else {hanoi {P.right :list} :a :c :b}
        {div}move {P.left :list} from :a to :b
        {hanoi {P.right :list} :a :c :b}
}}}
}

_p Let's test with 4 discs

{pre
'{def discs 
 {P.new ■■■■.■■■■
  {P.new ■■■.■■■ 
   {P.new ■■.■■ 
    {P.new ■.■
            \}}}}}  // "\" is just a word, not a pair
-> {def discs 
 {P.new ■■■■.■■■■
  {P.new ■■■.■■■ 
   {P.new ■■.■■ 
    {P.new ■.■ \}}}}}

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

_p Note that we don't use numbers. Just words.

_h2 2) lambda{sup calc} code

_p We want to stay at the lambda{sup calc} level, i.e. a lambda{sup talk} reduced to {b lambdas & defs and an empty dictionary}. The {b '{if then else}} special form doesn't exist.  
_p Here are the basic functions building the missing booleans and pairs. See [[the code factory|?view=concepts]] for detailed explanations.

{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}}}
'{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 NIL {lambda {} TRUE}}                 -> {def NIL {lambda {} TRUE}}
'{def !NIL {lambda {} FALSE}}               -> {def !NIL {lambda {} FALSE}}
'{def NIL? {lambda {:c} {:c !NIL}}}         -> {def NIL? {lambda {:c} {:c !NIL}}} 
}

_p Using these building bricks here is, without explanation for the moment, the translation of the pseudo-code into lambda{sup calc}

{pre
'{def HANOI
 {lambda {:list :a :b :c}
  {{IF {NIL? :list}
    {lambda {:list :a :b :c} 
       // nothing
    } 
    {lambda {:list :a :b :c}
       {HANOI {RIGHT :list} :a :c :b}
       {div}move {LEFT :list} 
            from :a 
              to :b 
       {HANOI {RIGHT :list} :c :b :a} 
    }
   } :list :a :b :c
  }
 }
}
-> {def HANOI
 {lambda {:list :a :b :c}
  {{IF {NIL? :list}
   {lambda {:list :a :b :c} } 
   {lambda {:list :a :b :c} {HANOI {RIGHT :list} :a :c :b}
                            {div}move {LEFT :list} 
                                 from :a 
                                   to :b 
                            {HANOI {RIGHT :list} :c :b :a} }}
            :list :a :b :c}
}} 
}

_p and here is the result of the {b HANOI} function applied on 4 disks:

{pre
'{def DISCS
 {PAIR ■■■■.■■■■ 
  {PAIR ■■■.■■■ 
   {PAIR ■■.■■ 
    {PAIR ■.■ 
          NIL}}}}}
-> {def DISCS
 {PAIR ■■■■.■■■■ 
  {PAIR ■■■.■■■ 
   {PAIR ■■.■■ 
    {PAIR ■.■ NIL}}}}}
 
'{HANOI {DISCS} A B C}    
-> {HANOI {DISCS} A B C} 
}

_p Note that only for a better display we allow us to use the {b div} HTML tag.

_h2 some explanations now

_p First, defining two "helper" functions {b THEN} and {b ELSE}

{pre
'{def THEN
 {lambda {:list :a :b :c} 
         // nothing
 }
}
-> {def THEN
 {lambda {:list :a :b :c} 
}}

'{def ELSE
 {lambda {:list :a :b :c}
         {HANOI {RIGHT :list} :a :c :b}
         {div}move {LEFT :list} 
              from :a 
                to :b 
         {HANOI {RIGHT :list} :c :b :a}
 }
}
-> {def ELSE
 {lambda {:list :a :b :c}
         {HANOI {RIGHT :list} :a :c :b}
         {div}move {LEFT :list} from :a to :b 
         {HANOI {RIGHT :list} :c :b :a}
}}
}

_p we rewrite the {b HANOI} function in a more readable form

{pre
'{def HANOI
 {lambda {:list :a :b :c}
         {{IF {NIL? :list} THEN ELSE} :list :a :b :c}
 }
}
-> {def HANOI
 {lambda {:list :a :b :c}
         {{IF {NIL? :list} THEN ELSE} :list :a :b :c}
}}
}

_p Then we follow the evaluation of the {b HANOI} function's body

{pre 
'{{IF {NIL? :list} THEN ELSE} :list :a :b :c}
}

_p According to the evaluation of {code '{NIL? :list}} to {code TRUE} or {code FALSE} this expression will be either {code '{THEN :list :a :b :c}} or {code '{ELSE :list a :b :c}}. More precisely:

_ul 1) in the first case

{pre 
'{THEN :list :a :b :c}
-> '{{lambda {:list :a :b :c}   // it's an IIFE
         // nothing
    } :list :a :b :c}
-> nothing ... & exit function
}

_ul 2) in the second case

{pre 
'{ELSE :list :a :b :c}
-> '{{lambda {:list :a :b :c}   // it's an IIFE
         {HANOI {RIGHT :list} :a :c :b}
         {div}move {LEFT :list} 
              from :a 
                to :b 
         {HANOI {RIGHT :list} :c :b :a}
    } :list :a :b :c}
-> '{HANOI {RIGHT :list} :a :c :b}
   '{div}move '{LEFT :list} 
        from :a 
          to :b 
   '{HANOI {RIGHT :list} :c :b :a}
}

_p which is the lambda{sup calc} translation of the initial pseudocode:

{pre
1) move upperdisks from A to C (via B)
2) move lowerdisk from A to B
3) move upperdisks from C to B (via A)
}

_p Quod erat demonstrandum!

_h2 3) down to lambdas

_p Without further explanationm, (see [[the code factory|?view=coding]]), you should know that there is an extremely simple function, called the {b Ω-combinator}

{pre
'{def Ω {lambda {:g} {:g :g}}}
-> {def Ω {lambda {:g} {:g :g}}}
}

_p thanks to which we can replace in

{pre
'{HANOI {DISCS} A B C}
}

_p all names by their lambda definitions. We end up with this cascade of lambdas

{pre
'{{{lambda {:g} {:g :g}} 
   {lambda {:g :n :a :b :c}
  {{{lambda {:a :b :c} {:a :b :c}}
    {{lambda {:c} {:c 
      {lambda {:a :b} 
       {lambda {:a :b} :b}}}} :n}
        {lambda {:g :n :a :b :c} }
         {lambda {:g :n :a :b :c} {:g :g 
         {{lambda {:c} {:c 
           {lambda {:a :b} :b}}} :n} :a :b :c} {br} move 
           {{lambda {:c} {:c 
             {lambda {:a :b} :a}}} :n} from :a to :b {:g :g
             {{lambda {:c} {:c 
               {lambda {:a :b} :b}}} :n} :c :b :a} }} :g :n :a :b :c}}}
               {{lambda {:a :b :c} {:c :a :b}} ■■■■.■■■■
               {{lambda {:a :b :c} {:c :a :b}}  ■■■.■■■
               {{lambda {:a :b :c} {:c :a :b}}   ■■.■■
               {{lambda {:a :b :c} {:c :a :b}}    ■.■   
                 {lambda {:a}
                  {lambda {:a :b} :a}}}}}} A B C}  
}

_p producing of course the same result and showing that all this is only a deep composition of text replacements. Where the border between data and code becomes difficult to find, some have given it a name: {b homoiconicity}. Nothing else than the systematic application of "{b IIFE}s".

_p {i alain marty | 2023/03/04-13}