Ein Quine aus Kleenes zweitem Rekursionstheorem, in Rocq formalisiert
Constructing a Quine from Kleene's Second Recursion Theorem
Dass Quines aus Kleenes zweitem Rekursionstheorem folgen, ist bekannt – aber wie leicht lässt sich die Konstruktion tatsächlich umsetzen? Der Autor skizziert einen Beweis im untyped Lambda Calculus, von der klassischen Berechenbarkeitstheorie über eine funktionale Sichtweise bis zum Diagonallemma. Mit Church-Encodings für den AST und einem Quasi-Quoter entsteht ein Quine, der in Rocq formalisiert und in de Bruijn-Notation angegeben wird.
Weit davon entfernt, eine mechanische Pflichtübung zu sein, kann der Akt der Formalisierung tatsächlich eine Quelle von Einsicht und Kreativität sein.