I might need some help with the following question.

Given a Partial Combinatory Algebra, we can define the fixed point combinator $Y := [\lambda^{*}xy.y(xxy)][\lambda^{*}xy.y(xxy)]$. How does this relate to Kleenes recursion theorem, aka. fixed point theorem?

In the setting of Kleenes first PCA, ie. the PCA of computable functions on $\mathbb{N}$, given a (partial) computable function $f = \varphi_c$ the fixed point combinator satisfies $Yc = c(Yc)$. As I understand it this means that taking d := Yc it translates to $f(d) = \varphi_c(d) = cd = d$, ie. $f$ having a fixed point.

However Kleene's recursion theorem originally gives a weaker assertion, namely that for every total computable function $g$ there is some $n$ such that $\varphi_{g(n)} \simeq \varphi_n$ (cf. Odifreddi - Classical Recursion Theory, Theorem II.2.10).

This really confuses me and I couldn't make up my mind what to do about it. I hope someone can help me out. Anyway, thank you for your time.

  • $\begingroup$ How do you know $Y c$ is defined? $\endgroup$ Jul 15, 2019 at 19:25
  • $\begingroup$ Hello Andrej. First of all thank you for your answer and sorry for this rather late reply. It seems like I refreshed the page improperly and did not see your comment for a long time... You are right. It is certainly not clear why $Yc$ should exist. However I still do not see whether or how a relation to the recursion theorem exists. Just taking $Ycc' = c(Yc)c'$ doesn't seem to make your problem any better... $\endgroup$ Aug 27, 2019 at 15:14
  • $\begingroup$ It wasn't really a question, it was a hint that could lead you to the answer, namely that the mystery goes away if $Y c$ is undefined. Can you find a single value $c$ for which $Y c$ is defined? You need to pay attention to the special provisos of the $\lambda^*$ notation and when you are allowed to perform $\beta$-reductions. And instead of using the $=$ sign, you should carefully use Kleene's equality $a \simeq b$ which means "if one side is defined then so is the other and they're equal". $\endgroup$ Aug 27, 2019 at 15:27
  • $\begingroup$ Well, literally the same problem arises in the proof of the Recursion theorem in Odifreddi's Classical Recursion Theory, Theorem II.2.10. There he takes $b$ to be a code satisfying $\varphi_b(e) \simeq f\varphi_e(e)$. Letting $e=b$ he deduces $\varphi_{\varphi_b(b)} \simeq \varphi_{f\varphi_b(b)}$ without a comment on why $\varphi_b(b)$ should exist. However if the point is that $\varphi_b(b)$ does not have to exist, we have found a non-existing fixed point. Now I really am confused... $\endgroup$ Aug 27, 2019 at 16:25
  • $\begingroup$ I don't have the book here, but I assure you that you need to actually dig into details yourself and try to figure them out. Don't just despair about some author not having made this or that comment. From what little Google books tells me about Theorem II.2.10, I cannot tell what it actually says. You may wish to quote it in your question. $\endgroup$ Aug 27, 2019 at 17:05

1 Answer 1


As I understand it this means that taking $d := Yc$ it translates to $f(d)=φ_{c}(d)=cd=d$, ie. $f$ having a fixed point.

Not every recursive function has a fixed point in the sense of $f(n)=n$ - for example, $f(n)=n+1$. Therefore, there must be something wrong with this proof. As noted in comments, this proof works only if $d=Y c$ is defined.

As you've noticed, you can work around this issue by using a variant of the Y combinator:

Just taking Ycc′=c(Yc)c′ doesn't seem to make your problem any better

But it does! To avoid confusion, I'll call this combinator Z. We have


Let's take a function $f=\varphi_c$ and let $d = Z c$, just like in the previous proof. Now, $d$ is guaranteed to be defined. We have

$d c' \equiv c d c'$

By the definition of application in the Kleene's first algebra this means:

$\varphi_{d}(c')$ $ \simeq \varphi_{\varphi_{c}(d)}(c')$

$\varphi_{d}(c')$ $ \simeq \varphi_{f(d)}(c')$

$\varphi_{d}$ $ \simeq \varphi_{f(d)}$

which is the Kleene's recursion theorem.

Well, literally the same problem arises in the proof of the Recursion theorem in Odifreddi's Classical Recursion Theory, Theorem II.2.10. There he takes $b$ to be a code satisfying $\varphi_{b}(e) \simeq f(\varphi_e(e))$.

No, $b$ is defined in Theorem II.2.10 using the equation:

$\varphi_{\varphi_{b}(e)} \simeq \varphi_{f(\varphi_e(e))}$

Importantly, $b$ is a code - it is a well-defined natural number that encodes a specific program. Furthermore, for every $e$, $\varphi_b(e)$ is also a code - it is not the result of running $f(\varphi_e(e))$, it is merely a code of a function which given $n$, runs the function $\varphi_{f(\varphi_e(e))}$ on $n$. (This difference mirrors the difference between Y and Z combinators.)

  • $\begingroup$ Thank you very much for your comment and pointing out the $Z$ combinator! From lectures I believe to recall something like $\beta$-reductions within a lambda abstraction are bad and with this I can see, why $Zc$ is defined. However, I cannot find this rule on the internet nor in Barendtregt - Introduction to Lambda Calculus and I suppose it is false. But then, using the lambda term from Wikipedia I seem to be able to $\beta$-reduce $Zc$ indefinetely. Yet, this may only be the case, because I often miscalculate such things... $\endgroup$ Aug 29, 2019 at 15:38
  • $\begingroup$ Regarding Odifreddi I got confused over "Let $b$ be an index of the [...] function defined as". So please correct me if I got this wrong: we have (kind of by universality) a partial computable function $(e,x) \mapsto \varphi_{f\varphi_e(e)}(x)$, so by $Smn$ there is a code $b$ such that $\varphi_b(e)$ is a total computable function and $\varphi_{\varphi_b(e)} \simeq \varphi_{f\varphi_e(e)}$. Then by totality $\varphi_b(b)$ exists and we can deduce the recursion theorem... $\endgroup$ Aug 29, 2019 at 15:59
  • $\begingroup$ @PrudiiArca That rule is implemented in many programming languages (e.g. $K (\lambda z. Y I z) 0$ will evaluate to 0, even though you could beta-reduce $Y I$ indefinitely). Regarding Odifreddi: Yes, your interpretation is correct. $\endgroup$
    – sdcvvc
    Sep 1, 2019 at 16:01
  • $\begingroup$ thank you so much. You really helped alot! $\endgroup$ Sep 4, 2019 at 10:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.