lambdaway :: pablo

3 | list | login |load

| |

_h1 a few steps in λ calculus

_p Following [[pablo rauzy| https://www.irif.fr/~carton/Enseignement/Complexite/ENS/Redaction/2009-2010/pablo.rauzy.pdf]]'s paper, the goal is to translate in {b live code} ({i ie. lambdatalk code active in this web page}) the sections from {{blue} 3.1.1 Condition et valeurs booléennes} to {{blue} 3.1.5 Compléments}. Detailed explanations can be seen in his paper.

_h2 1) booleans

{pre
{{blue}
– true := λab.a
– false := λab.b
– if := λcab.(c a b)
}

'{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 {:c :a :b}  {:c :a :b}}}
-> {def IF {lambda {:c :a :b}  {:c :a :b}}}

'{IF TRUE yes no}
-> {IF TRUE yes no}
'{IF FALSE yes no}
-> {IF FALSE yes no}

{{blue}
– and := λab.(if a b false)
– or := λab.(if a true b)
– not := λa.(if a false true)
}

'{def AND {lambda {:a :b} {IF :a :b FALSE}}}
-> {def AND {lambda {:a :b} {IF :a :b FALSE}}}
'{def OR {lambda {:a :b} {IF :a TRUE :b}}}
-> {def OR {lambda {:a :b} {IF :a TRUE :b}}}
'{def NOT {lambda {:a} {IF :a FALSE TRUE}}}
-> {def NOT {lambda {:a} {IF :a FALSE TRUE}}}

'{AND TRUE FALSE}
-> {AND TRUE FALSE}
'{AND TRUE TRUE}
-> {AND TRUE TRUE}
'{OR TRUE FALSE}
-> {OR TRUE FALSE}
'{OR FALSE FALSE}
-> {OR TRUE FALSE}
'{NOT TRUE}
-> {NOT TRUE}
'{NOT FALSE}
-> {NOT FALSE}
}

_h2 2) pairs and lists

{pre
{{blue}
– cons := λabc.(c a b)
– head := λp.(p (λab.a))
– tail := λp.(p (λab.b))
– nil := λa.true
– nilp := λp.(p (λab.false))
}

'{def CONS {lambda {:a :b :c} {:c :a :b}}}
-> {def CONS {lambda {:a :b :c} {:c :a :b}}}
'{def HEAD {lambda {:p} {:p {lambda {:a :b} :a}}}}
-> {def HEAD {lambda {:p} {:p {lambda {:a :b} :a}}}}
'{def TAIL {lambda {:p} {:p {lambda {:a :b} :b}}}}
-> {def TAIL {lambda {:p} {:p {lambda {:a :b} :b}}}}
'{def NIL {lambda {:a} TRUE}}
-> {def NIL {lambda {:a} TRUE}} 
'{def NILP {lambda {:p} {:p {lambda {:a :b} FALSE}}}}
-> {def NILP {lambda {:p} {:p {lambda {:a :b} FALSE}}}}

'{def P {CONS hello world}} 
-> {def P {CONS hello world}}
'{HEAD {P}}
-> {HEAD {P}}
'{TAIL {P}}
-> {TAIL {P}}

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

'{HEAD {L}} & '{NILP {L}}
-> {HEAD {L}} & {NILP {L}}
'{HEAD {TAIL {L}}} & '{NILP {TAIL {L}}}
-> {HEAD {TAIL {L}}} & {NILP {TAIL {L}}}
'{HEAD {TAIL {TAIL {L}}}} & '{NILP {TAIL {TAIL {L}}}}
-> {HEAD {TAIL {TAIL {L}}}} & {NILP {TAIL {TAIL {L}}}}
'{HEAD {TAIL {TAIL {TAIL {L}}}}} & '{NILP {TAIL {TAIL {TAIL {L}}}}}
-> {HEAD {TAIL {TAIL {TAIL {L}}}}} & {NILP {TAIL {TAIL {TAIL {L}}}}}
'{NILP {TAIL {TAIL {TAIL {TAIL {L}}}}}}
-> {NILP {TAIL {TAIL {TAIL {TAIL {L}}}}}}

'{def DISP
 {lambda {:l}
  {{{IF {NILP :l}
   {lambda {:l} }
   {lambda {:l} {HEAD :l} {DISP {TAIL :l}}}}} :l}}}
