Kleene formalise la construction d'un quine via le théorème de récursion

Contexte théorique

Le théorème de récursion de Kleene (deuxième version) affirme que pour toute fonction partielle récursive ψ à n+1 arguments, il existe un indice e tel que ψ(e, x̄) ≃ φ_e(x̄). En choisissant ψ comme identité, on obtient e = φ_e(), c’est‑à‑dire un programme qui, sans entrée, renvoie son propre code. Cette propriété sous‑jacent constitue la base formelle des quines.

Construction fonctionnelle

Dans un langage fonctionnel L disposant d’un type AST représentant les arbres syntaxiques, on définit deux opérateurs : la citation ⟦t⟧ : AST et le quasi‑quotateur q : AST → AST tel que q ⟦t⟧ = ⟦⟦t⟧⟧. En posant d = λe. P(e·q e) où P : AST → T est une fonction arbitraire, le terme t = d ⟦d⟧ satisfait P ⟦t⟧ = t. La dérivation s’écrit :

t = d ⟦d⟧
  = (λe. P(e·q e)) ⟦d⟧
  = P(⟦d⟧·q ⟦d⟧)
  = P(⟦d⟧·⟦⟦d⟧⟧)
  = P ⟦d ⟦d⟧⟧
  = P ⟦t⟧

Lorsque P est l’identité, t est exactement un quine : il produit son propre code source.

Analyse des implications

Le cadre ci‑dessus montre que le théorème ne dépend pas de la puissance de calcul du langage, mais uniquement de la capacité à manipuler son propre code sous forme de données. Ainsi, même des langages non Turing‑complets peuvent générer des fixpoints syntaxiques, à condition de fournir AST, la citation et q. Cette observation relie le théorème à la lemme diagonal de Gödel : en prenant T = Prop et P = Prov, on obtient une formule qui affirme sa propre provabilité.

Limites et perspectives

La construction repose sur l’existence d’un opérateur q capable de doubler les citations. Dans les langages où la métaprogrammation est restreinte, implémenter q peut nécessiter des extensions non triviales. De plus, le modèle lambda non typé utilisé ici ignore les contraintes de typage qui, dans les systèmes fortement typés, imposent des vérifications supplémentaires pour garantir que d ⟦d⟧ reste bien typé. Explorer ces contraintes dans des langages à typage statique constitue une direction de recherche ouverte.