El segundo teorema de recursión de Kleene es un resultado fundamental en la teoría de la computabilidad que permite la construcción de programas autorreferenciales. En su forma clásica, el teorema establece que para cualquier función recursiva parcial $\psi$, existe un índice $e$ tal que la función $\varphi_e$ se comporta como $\psi(e, \bar{x})$. Un Quine es una consecuencia específica de este teorema: al establecer $\psi$ como la función identidad, se puede encontrar un índice $e$ que representa un programa que, al ejecutarse, produce su propio código fuente. Aunque a menudo se discute en términos abstractos, la formalización de esta construcción proporciona un camino más claro para comprender cómo la autorreferencia está estructuralmente respaldada por la lógica subyacente de la computación.
Esta imagen ilustra la propiedad matemática central del segundo teorema de recursión de Kleene, donde se encuentra un índice de función $e$ tal que $\varphi_e$ se comporta como la propiedad deseada.
Esta notación específica apoya directamente la explicación del artículo sobre cómo un Quine es una consecuencia del teorema al encontrar un punto fijo.
Para pasar de la teoría abstracta a una implementación concreta, se puede adoptar una perspectiva de programación funcional. En este modelo, se asume que un lenguaje $L$ tiene un tipo $\mathsf{AST}$ para los árboles sintácticos y un cuasicotador $\mathsf{q}$ que puede realizar cotizaciones internamente. Bajo estas suposiciones, el teorema puede enunciarse como: para cualquier tipo $T$ y cualquier propiedad $P : \mathsf{AST} \rightarrow T$, existe un término $t : T$ tal que $P \lceil t \rceil = t$. La demostración implica construir un término $d$ que captura la propiedad $P$ y luego encontrar un punto fijo $t := d \lceil d \rceil$. Este enfoque demuestra que el teorema no trata solo sobre Quines, sino sobre encontrar puntos fijos para cualquier propiedad sintáctica, como un programa que produce su propio tamaño o su propio código fuente formateado.
Implementar esto en el cálculo lambda no tipado requiere representar la sintaxis propia del lenguaje utilizando codificaciones de Church. Debido a que el cálculo lambda no tipado es lo suficientemente expresivo para manejar datos de tipo árbol, se puede definir una representación AST donde las variables, las aplicaciones y las abstracciones lambda se codifican como abstracciones lambda en sí mismas. El componente más complejo es el cuasicotador, que debe definirse como un plegado (fold) sobre la estructura de árbol del AST. Al traducir estas ecuaciones a codificaciones de Church, se puede construir un Quine en notación de de Bruijn. Esta formalización resalta una compensación significativa: si bien el cálculo lambda no tipado simplifica la demostración al eliminar las restricciones de tipo, requiere una construcción manual y rigurosa del AST y de los mecanismos de cotización para lograr el mismo resultado que los lenguajes funcionales de alto nivel.