-> {def DISP
 {lambda {:l}
  {{{IF {NILP :l}
   {lambda {:l} }
   {lambda {:l} {HEAD :l} {DISP {TAIL :l}}}}} :l}}}

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

'{def LENGTH
 {lambda {:l}
  {{{IF {NILP :l}
   {lambda {:l} 0}
   {lambda {:l} {+ 1 {LENGTH {TAIL :l}}}}}} :l}}}
-> {def LENGTH
 {lambda {:l}
  {{{IF {NILP :l}
   {lambda {:l} 0}
   {lambda {:l} {+ 1 {LENGTH {TAIL :l}}}}}} :l}}}

'{LENGTH {L}}
-> {LENGTH {L}}

'{def REVERSE
 {def REVERSE.r
  {lambda {:a :b}
   {{{IF {NILP :a}
    {lambda {:a :b} :b}
    {lambda {:a :b} {REVERSE.r {TAIL :a} {CONS {HEAD :a} :b}}}}}
     :a :b}}}
 {lambda {:a} {REVERSE.r :a NIL}}}
-> {def REVERSE
 {def REVERSE.r
  {lambda {:a :b}
   {{{IF {NILP :a}
    {lambda {:a :b} :b}
    {lambda {:a :b} {REVERSE.r {TAIL :a} {CONS {HEAD :a} :b}}}}}
     :a :b}}}
 {lambda {:a} {REVERSE.r :a NIL}}}

'{DISP {REVERSE {L}}}
-> {DISP {REVERSE {L}}}

'{def APPEND                            
 {def APPEND.r
  {lambda {:a :b}
   {{{IF {NILP :b}
    {lambda {:a :b} :a}
    {lambda {:a :b} {APPEND.r {CONS {HEAD :b} :a}
                                    {TAIL :b}}}  }} :a :b}}}
 {lambda {:a :b} {APPEND.r {REVERSE :a} :b}}} 
-> {def APPEND                            
 {def APPEND.r
  {lambda {:a :b}
   {{{IF {NILP :b}
    {lambda {:a :b} :a}
    {lambda {:a :b} {APPEND.r {CONS {HEAD :b} :a}
                                    {TAIL :b}}}  }} :a :b}}}
 {lambda {:a :b} {APPEND.r {REVERSE :a} :b}}}

'{DISP {APPEND {L} {REVERSE {L}}}}
-> {DISP {APPEND {L} {REVERSE {L}}}}
}

_h2 3) numbers

{pre
{{blue}
Here Pablo Rauzy chooses to implement numbers as lists

– 0 := cons true true   // why not NIL
– succ := λn.(cons false n) 
– zerop := λn.(head n)
– pred := λn.(tail n)   // bug with SUB
}
   
'{def SUCC {lambda {:n} {CONS FALSE :n}}}
-> {def SUCC {lambda {:n} {CONS FALSE :n}}}
'{def PRED {lambda {:n} {IF {NILP :n} NIL {TAIL :n}}}}
-> {def PRED {lambda {:n} {IF {NILP :n} NIL {TAIL :n}}}}
'{def ZEROP {lambda {:n} {HEAD :n}}}
-> {def ZEROP {lambda {:n} {HEAD :n}}}

{{blue}
Note that the list's LENGTH function 
will be used to display numbers as usual
}

'{def ZERO NIL} = '{LENGTH {ZERO}}
-> {def ZERO NIL} = {LENGTH {ZERO}}
'{def ONE {SUCC {ZERO}}} = '{LENGTH {ONE}}
-> {def ONE {SUCC {ZERO}}} = {LENGTH {ONE}}
'{def TWO {SUCC {ONE}}} = '{LENGTH {TWO}}
-> {def TWO {SUCC {ONE}}} = {LENGTH {TWO}}
'{def THREE {SUCC {TWO}}} = '{LENGTH {THREE}}
-> {def THREE {SUCC {TWO}}} = {LENGTH {THREE}} 
'{def FOUR {SUCC {THREE}}} = '{LENGTH {FOUR}}
-> {def FOUR {SUCC {THREE}}} = {LENGTH {FOUR}} 
'{def FIVE {SUCC {FOUR}}} = '{LENGTH {FIVE}}
-> {def FIVE {SUCC {FOUR}}} = {LENGTH {FIVE}} 
'{def SIX {SUCC {FIVE}}} = '{LENGTH {SIX}}
-> {def SIX {SUCC {FIVE}}} = {LENGTH {SIX}}

{{blue}
add := λab.(if (zerop a) b (add (pred a) (succ b)))
add-rec := λf.(λab.(if (zerop a) b (f (pred a) (succ b))))
Y := λf.((λx.f(x x)) (λx.f(x x))) 
(Y add-rec) (succ 0) (succ 0) = succ (succ 0)

We follow another way, without any Y-combinator.
}

'{def ADD
 {lambda {:a :b}
  {{IF {ZEROP :b}
   {lambda {:a :b} :a}
   {lambda {:a :b} {ADD {SUCC :a} {PRED :b}}}} :a :b}}}
