Een Quine construeren vanuit Kleene's tweede recursietheorema

Inleiding

Een van de voordelen van formalisering is dat het de wiskundige natuurlijk motiveert om definities en bewijzen op een duidelijkere en beknoptere manier te structureren. De pijn van een onhandige definitie of een slecht gestructureerd argument is daadwerkelijk voelbaar, waardoor de doelen van efficiënte bewijzen en goed gestructureerde bewijzen vaak samenvallen. Verre van een mechanische klus te zijn, kan de actie van formalisering juist een bron van inzicht en creativiteit zijn (overigens is dit waarom ik denk dat de populaire visie op formele verificatie als een loutere oefening in transcriptie de plank misslaat).

Met dit in gedachten hoopte ik een schone formalisering te vinden of te ontwikkelen die licht kon werpen op een theorema waar ik alleen in vrij vage termen mee bekend was. Tijdens mijn zoektocht ontdekte ik een uitstekend preprint dat uiteenzette hoe deze constructie kan worden uitgevoerd in de ongetypeerde lambdacalculus. In de rest van dit artikel schets ik het bewijs uit dit preprint en bied ik some motivatie waarom we ervoor zouden kiezen het theorema op deze manier te presenteren.

Kleene: een klassiek perspectief

De gebruikelijke presentatie van het recursietheorema gaat ervan uit dat we werken met een effectieve nummering van de partiële recursieve functies $\lbrace \varphii \rbrace{i \in \mathbb{N}}$. We kunnen het resultaat dan als volgt formuleren:

