Search code examples
clojurelambda-calculusturing-completey-combinator

Why does the y-combinator provide Turing equivalence?


This answer says

  1. Here is a basic y-combinator in lambda calculus:

    Y f = (\x -> f (x x)) (\x -> f (x x))

Ie Something like this in Clojure:

(defn Y [f]
  ((fn [x] (x x))
   (fn [x]
     (f (fn [& args]
          (apply (x x) args))))))

(def fac
     (fn [f]
       (fn [n]
         (if (zero? n) 1 (* n (f (dec n)))))))

(def fib
     (fn [f]
       (fn [n]
         (condp = n
           0 0
           1 1
           (+ (f (dec n))
              (f (dec (dec n))))))))
  1. Here is another expression of the y-Combinator (step 2 of the argument)

  2. We have encoded a Turing complete language (since we used the y-Combinator) (step 3 of the argument)

My question is: Why does the y-combinator provide Turing equivalence? It seems it was just an assumption of the argument.


Solution

  • Since having just λ already suffices for turing completeness, the Y Combinator is mere library code. It provides easy self-recursion.

    The question as I read it, asks whether one could take away turing completeness from λ calculus, by elminiating self-application, to which the question obviously is no, since there is no way to reliably detecting self-application, short of actually running the calculus (the halting problem).

    The argument just shows how to build Y without obvious self recursion and highlights the fact that Y is just the most condensed version of a whole family of patterns.

    The real answer to the subset of lambda calculus that's not turing-complete is: total functions.