クリーン第二再帰定理は、自己参照的なプログラムの構築を可能にする計算可能性理論における基本的な結果です。古典的な形式では、この定理は任意の部分再帰関数 $\psi$ に対して、関数 $\varphi_e$ が $\psi(e, \bar{x})$ として振る舞うようなインデックス $e$ が存在することを述べています。クワインはこの定理の特定の系として位置づけられます。$\psi$ を恒等関数に設定することで、実行時に自身のソースコードを出力するプログラムを表すインデックス $e$ を見つけることができるのです。この概念は抽象的な用語で議論されることが多いですが、この構築を形式化することは、自己参照が計算の基礎となる論理によって構造的にどのように支えられているかを理解するためのより明確な道筋を提供します。
この画像は、関数インデックス $e$ が望ましい性質として振る舞う $\varphi_e$ を持つように見つかるという、クリーン第二再帰定理の核心的な数学的特性を説明しています。
この特定の記法は、固定点を見つけることでクワインが定理の系であることを説明する記事の内容を直接裏付けています。
抽象的な理論から具体的な実装へと移行するために、関数型プログラミングの視点を採用することができます。このモデルでは、言語 $L$ が構文木のための型 $\mathsf{AST}$ と、内部的に引用を実行できる準クォーター $\mathsf{q}$ を持つと仮定します。これらの仮定の下では、定理は次のように述べられます。任意の型 $T$ と任意の性質 $P : \mathsf{AST} \rightarrow T$ に対して、$P \lceil t \rceil = t$ となる項 $t : T$ が存在します。この証明には、性質 $P$ を捉える項 $d$ を構築し、その後に固定点 $t := d \lceil d \rceil$ を見つけるプロセスが含まれます。このアプローチは、この定理が単にクワインに関するものだけではなく、自身のサイズや自身の整形済みソースコードを出力するプログラムなど、あらゆる構文的な性質に対する固定点を見つけることに関するものであることを示しています。
これを無型ラムダ計算で実装するには、Church符号を用いて言語自身の構文を表現する必要があります。無型ラムダ計算は木構造のデータを扱うのに十分な表現力を持っているため、変数、適用、およびラムダ抽象をそれ自体としてラムダ抽象として符号化するAST表現を定義できます。最も複雑なコンポーネントは準クォーターであり、これはASTのツリー構造に対するfoldとして定義される必要があります。これらの方程式をChurch符号に変換することで、de Bruijn記法によるクワインを構築できます。この形式化は重要なトレードオフを浮き彫りにしています。無型ラムダ計算は型制約を取り除くことで証明を簡略化する一方で、高レベルの関数型言語と同じ結果を得るためには、ASTおよび引用メカニズムの厳密かつ手動な構築が必要となります。