lambdaway :: ifac

2 | list | login |load

| |

_h1 IFAC & RFAC

_p Two special forms, lambda & def, an empty dictionary and the shortest way to build a factorial, the first one iterative, the second recursive.

{prewrap
1. booleans

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

2. pairs

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

3. Church numbers: 0, succ(0), succ(succ(0)), ...

'{def SUCC {lambda {:n :f :x} {:f {:n :f :x}}}}
-> {def SUCC {lambda {:n :f :x} {:f {:n :f :x}}}}

'{def ZERO FALSE}
-> {def ZERO FALSE}
'{def ONE {SUCC FALSE}}
-> {def ONE {SUCC FALSE}}
...
'{def N {SUCC {SUCC {SUCC {SUCC {SUCC {SUCC FALSE}}}}}}}
-> {def N {SUCC {SUCC {SUCC {SUCC {SUCC {SUCC FALSE}}}}}}}

'{def CHURCH {lambda {:n} {:n {lambda {:x} .:x} _}}}
-> {def CHURCH {lambda {:n} {:n {lambda {:x} .:x} _}}}  // displays church numbers as dots ending with _

'{CHURCH {ZERO}}
-> {CHURCH {ZERO}}
'{CHURCH {ONE}}
-> {CHURCH {ONE}}
...
'{CHURCH {N}}
-> {CHURCH {N}}

'{def PRED
 {lambda {:n} 
  {HEAD                     // take the first of
   {{:n {lambda {:i}             // apply n times the function
                {CONS                      // building the pair
                 {TAIL :i}                 // with the second
                 {SUCC {TAIL :i}}}}}       // and its successor
        {CONS FALSE FALSE}}}}}   // .. to (0,0)
-> {def PRED
 {lambda {:n} 
  {HEAD {{:n {lambda {:p} {CONS {TAIL :p} {SUCC {TAIL :p}}}}} 
             {CONS FALSE FALSE}}}}}

'{def ZERO? {lambda {:n} {:n {lambda {:x} FALSE} TRUE}}}
-> {def ZERO? {lambda {:n} {:n {lambda {:x} FALSE} TRUE}}}

'{ZERO? {ZERO}}
-> {ZERO? {ZERO}}
'{ZERO? {ONE}}
-> {ZERO? {ONE}}

4. operators
°°°
'{def SUB {lambda {:m :n} {{:n PRED} :m}}} 
-> {def SUB {lambda {:m :n} {{:n PRED} :m}}}

'{def EQUAL?
 {lambda {:a :b}
  {ZERO? {SUB :a :b}}}}
-> {def EQUAL?
 {lambda {:a :b}
  {ZERO? {SUB :a :b}}}}

{EQUAL? {ONE} {ZERO}}
°°°
'{def MUL {lambda {:n :m :f :x} {:n {:m :f} :x}}}
-> {def MUL {lambda {:n :m :f :x} {:n {:m :f} :x}}}

'{def IFAC        // iterative version
 {lambda {:n}
  {TAIL                      // take the second of
   {{:n {lambda {:i}              // apply n times the function
                {CONS                      // building the pair
                 {SUCC {HEAD :i}}     // with succ of first and 
                 {MUL {HEAD :i} {TAIL :i}}}}}   // first*second
        {CONS {ONE} {ONE}}}}}}    // .. to (1,1)
-> {def IFAC
 {lambda {:n}
  {TAIL {{:n {lambda {:p}
   {CONS {SUCC {HEAD :p}} {MUL {HEAD :p} {TAIL :p}}}}}
   {CONS {ONE} {ONE}}}}}}

'{def RFAC        // recursive version
 {lambda {:n}
  {{IF {ZERO? :n}
   {lambda {:n} {ONE}} 
   {lambda {:n} {MUL :n {RFAC {PRED :n}}}}} :n}}}
-> {def RFAC
 {lambda {:n}
  {{IF {ZERO? :n}
   {lambda {:n} {ONE}} 
   {lambda {:n} {MUL :n {RFAC {PRED :n}}}}} :n}}}

'{CHURCH {IFAC {N}}}  
-> {CHURCH {IFAC {N}}}  // read 720 dots

'{CHURCH {RFAC {N}}}
-> {CHURCH {RFAC {N}}}

}

°°°
_h2 parigot encoding

{pre

suc=λ n.λ f.λ a.fn(nfa) 
{def succ
 {lambda {:n :f :a} {:f {:n {:n :f :a}}}}}

add=λ n.λ m.n(λ p.suc)m 
mult=λ n.λ m.n(λ p.addm)0 
pred=λ n.n(λ p.λ d.p)0

}
°°°

_h2 refs

_ul [[lambda encoding reborn| https://homepage.divms.uiowa.edu/~astump/talks/colloq-10-24-2014.pdf]]
_ul [[programming with nothing| https://news.ycombinator.com/item?id=3343205]]