-> {def ADD
 {lambda {:a :b}
  {{IF {ZEROP :b}
   {lambda {:a :b} :a}
   {lambda {:a :b} {ADD {SUCC :a} {PRED :b}}}} :a :b}}}

'{LENGTH {ADD {SIX} {SIX}}} 
-> {LENGTH {ADD {SIX} {SIX}}}

'{def SUB
 {lambda {:a :b}
  {{IF {ZEROP :b}
   {lambda {:a :b} :a}
   {lambda {:a :b} {SUB {PRED :a} {PRED :b}}}} :a :b}}}
-> {def SUB
 {lambda {:a :b}
  {{IF {ZEROP {PRED :b}}
   {lambda {:a :b} {PRED :a}}
   {lambda {:a :b} {SUB {PRED :a} {PRED :b}}}} :a :b}}}

'{LENGTH {SUB {ONE} {TWO}}}
-> {LENGTH {SUB {ONE} {TWO}}} 
'{LENGTH {SUB {TWO} {TWO}}}
-> {LENGTH {SUB {TWO} {TWO}}}
'{LENGTH {SUB {THREE} {TWO}}}
-> {LENGTH {SUB {THREE} {TWO}}}

'{def MUL
 {def MUL.r
  {lambda {:a :b :c}
   {{IF {ZEROP :b}
    {lambda {:a :b :c} :c}
    {lambda {:a :b :c} {MUL.r :a {PRED :b} {ADD :c :a}}}} :a :b :c}}}
 {lambda {:a :b} {MUL.r :a :b {ZERO}}}}
-> {def MUL
 {def MUL.r
  {lambda {:a :b :c}
   {{IF {ZEROP :b}
    {lambda {:a :b :c} :c}
    {lambda {:a :b :c} {MUL.r :a {PRED :b} {ADD :c :a}}}} :a :b :c}}}
 {lambda {:a :b} {MUL.r :a :b {ZERO}}}}

'{LENGTH {MUL {SIX} {SIX}}} 
-> {LENGTH {MUL {SIX} {SIX}}}

'{def POW
 {def POW.r
  {lambda {:a :b :c}
   {{IF {ZEROP :b}
    {lambda {:a :b :c} :c}
    {lambda {:a :b :c} {POW.r :a {PRED :b} {MUL :c :a}}}} :a :b :c}}}
 {lambda {:a :b} {POW.r :a :b {ONE}}}}
-> {def POW
 {def POW.r
  {lambda {:a :b :c}
   {{IF {ZEROP :b}
    {lambda {:a :b :c} :c}
    {lambda {:a :b :c} {POW.r :a {PRED :b} {MUL :c :a}}}} :a :b :c}}}
 {lambda {:a :b} {POW.r :a :b {ONE}}}}

'{LENGTH {POW {TWO} {SIX}}}
-> {LENGTH {POW {TWO} {SIX}}}

'{def DIV                           
  {lambda {:a :b}
   {{IF {ZEROP {SUB :b :a}}
    {lambda {:a :b} {ADD {ONE} {DIV {SUB :a :b} :b}}}
    {lambda {:a :b} {ZERO}} } :a :b}}}
