Is there an abstract proof of Kleene's Recursion Theorem in a typed lambda-calculus?

Question

I have written out a proof using lambda-functions that formalizes the exposition of Kleene's Recursion Theorem statement and proof in Michael Sipser's book "Introduction to the Theory of Computation." But my setup is rather naive, so I wonder whether there is a published rigorous proof in a typed lambda-calculus (in the sense of the Lambek-Scott book on categorical logic). If so, there would be a statement and proof of Kleene's Recursion Theorem in the corresponding cartesian closed category.

Answer 1

In my paper On fixed-point theorems in synthetic computability I prove the recursion theorem using higher-order intuitionistic logic a la Lambek & Scott in the following form (Theorem 5.2 in the paper):

Theorem: If there is a surjection $e : \mathbb{N} \to A^\mathbb{N}$ then every multivalued map $f : A \rightrightarrows A$ has a fixed point. $\newcommand{\NN}{\mathbb{N}}$

Proof. Recall that a multivalued map $f : A \rightrightarrows A$ is a map $f : A \to P_*(A)$ from $A$ to the set of inhabited subsets of $A$. For every $n \in \NN$ there is $x \in f(e(n)(n))$, hence by the Axiom of Countable Choice there is a map $g : \NN \to A$ such that $g(n) \in f(e(n)(n))$ for all $n \in \NN$. There is $k \in \NN$ such that $e(k) = g$, and so $e(k)(k) = g(k) \in f(e(k)(k))$. $\Box$

Note tha the proof uses the Axiom of Countable Choice, which is valid in realizability toposes, and in particular in the effective topos. Also, the above proof is really using $\lambda$-calculus, but not its notation.

The usual Kleene's Recursion Theorem is a consequence of the synthetic one, at least in the effective topos, see Corollary 5.3 in the paper.

Answer 2

Assume there are types $\mathbb{C}^{(1)},D^{(1)}, \mathbb{C}^{(2)},D^{(2)},S$ and $\lambda$ functions $D:\mathbb{C}^{(n)}\rightarrow D^{(n)}\hookrightarrow S, E:D^{(n)}\rightarrow \mathbb{C}^{(n)}$ such that $D\circ E =1$ and $E\circ D=1$. Define $K: S\rightarrow \mathbb{C}^{(1)}$ by $K\sigma=\lambda \tau\in S.\sigma$. Theorem. For every $T\in \mathbb{C}^{(2)}$ there exists $R\in\mathbb{C}^{(1)}$ such that $R\sigma=T(DR,\sigma)$. Proof. Define $1_S=\lambda \sigma\in S.\sigma$, and define $B=\lambda DM\in D^{(2)}.D(EDM\circ(KDM,1_S))$, where $(KDM,1_S):S\rightarrow \mathbb{C}^{(1)}\times\mathbb{C}^{(1)}$. For any $T\in \mathbb{C}^{(2)}$, define $A=KD(T\circ(B,1_S))\in\mathbb{C}^{(1)}$. Also, define $R=T\circ ((B\circ A),1_S)$. Calculate $(B\circ A)\sigma = B(A\sigma)=BD(T\circ (B,1_S))=D(T\circ (B,1_S)\circ(A,1_S))=D(T\circ(B\circ A),1_S)=DR$. Therefore, $R\sigma=(T\circ (B\circ A,1_S))\sigma=T((B\circ A,1_S)\sigma)=T((B\circ A)\sigma,\sigma)=T(DR,\sigma)$. My original question is whether this is sufficiently abstract to be formalized in a legitimate typed $\lambda-$calculus. I understand there is no idea here about natural numbers ($S$ is just "description strings"). there are no Turing machines here ($\mathbb{C}^{(n)}$ are just types that represent the sets of partial recursive functions with $n$ inputs, $n=1,2$) and I am being very vague about things like arrows and composition.

Answer 3

Kleene's recursion theorem follows from the call-by-value version of $Y$ combinator (let's call it $Z$), which is a special case of Lawvere's fixed point theorem. The proof can be found in this post: call-by-value version of $Y$ combinator

$$Z := \lambda y.(\lambda x.y(\lambda v.xxv))(\lambda x.y(\lambda v.xxv))$$

$$Zhv=h(Zh)v$$

$$e := Zh\implies ev=hev$$

which is the Kleene's recursion theorem.