Theorema (Kleene's tweede recursietheorema, klassieke berekenbaarheidstheoretische versie) Laat $\psi$ een $(n+1)$-aire partiële recursieve functie zijn. Er bestaat dan een index $e$ zodanig dat: \[\psi(e,\bar{x}) \simeq \varphi_e(\bar{x})\]

Quines volgen als een corollary wanneer we $\psi$ als de identiteitsfunctie nemen, wat ons geeft: \[e = \psi(e) \simeq \varphi_e()\]

Als we goed kijken, kunnen we ons voorstellen dat dit een Quine is. Intuïtief is de index $e$ een representatie van de functie $\varphie$, en dus is $\varphie$ een programma dat bij geen enkele input $e$ output: zijn eigen "broncode".

Computatiemodellen

Traditionele presentaties van de berekenbaarheidstheorie neigen naar een reductionistische houding waarbij alle discrete structuren (paren, lijsten, syntactische objecten, etc.) simpelweg natuurlijke getallen zijn. Dit noodzaakt tot veel tedious coderingen waarvan de details door de presentator liever niet worden genoemd, waardoor we veel "hand-waving" krijgen.

Dit soort presentatie is tot op zekere hoogte begrijpelijk. Als je alleen geïnteresseerd bent in het bereiken van diepe of geavanceerde resultaten, is het logisch dat je niet te veel tijd wilt verspillen aan laagwaardige details, aangezien "al deze computatiemodellen toch equivalent zijn". Echter, deze benadering brengt het risico met zich mee dat er een soort nihilisme ontstaat ten aanzien van formele systemen: alle systemen zijn even arbitrair en lelijk, dus waarom zou je ze überhaupt in detail bestuderen?

Er is een subveld dat structurele kwesties in formele systemen serieuzer neemt: de bewijstheorie. Een van de belangrijkste inzichten die ik uit de bewijstheorie heb gehaald, is dat er aanzienlijke inhoud te vinden is in de manier waarop we onze formele systemen structureren. Dus, terugkerend naar de berekenbaarheidstheorie, is het passend dat onze zoektocht naar een model dat structuur serieus neemt, ons leidt naar het meest bewijstheoretische computatiemodel: de lambdacalculus.

Kleene: een functioneel programmeringsperspectief

Hoewel we uiteindelijk in de ongetypeerde lambdacalculus zullen werken, is het nuttig om een getypeerde presentatie van het recursietheorema te overwegen. We zullen zien dat het gebruik van expliciete typen verbindingen legt met andere resultaten, maar het argument is nog steeds van toepassing op het ongetypeerde geval, waar de typen wegvallen als "morele typen" (bijvoorbeeld kunnen we nog steeds spreken van functies $\mathbb{N} \rightarrow \mathbb{N}$ in de ongetypeerde lambdacalculus, zelfs als de typen er technisch gezien niet zijn).

We gaan ervan uit dat we werken in een functionele taal $L$ die in staat is tot zelfreflectie. In het bijzonder:

• Het heeft een type $\mathsf{AST}$ van syntaxbomen die $L$-expressies representeren: als $t$ een term is, dan duiden we $\lceil t \rceil : \mathsf{AST}$ als diens citering (quotation).
• De constructor voor functie-applicatie wordt gegeven door de infix $\cdot$, waardoor de volgende vergelijking geldig is:

$ \lceil t1 t2\rceil = \lceil t1 \rceil \cdot \lceil t2 \rceil $

• Het heeft een quasi-citeerder (quasi-quoter) die in staat is om intern citeringen uit te voeren wanneer de expressie zelf een citaat is. Specifiek is er een term $\mathsf{q} : \mathsf{AST} \rightarrow \mathsf{AST}$ zodanig dat voor elke term $t$ geldt dat $\mathsf{q} \lceil t \rceil = \lceil \lceil t \rceil \rceil$. In andere woorden, $\mathsf{q}$ is een functie die enkelvoudig geciteerde expressies omzet in dubbel geciteerde expressies.

Met deze aannames kan Kleene's theorema als volgt worden geformuleerd:

Theorema (Kleene's tweede recursietheorema, functionele versie) Laat $T$ een type zijn en $P : \mathsf{AST} \rightarrow T$. Er is dan een term $t : T$ zodanig dat $P \lceil t \rceil = t$.

Bewijs: Neem $d : \mathsf{AST} \rightarrow T := \lambda e. P (e \cdot \mathsf{q} \hspace{2pt} e)$. Dan is onze fixpunt-expressie $t := d \lceil d \rceil$:

\[\begin{aligned} t &= d \lceil d \rceil \\ &= (\lambda e. P (e \cdot \mathsf{q} \hspace{2pt} e)) \lceil d \rceil \\ &= P (\lceil d \rceil \cdot \mathsf{q} \lceil d \rceil) \\ &= P (\lceil d \rceil \cdot \lceil \lceil d \rceil \rceil) \\ &= P \lceil d \lceil d \rceil \rceil \\ &= P \lceil t \rceil. \end{aligned}\]

Zoals eerder vermeld, krijgen we Quines wanneer we $P$ als de identiteitsfunctie nemen, maar we zien dat het theorema breder kan worden toegepast om fixpunten te vinden voor elke soort "syntactische" eigenschap van een programma. Bijvoorbeeld:

• Door $P := \mathsf{size} : \mathsf{AST} \rightarrow \mathbb{N}$ te nemen, produceren we een programma dat zijn eigen grootte output.
• Door $P := \mathsf{pretty}\text{_}\mathsf{print}: \mathsf{AST} \rightarrow \mathsf{string}$ te nemen, verkrijgen we de bekendere vorm van een Quine als een programma dat zijn eigen broncode in tekstformaat print.

Enkele logische excursies

Hoewel het recursietheorema vaak wordt gepresenteerd in de context van partiële recursieve functies, moet worden opgemerkt dat ons bewijs er niet van uitgaat dat $L$ Turing-compleet is. Sterker nog, we vinden belangrijke verbindingen met andere gebieden van de logica wanneer we Kleene beschouwen in de context van een specifieke klasse van totale talen: de termtalen van aritmetische systemen.

Stel dat we werken in een soort hogere-orde aritmetica met een type proposities $\mathsf{Prop}$. Dit zou bijvoorbeeld een bewijsassistent zoals Rocq kunnen zijn.

Als we $T = \mathsf{Prop}$ nemen, hebben we een zeer functionele presentatie van het diagonaallemma, het sleutelelement voor zowel Gödels eerste onvolledigheidsstelling als Tarski's ondefinbaarheidsstelling. Hier is hoe deze twee in deze setting verschijnen:

• Gödel: Neem $\mathsf{Prov} : \mathsf{AST} \rightarrow \mathsf{Prop}$ als ons bewijsbaarheidspredikaat. Als we $P := \neg \circ \mathsf{Prov}$ instellen, geeft het recursietheorema ons een $\phi$ zodanig dat:

\[\phi = \neg \mathsf{Prov} \lceil \phi \rceil\] Deze $\phi$ is de Gödel-zin.

• Tarski: Stel dat $\mathsf{Tr} : \mathsf{AST} \rightarrow \mathsf{Prop}$ een waarheidspredikaat is, wat betekent dat het waarheidsschema

\(\mathsf{Tr}\lceil \phi \rceil \iff \phi\) geldt voor alle $\phi$. Neem $P := \neg \circ \mathsf{Tr}$. Er is dan een $\phi$ met: \[\phi = \neg \mathsf{Tr}\lceil \phi \rceil \iff \neg \phi\]

Een Quine bouwen in de ongetypeerde lambdacalculus

Uit het bovenstaande bewijs hebben we gezien dat lambdacalculi leiden tot een vrij schone en beknopte bewijsschets. Wat de ongetypeerde lambdacalculus bijzonder aantrekkelijk maakt, is dat de taal zeer eenvoudig is met weinig functies, terwijl hij toch expressief genoeg is om niet-triviale programmeertaken uit te voeren. Voor een taak als deze, waarbij we de taal binnen zichzelf moeten implementeren, is deze combinatie van kwaliteiten essentieel.

Het eerste dat we nodig hebben om het bovenstaande bewijs te implementeren, is een AST-representatie van de taal zelf. Gelukkig kan de ongetypeerde lambdacalculus dergelijke boomstructuren eenvoudig afhandelen met Church-coderingen.

De ongetypeerde lambdacalculus bestaat uit variabelen, applicaties en lambda-abstracties: \[\Lambda ::= v | \Lambda \Lambda | \lambda v. \Lambda\]

Deze drie constructoren verschijnen in de codering als drie lambda-abstracties $\lambda v a l. \cdots$, waarbij het lichaam van de term wordt opgebouwd uit $v, a, l$ op een manier die direct de structuur van de term spiegelt. Als we bijvoorbeeld de term $\lambda x y. y x$ willen citeren, krijgen we dit: \[\lceil \lambda x y. y x \rceil = \lambda v a l. l (l (a (v \underline{0}) (v \underline{1})))\] ($\underline{0}$ and $\underline{1}$ zijn de Church-getallen van de de Bruijn-indices van de variabelen).

Het laatste wat we nodig hebben is een quasi-citeerder. Dit is absoluut het meest complexe deel, maar het is niet te erg zodra je de details op orde hebt.

Als we de vergelijkingen voor een quasi-citeerder in colloquiaal FP zouden uitschrijven, zou het er ongeveer zo uitzien: \[\begin{aligned} \mathsf{q}(\mathsf{Var} \hspace{2pt} i) &= \mathsf{App} (\mathsf{Constr} \hspace{2pt} \texttt{"Var"}) (\mathsf{Num} \hspace{2pt} i)\\ \mathsf{q}(\mathsf{App} \hspace{2pt} e1 \hspace{2pt} e2) &= \mathsf{App}(\mathsf{App}(\mathsf{Constr} \hspace{2pt} \texttt{"App"}) (\mathsf{q} \hspace{2pt} e1)) (\mathsf{q} \hspace{2pt} e2)\\ \mathsf{q}(\mathsf{Lam} \hspace{2pt} e) &= \mathsf{App} (\mathsf{Constr} \hspace{2pt} \texttt{"Lam"}) (\mathsf{q} \hspace{2pt} e) \end{aligned}\]

Vertaald terug naar onze Church-codering: \[\begin{aligned} \mathsf{q}(v \hspace{2pt} \underline{i}) &= a (v \hspace{2pt} \underline{2}) (\mathsf{qn} \hspace{2pt} \underline{i})\\ \mathsf{q}(a \hspace{2pt} e1 \hspace{2pt} e2) &= a (a (v \hspace{2pt} \underline{1}) (\mathsf{q} \hspace{2pt} e1)) (\mathsf{q} \hspace{2pt} e2)\\ \mathsf{q}(l \hspace{2pt} e) &= a (v \hspace{2pt} \underline{0}) (\mathsf{q} \hspace{2pt} e) \end{aligned}\] waarbij $\mathsf{qn}$ een quasi-citeerder is voor Church-getallen (op vergelijkbare wijze afgeleid). Let op dat de correspondentie tussen $v, a, l$ en $v \hspace{2pt} \underline{2}, v \hspace{2pt} \underline{1}, v \hspace{2pt} \underline{0}$ wordt bepaald door onze Church-coderingsconventie $\lambda v a l. \cdots$.

Deze drie vergelijkingen beschrijven een fold over de boomstructuur van de AST's. Aangezien Church-coderingen van nature folds afhandelen, kunnen we deze vergelijkingen gemakkelijk omzetten in een enkele term.

Alles samenbrengen

Deze constructies zijn uitgevoerd en geanalyseerd in Rocq. De resulterende Quine wordt hieronder getoond in de Bruijn-notatie:

((λ((λ0) (((λ(λ(λ(λ(λ((1 (((4 2) 1) 0)) (((3 2) 1) 0))))))) 0) ((λ(λ(λ(λ(0 (0 (0 (((((λ(λ(λ(λ(((3 ((((λ(λ(λ(λ((2 (3 (λ(λ(1 (1 0)))))) (((((λ(λ(λ(λ(1 (1 (((((λ(λ(λ(λ((0 (2 (3 (λ(λ(1 0)))))) (3 (λ(λ0)))))))) 3) 2) 1) 0))))))) 3) 2) 1) 0)))))) 2) 1) 0)) ((((λ(λ(λ(λ(2 ((2 (3 (λ(λ(1 0))))) 0)))))) 2) 1) 0)) ((((λ(λ(λ(1 (2 (λ(λ0))))))) 2) 1) 0)))))) 3) 2) 1) 0)))))))) 0)))) (λ(λ(λ(0 ((1 (0 (2 (λ(λ0))))) ((1 ((1 (0 (0 (0 (0 (0 ((1 ((1 (2 (λ(λ(1 0))))) ((1 ((1 ((1 (2 (λ(λ(1 (1 (1 0)))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0)))))) ((1 ((1 ((1 (2 (λ(λ(1 (1 (1 0))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0))))))))))) (2 (λ(λ0))))) ((1 (0 (0 (0 (0 ((1 (2 (λ(λ0)))) ((1 (2 (λ(λ0)))) ((1 (2 (λ(λ0)))) ((1 ((1 ((1 ((1 (0 (0 (0 (0 ((1 ((1 (1 (2 (λ(λ(1 (1 (1 0))))))) ((1 ((1 ((1 (0 (0 (0 (0 ((1 ((1 (2 (λ(λ(1 (1 0)))))) ((1 (2 (λ(λ(1 (1 (1 0))))))) (0 (0 ((1 (2 (λ(λ(1 0))))) ((1 (2 (λ(λ(1 0))))) (2 (λ(λ0)))))))))) ((1 ((1 ((1 ((1 (0 (0 (0 (0 ((1 (2 (λ(λ(1 0))))) ((1 (2 (λ(λ(1 0))))) ((1 ((1 ((1 ((1 (0 (0 (0 (0 ((1 ((1 (2 (λ(λ0)))) ((1 (2 (λ(λ(1 (1 0)))))) ((1 (2 (λ(λ(1 (1 (1 0))))))) (0 (0 ((1 (2 (λ(λ(1 0))))) (2 (λ(λ0)))))))))) ((1 (2 (λ(λ(1 (1 (1 0))))))) (0 (0 (2 (λ(λ0)))))))))))) (2 (λ(λ(1 (1 (1 0)))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0))))))))))) (2 (λ(λ(1 (1 (1 0)))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0)))))))))) (2 (λ(λ(1 (1 (1 0))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0)))))) ((1 ((1 ((1 (0 (0 (0 (0 ((1 (2 (λ(λ(1 (1 0)))))) ((1 ((1 (2 (λ(λ(1 (1 0)))))) ((1 (2 (λ(λ(1 (1 (1 0))))))) (0 (0 ((1 (2 (λ(λ(1 0))))) (2 (λ(λ0))))))))) (2 (λ(λ0)))))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0)))))) ((1 ((1 ((1 (0 (0 (0 ((1 (2 (λ(λ(1 0))))) ((1 (2 (λ(λ(1 (1 0)))))) (0 (0 (2 (λ(λ0))))))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0)))))))))) (2 (λ(λ(1 (1 (1 0)))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0)))))))))))) (2 (λ(λ0)))))))))))

Referenties

Kleene Second Recursion Theorem: A Functional Pearl Geschreven op 28 oktober 2026