-> {def DIV                            
 {lambda {:a :b}
  {{IF {ZEROP {SUB :b :a}}
       {lambda {:a :b} {SUCC {DIV {SUB :a :b} :b}}}
       {lambda {:a :b} {ZERO}}}
                :a :b}}}

'{LENGTH {DIV {THREE} {TWO}}}
-> {LENGTH {DIV {THREE} {TWO}}}
'{LENGTH {DIV {FOUR} {TWO}}}
-> {LENGTH {DIV {FOUR} {TWO}}}

'{def MOD                            
 {lambda {:a :b}
  {SUB :a {MUL {DIV :a :b} :b}}}}
-> {def MOD                            
 {lambda {:a :b}
  {SUB :a {MUL {DIV :a :b} :b}}}}

'{LENGTH {MOD {THREE} {TWO}}}
-> {LENGTH {MOD {THREE} {TWO}}}
'{LENGTH {MOD {FOUR} {TWO}}}
-> {LENGTH {MOD {FOUR} {TWO}}}

'{def GCD
 {lambda {:a :b}
  {{IF {ZEROP {SUB :b :a}}
   {lambda {:a :b} :b}
   {lambda {:a :b} {GCD :b {MOD :a :b}}}} :a :b}}}
-> {def GCD
 {lambda {:a :b}
  {{IF {ZEROP :b}
   {lambda {:a :b} :a}
   {lambda {:a :b} {GCD :b {MOD :a :b}}}} :a :b}}}

{def gcd
 {lambda {:a :b}
  {if {= :b 0}
   then :a
   else {gcd :b {% :a :b}}}}}

'{LENGTH {GCD {MUL {TWO} {THREE}} {TWO}}}  
-> {LENGTH {GCD {MUL {TWO} {THREE}} {TWO}}}

'{LENGTH {GCD {THREE} {TWO}}} 
-> ???

'{def FAC
 {lambda {:n}
  {{IF {ZEROP :n} 
   {lambda {:n} {ONE}}
   {lambda {:n} {MUL :n {FAC {PRED :n}}}}} :n}}}
-> {def FAC
 {lambda {:n}
  {{IF {ZEROP :n} 
   {lambda {:n} {ONE}}
   {lambda {:n} {MUL :n {FAC {PRED :n}}}}} :n}}}

'{LENGTH {FAC {FIVE}}}  
-> 120        // '{LENGTH {FAC {SIX}}} locks on my iPad

}

_h2 4) map, reduce & filter

{pre
{{blue}
map := Y (λm.(λfl. (if (nilp l)
    nil
    (cons (f (head l)) (m f (tail l))))))

reduce := Y (λr.(λfxl. (if (nilp l)
    x
    (r f (f x (head l)) (tail l)))))

filter := Y (λf.(λpl. (if (nilp l)
    nil
    (if (p (head l))
      (cons (head l) (f p (tail l)))
      (f p (tail l))))))
}

'{def MAP
 {lambda {:f :l}
  {{{IF {NILP :l} 
   {lambda {:f :l} }
   {lambda {:f :l} {:f {HEAD :l}} 
                       {MAP :f {TAIL :l}}}}} :f :l}}}
-> {def MAP
 {lambda {:f :l}
  {{{IF {NILP :l} 
   {lambda {:f :l} }
   {lambda {:f :l} {:f {HEAD :l}} {MAP :f {TAIL :l}}}}} :f :l}}}

'{def REDUCE
 {def REDUCE.r
  {lambda {:f :a :b}
   {{{IF {NILP :a}
     {lambda {:f :a :b} :b}
     {lambda {:f :a :b} {:f {HEAD :a}
                            {REDUCE.r :f {TAIL :a} :b}}}}} :f :a :b}}}
 {lambda {:f :a}
  {REDUCE.r :f :a {HEAD :a}}}}
-> {def REDUCE
 {def REDUCE.r
  {lambda {:f :a :b}
   {{{IF {NILP :a}
     {lambda {:f :a :b} :b}
     {lambda {:f :a :b} {:f {HEAD :a} {REDUCE.r :f {TAIL :a} :b}}}}} :f :a :b}}}
 {lambda {:f :a}
  {REDUCE.r :f :a {HEAD :a}}}}

