lambdaway :: fac9

2 | list | login |load

| |

_h1 9! | [[lambdafact]]

_p In [[http://www.flownet.com/ron/lambda-calculus.html| http://www.flownet.com/ron/lambda-calculus.html]] Ron Garret explains in a {i very long and very geeky post} how {b 10!} can be computed in less than a second using this LISP code.

{pre
(λ ()
   ((λ (f s) (f (s (s (s (s (f (s (s (s (λ (f x) x)))))))))))
    (λ (n f) (n (λ (c i) (i (c (λ (f x) (i f (f x))))))
                (λ x f) (λ x x)))
    (λ (n f x) ((n f) (f x)))
    '1+ 0))
->  {* {S.serie 1 10}}
}

_p You know what? COMMON-LISP is not installed in my computer, it's a huge language, very hard to use, and I don't understand code if I can't code by myself, if I can't test it by myself. So, noting that {code 10! = {* {S.serie 1 10}}} is {code 9! = {* {S.serie 1 9}}} followed by a zero, I'm going to compute {code 9!} using '{lambda talk}, a language working in any web browser, free and easy to install.

_p Lest's first define a function, {code CHURCH}, to display Church numbers defined as

{center {code (n f x) ::= (f (f (f [n times] x)))}}

{script ;; 
  LAMBDATALK.DICT['1+'] = function() {
    var args = parseInt( arguments[0].trim() );
    return args+1  // or args+"."
  };
}

{pre
'{def CHURCH {lambda {:n} {:n 1+ 0}}}     // 1+ is a primitive n -> n+1            
-> {def CHURCH {lambda {:n} {:n 1+ 0}}}

'{CHURCH {lambda {:f :x} :x}}
-> {CHURCH {lambda {:f :x} :x}}
'{CHURCH {lambda {:f :x} {:f {:f {:f :x}}}}}
-> {CHURCH {lambda {:f :x} {:f {:f {:f :x}}}}} 
}

_p On the following set of basic functions (booleans & pairs)

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

_p we define two functions {code SUCC & MUL}

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

_p to build the factorial function

{pre
'{def FAC
 {lambda {:n}
  {RIGHT {{:n {lambda {:p} {PAIR {SUCC {LEFT :p}}
                                 {MUL {LEFT :p} {RIGHT :p}}}}}
                           {PAIR {SUCC FALSE}
                                 {SUCC FALSE}}}}}}
-> {def FAC
 {lambda {:n}
  {RIGHT {{:n {lambda {:p} {PAIR {SUCC {LEFT :p}}
                                 {MUL {LEFT :p} {RIGHT :p}}}}}
                           {PAIR {lambda {:f :x} {:f :x}}
                                 {lambda {:f :x} {:f :x}}}}}}}

'{CHURCH {FAC {lambda {:f :x}
             {:f {:f {:f {:f {:f {:f {:f {:f {:f :x}}}}}}}}}}}}
-> 362880     (ie. 9! computed in 7 000ms) ;; = {* {S.serie 1 9}}
}

_p This is the expanded version of {b '{FAC 9}}

{pre
'{CHURCH  
 {{lambda {:n}
  {{lambda {:c} {:c 
    {lambda {:a :b} :b}}} {{:n 
     {lambda {:p} 
     {{lambda {:a :b :c} {:c :a :b}}
      {{lambda {:n :f :x} {:f {:n :f :x}}}
       {{lambda {:c} {:c
         {lambda {:a :b} :a}}} :p}}
         {{lambda {:n :m :f :x} {:n {:m :f} :x}}
          {{lambda {:c} {:c
            {lambda {:a :b} :a}}} :p}
            {{lambda {:c} {:c
              {lambda {:a :b} :b}}} :p}}}}}
              {{lambda {:a :b :c} {:c :a :b}}
               {{lambda {:n :f :x} {:f {:n :f :x}}}
                 {lambda {:a :b} :b}}
                 {{lambda {:n :f :x} {:f {:n :f :x}}}
                   {lambda {:a :b} :b}}}}}} 
                   {{lambda {:f :x}
      {:f {:f {:f {:f {:f {:f {:f {:f {:f :x}}}}}}}}}}}}}
-> 362880  // computed in 13 000ms
}

;; _p 10! is computed in 109 000ms on my MacBookPro.

_p More {b and better} explanations in [[fromroots2canopy]] and [[coding]].