[lisper]

Oh dear, I have failed. The whole point of that paper was supposed to be that all this theory stuff actually has practical applications. The same techniques that worked on that toy problem can be used on real problems and produce similar results.

I did some follow-up work after that paper to implement binary arithmetic in the lambda calculus, and using that, of course, you can compute "real" factorials. Here it is computing the factorial of 100 in under a second:

  ? (time (pbn (bn_fact (bn 100))))
  (PBN (BN_FACT (BN 100)))
  took 942,269 microseconds (0.942269 seconds) to run.
        64,791 microseconds (0.064791 seconds, 6.88%) of which was spent in GC.
  During that period, and with 4 available CPU cores,
       878,343 microseconds (0.878343 seconds) were spent in user mode
       111,475 microseconds (0.111475 seconds) were spent in system mode
   759,285,088 bytes of memory allocated.
   504 minor page faults, 0 major page faults, 0 swaps.
  93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000

This is he expanded code:

  ((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
   (λ f
    (λ n
       (λ nil
          (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) n)
            (λ dummy ((λ (l r s) (s l r)) (λ (_t e) _t) (λ s (λ (_t e) _t))))
            (λ dummy
               (((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
                 (λ f
                    (λ (n1 n2 r)
                       (λ nil
                          (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) n1) (λ dummy r)
                            (λ dummy
                               (f
                                ((λ (l)
                                    (λ nil
                                       (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                         (λ dummy (λ s (λ (_t e) _t))) (λ dummy ((λ p (p (λ (l r) r))) l)))
                                        (λ x x))))
                                 n1)
                                ((λ (l r s) (s l r)) (λ (_t e) e) n2)
                                (((λ (l)
                                     (λ nil
                                        (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                          (λ dummy (λ (_t e) e)) (λ dummy ((λ p (p (λ (l r) l))) l)))
                                         (λ x x))))
                                  n1)
                                 (((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
                                   (λ f
                                      (λ (n1 n2 c)
                                         (λ nil
                                            (((λ (c _t e) (c _t e))
                                              ((λ (p q) (p q (λ (_t e) e))) ((λ p (p (λ (l r) (λ (_t e) e)))) n1)
                                               ((λ p (p (λ (l r) (λ (_t e) e)))) n2))
                                              (λ dummy
                                                 (c ((λ (l r s) (s l r)) (λ (_t e) _t) (λ s (λ (_t e) _t)))
                                                  (λ s (λ (_t e) _t))))
                                              (λ dummy
                                                 ((λ (l r s) (s l r))
                                                  ((λ (b1 b2 c)
                                                      (b1 (b2 c ((λ c (c (λ (_t e) e) (λ (_t e) _t))) c))
                                                       (b2 ((λ c (c (λ (_t e) e) (λ (_t e) _t))) c) c)))
                                                   ((λ (l)
                                                       (λ nil
                                                          (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                                            (λ dummy (λ (_t e) e)) (λ dummy ((λ p (p (λ (l r) l))) l)))
                                                           (λ x x))))
                                                    n1)
                                                   ((λ (l)
                                                       (λ nil
                                                          (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                                            (λ dummy (λ (_t e) e)) (λ dummy ((λ p (p (λ (l r) l))) l)))
                                                           (λ x x))))
                                                    n2)
                                                   c)
                                                  (f
                                                   ((λ (l)
                                                       (λ nil
                                                          (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                                            (λ dummy (λ s (λ (_t e) _t)))
                                                            (λ dummy ((λ p (p (λ (l r) r))) l)))
                                                           (λ x x))))
                                                    n1)
                                                   ((λ (l)
                                                       (λ nil
                                                          (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                                            (λ dummy (λ s (λ (_t e) _t)))
                                                            (λ dummy ((λ p (p (λ (l r) r))) l)))
                                                           (λ x x))))
                                                    n2)
                                                   ((λ (b1 b2 c) (b1 (b2 (λ (_t e) _t) c) (b2 c (λ (_t e) e))))
                                                    ((λ (l)
                                                        (λ nil
                                                           (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                                             (λ dummy (λ (_t e) e))
                                                             (λ dummy ((λ p (p (λ (l r) l))) l)))
                                                            (λ x x))))
                                                     n1)
                                                    ((λ (l)
                                                        (λ nil
                                                           (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                                             (λ dummy (λ (_t e) e))
                                                             (λ dummy ((λ p (p (λ (l r) l))) l)))
                                                            (λ x x))))
                                                     n2)
                                                    c)))))
                                             (λ x x))))))
                                  n2 r (λ (_t e) e))
                                 r))))
                           (λ x x))))))
                n
                (f
                 (((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
                   (λ f
                      (λ n
                         (λ nil
                            (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) n) (λ dummy n)
                              (λ dummy
                                 (λ nil
                                    (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) l))) n)
                                      (λ dummy
                                         (((λ p (p (λ (l r) (λ (_t e) e)))) ((λ p (p (λ (l r) r))) n))
                                          (λ s (λ (_t e) _t))
                                          ((λ (l r s) (s l r)) (λ (_t e) e) ((λ p (p (λ (l r) r))) n))))
                                      (λ dummy ((λ (l r s) (s l r)) (λ (_t e) _t) (f ((λ p (p (λ (l r) r))) n)))))
                                     (λ x x)))))
                             (λ x x))))))
                  n))
                (λ s (λ (_t e) _t)))))
           (λ x x))))))"

I didn't write that all by hand, of course. I built it up in pieces and my "compiler" assembled it for me. But start to finish that took be about an hour.

[dewster]

If we were playing the Hot and Cold game you would be getting colder.

Are you telling me that the most efficient means of generating factorials is via LC? That no other method can touch it in terms of real time?

[lisper]

No, of course not. Factorial are just an illustrative example.

My goal was to dispel the myth that the lamdba calculus is nothing more than an intellectual curiosity. It is much, much more than that, not because you can use it to compute factorials, but because the techniques that you use to compute factorials in LC are generally applicable. If you really want to master the craft there are a few things you really need to know how to do: write your own compiler, your own editor, your own implementation of the Hindley-Milner type system. Writing an efficient factorial in LC is like that. It's not useful in and of itself, but for what you learn simply by going through the process.

[dewster]

Your initial words were "Here is how you can use the lambda calculus to compute factorials in non-geological time" which led me to believe you were claiming LC was a very (the most?) efficient route to factorial calculation. Which would make me sit up and take notice were that the case.

I'm sorry to say that your factorial example just seems painful and pointless to me, and doesn't encourage me to expand my mind via LC at all.

[posterboy]

> LC was a very (the most?) efficient route to factorial calculation

It is, because it is a standard model for computation. To put it in layman terms, every programming language is lambda calculus in disguise. You have absolutely no idea of computability theory. That is the theory in which the P=NP conjecture is formulated, which has massive implications e.g. on cryptography.

You seem frustrated for not understanding at all what's going on here and you try to provoke answers. I know what I'm talking about, because I don't grok LC either and I get furious quickly when I'm hungry, tired or overworked. You are paranoid.

[lisper]

:-(