'{def NUMBERS {CONS {ONE}
             {CONS {TWO}
             {CONS {THREE}
             {CONS {FOUR}
             {CONS {FIVE}
                    NIL}}}}}}
-> {def NUMBERS {CONS {ONE}
            {CONS {TWO}
            {CONS {THREE}
            {CONS {FOUR}
            {CONS {FIVE}
                  NIL}}}}}}

'{MAP {lambda {:n} {LENGTH {FAC :n}}} {NUMBERS}}
-> {MAP {lambda {:n} {LENGTH {FAC :n}}} {NUMBERS}}

'{LENGTH {REDUCE MUL {NUMBERS}}}
-> {LENGTH {REDUCE MUL {NUMBERS}}}

FILTER ... wait & see.
}

_p It can be noted that the approach detailed in [[fromroots2canopy]] seems to be more efficient. I don't know why.

_h2 5) hilbert curve

_p Explanations in [[hilbert]]. We just forget numbers, replaced by a list.

{prewrap
'{def LEFT
 {lambda {:d :l}
  {{{IF {NILP :l}
   {lambda {:d :l} }
   {lambda {:d :l}
    T90      {RIGHT :d {TAIL :l}}
    M:d T-90 {LEFT  :d {TAIL :l}}
    M:d      {LEFT  :d {TAIL :l}}
    T-90 M:d {RIGHT :d {TAIL :l}}
    T90
}}} :d :l}}}
-> {def LEFT
 {lambda {:d :l}
  {{{IF {NILP :l}
   {lambda {:d :l} }
   {lambda {:d :l}
    T90      {RIGHT :d {TAIL :l}}
    M:d T-90 {LEFT  :d {TAIL :l}}
    M:d      {LEFT  :d {TAIL :l}}
    T-90 M:d {RIGHT :d {TAIL :l}}
    T90
}}} :d :l}}}

'{def RIGHT
 {lambda {:d :l}
  {{{IF {NILP :l}
   {lambda {:d :l} }
   {lambda {:d :l}
     T-90    {LEFT  :d {TAIL :l}}
     M:d T90 {RIGHT :d {TAIL :l}}
     M:d     {RIGHT :d {TAIL :l}}
     T90 M:d {LEFT  :d {TAIL :l}}
     T-90
}}} :d :l}}}
-> {def RIGHT
 {lambda {:d :l}
  {{{IF {NILP :l}
   {lambda {:d :l} }
   {lambda {:d :l}
     T-90    {LEFT  :d {TAIL :l}}
     M:d T90 {RIGHT :d {TAIL :l}}
     M:d     {RIGHT :d {TAIL :l}}
     T90 M:d {LEFT  :d {TAIL :l}}
     T-90
}}} :d :l}}}

'{LEFT 25 {L}}
-> {b 595} words beginning with "T90 T-90 T90 T-90  M25 T90  M25  T90 M25  T-90 M25 T-90 T90  M25 T-90  M25  T-90 M25 ..."
}

_p which sen to a SVG graphic device outputs the following Hilbert curve at level 4:

{center
{svg {@ width="395px" height="395px" style="background:#eee;"}
 {path 
 {@ id="spline"
     d="M {turtle 10 10 0 {LEFT 25 {L}}}"  
      fill="transparent" stroke="#000" stroke-width="1"
 }}
 {circle 
  {@ cx="0" cy="0" r="5" fill="#0ff" stroke="#f00"}
  {animateMotion 
   {@ dur="100s" repeatCount="indefinite" rotate="auto"}
   {mpath {@ xlink:href="#spline"}}
 }}  
}}

_p thanks to this code:

{pre
'{svg {@ width="395px" height="395px" style="background:#eee;"}
 {path 
 {@ id="spline"
     d="M {turtle 10 10 0 {LEFT 25 {L}}}"  
      fill="transparent" stroke="#000" stroke-width="1"}}
 {circle 
  {@ cx="0" cy="0" r="5" fill="#0ff" stroke="#f00"}
  {animateMotion 
   {@ dur="100s" repeatCount="indefinite" rotate="auto"}
   {mpath {@ xlink:href="#spline"}}}}  
}}

_p {i Alain Marty 2020/03/28 | updated 2023/03/22}

{{hide}
{def blue span {@ style="color:blue"}}}