クリーネの第二再帰定理からクワインを構築する
Constructing a Quine from Kleene's Second Recursion Theorem (emarzion.github.io)
要約
この記事は、計算機科学におけるクリーネの第二再帰定理を用いて、プログラム自身を出力する「クワイン」を構築するプロセスを解説しています。特に、型付き・型なしラムダ計算の文脈で、この定理がどのようにクワインの存在を保証し、さらに証明論やゲーデルの不完全性定理、タルスキの定義不能定理といった論理学の概念とどのように関連するかを掘り下げています。
全文翻訳
クリーネの第二再帰定理からクワインを構築する
目次
はじめに
クワインの存在がクリーネの第2再帰定理の結果であることはよく知られています。この構成を実際に行うのがどれほど容易か、あるいは困難かを確かめたかったので、それを形式化してみることにしました。
形式化の利点の一つは、定義や証明をより明確かつ簡潔に構造化するように数学者に自然に動機づけることです。不格好な定義や構造化されていない議論の苦痛は実際に感じられるため、効率的な証明と構造化された証明という目標はしばしば一致します。機械的な作業からかけ離れた形式化という行為は、実際には洞察と創造性の源となり得ます（ちなみに、これが私が形式検証を単なる書き写しの練習と見なす一般的な見方が的外れだと考える理由です）。
これを念頭に、私は、私がかなり手短かにしか知らなかった定理に光を当てることができる、クリーンな形式化を見つけるか開発できることを願っていました。私の探求中、幸運にも、型なしラムダ計算でこの構成を実行する方法を示したこの優れたプレプリントに出会いました。この記事の残りの部分では、このプレプリントからの証明の概要を説明し、なぜこの定理をこのように提示することを選択するのかについてのいくつかの動機を提供します。
クリーネ、古典的視点
再帰定理の通常の提示は、部分帰納関数の効果的な数え上げ（ゲーデル数付け） $\lbrace \varphi_i \rbrace
_{i \in \mathbb{N}}$ を扱っていると仮定します。その場合、結果を次のように述べることができます。
定理（クリーネの第二再帰定理、古典計算論的バージョン）
$n+1$項の部分帰納関数 $\psi$ が与えられたとき、次のようなインデックス $e$ が存在します。
\[\psi(e,\bar{x}) \simeq \varphi_e(\bar{x})\]
$\psi$ を恒等関数とすると、これは推論として得られます。
\[e = \psi(e) \simeq \varphi_e()]
これをクワインと見なすことができます。直感的には、インデックス $e$ は関数 $\varphi_e$ の表現であり、したがって $\varphi_e$ は入力なしで自身の「ソースコード」である $e$ を出力するプログラムです。
計算モデル
計算理論の伝統的な提示は、すべての離散構造（ペア、リスト、構文オブジェクトなど）が単なる自然数であるという還元主義的な態度を採用する傾向があります。これには多くの面倒なエンコーディングが必要であり、提示者は言及を避けたがります。そのため、多くの手短な説明が生まれます。
このような提示はある程度理解できます。もしあなたが深い/高度な結果に到達することだけに関心があるなら、結局のところ「これらの計算モデルはすべて同等」なので、低レベルの詳細にあまり時間を費やしたくないのは理にかなっています。しかし、この種のアプローチは、形式システムに対する一種のニヒリズムを助長するリスクを伴います。すべてのシステムは同様に恣意的で醜いなど、なぜ詳細に研究する価値があるのでしょうか？
形式システムにおける構造の問題をより真剣に受け止める分野があります。それは証明論です。証明論から得た大きな教訓の一つは、形式システムの構造方法にかなりの内容が見出せるということです。したがって、構造を真剣に受け止めるモデルの探求に戻ると、計算の最も証明論的なモデルであるラムダ計算にたどり着くのは適切です。
クリーネ、関数型プログラミングの視点
最終的には型なしラムダ計算で作業しますが、型付きの再帰定理の提示を検討することは有益です。明示的な型を使用すると他の結果とのつながりがわかるでしょうが、この議論は型なしの場合にも適用されます。そこでは、型は「道徳的な型」として消えていきます（たとえば、型は実際には存在しませんが、型なしラムダ計算で $\mathbb{N} \rightarrow \mathbb{N}$ のような関数について話すことができます）。
自己反映能力を持つ関数型言語 $L$ で作業していると仮定します。特に：
- $L$ 式を表す構文木の型 $\mathsf{AST}$ を持ちます。
- $t$ が項である場合、その引用を $\lceil t \rceil : \mathsf{AST}$ と表記します。
- 関数適用のコンストラクタは中置演算子 $\cdot$ で与えられるとします。したがって、次の等式が成り立ちます。$ \lceil t_1 t_2\rceil = \lceil t_1 \rceil \cdot \lceil t_2 \rceil $
- 式自体が引用である場合に内部的に引用を実行できる準引用子を持ちます。具体的には、項 $\mathsf{q} : \mathsf{AST} \rightarrow \mathsf{AST}$ が存在し、任意の項 $t$ に対して $\mathsf{q} \lceil t \rceil = \lceil \lceil t \rceil \rceil$ が成り立ちます。つまり、$\mathsf{q}$ は単一引用符で囲まれた式を二重引用符で囲まれた式に変換する関数です。
これらの仮定の下で、クリーネの定理は次のように述べることができます。
定理（クリーネの第二再帰定理、関数型バージョン）
型 $T$ と項 $P : \mathsf{AST} \rightarrow T$ が与えられたとき、次のような項 $t : T$ が存在します。
\[P \lceil t \rceil = t\]
証明。
$d : \mathsf{AST} \rightarrow T := \lambda e. P (e \cdot \mathsf{q} \hspace{2pt} e)$ とすると、不動点式は $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}]
以前と同様に、 $P$ を恒等関数とするとクワインが得られますが、定理は任意の「構文的」なプログラムのプロパティに対して不動点を見つけるために、より広く適用できることがわかります。たとえば、$P := \mathsf{size} : \mathsf{AST} \rightarrow \mathbb{N}$ とすると、自身のサイズを出力するプログラムが得られ、$P := \mathsf{pretty}\text{_}\mathsf{print}: \mathsf{AST} \rightarrow \mathsf{string}$ とすると、プログラムが自身のソースコードをテキスト形式で出力するという、より一般的なクワインの形式が得られます。
論理学に関するいくつかの考察
再帰定理は部分帰納関数の文脈で提示されることが多いですが、私たちの証明は $L$ がチューリング完全であることを仮定していないことに注意してください。実際、算術システムの項言語という、特定の種類の全言語のクラスを考慮すると、他の論理学の分野との重要なつながりが見出されます。
ある種の高階算術で、命題の型 $\mathsf{Prop}$ を扱っていると想像してください。これはたとえば Rocq のような証明支援システムかもしれません。もし $T = \mathsf{Prop}$ とすると、不動点補題の非常に機能的な提示が得られます。これは、ゲーデルの第一不完全性定理とタルスキの定義不能定理の両方の鍵となる要素です。ここでは、それらがこの設定でどのように現れるかを示します。
- ゲーデル: 証明可能性述語を $\mathsf{Prov} : \mathsf{AST} \rightarrow \mathsf{Prop}$ とします。$P := \neg \circ \mathsf{Prov}$ と設定すると、再帰定理により、次のような $\phi$ が得られます。
\[\phi = \neg \mathsf{Prov} \lceil \phi \rceil\]
この $\phi$ がゲーデル文です。
- タルスキ: 真理述語 $\mathsf{Tr} : \mathsf{AST} \rightarrow \mathsf{Prop}$ が存在し、すべての $\phi$ に対して真理スキーム (\mathsf{Tr}\lceil \phi \rceil \iff \phi) が成り立つと仮定します。
$P := \neg \circ \mathsf{Tr}$ とすると、次のような $\phi$ が存在します。
\[\phi = \neg \mathsf{Tr}\lceil \phi \rceil \iff \neg \phi\]
型なしラムダ計算でクワインを構築する
上記で概説した証明から、ラムダ計算がかなりクリーンで簡潔な証明の概要につながることがわかりました。型なしラムダ計算が特に魅力的なのは、言語が非常にシンプルで機能が少ないにもかかわらず、非自明なプログラミングタスクを実行するのに十分な表現力があることです。言語自体を実装するというようなタスクでは、これらの品質の組み合わせが不可欠です。
上記の証明を実装するために最初に必要なのは、言語自体のAST表現です。幸いなことに、型なしラムダ計算は、チャーチ数エンコーディングを使用して、このようなツリー構造のデータを簡単に処理できます。
型なしラムダ計算は、変数、適用、ラムダ抽象で構成されます。
\[\Lambda ::= v | \Lambda \Lambda | \lambda v. \Lambda\]
これらの3つのコンストラクタは、エンコーディングでは3つのラムダ抽象 $\lambda v a l. \cdots$ として現れ、項の本体は $v, a, l$ から項の構造を直接模倣する形で構築されます。たとえば、項 $\lambda x y. y x$ を引用したい場合、次のようになります。
\[\lceil \lambda x y. y x \rceil = \lambda v a l. l (l (a (v \underline{0}) (v \underline{1})))\]
（$\underline{0}$ と $\underline{1}$ は、変数のde Bruijnインデックスのチャーチ数です）。
次に必要なのは準引用子です。これは間違いなく最も複雑な部分ですが、詳細がわかればそれほど難しくありません。
もし私たちが、一般的なFPで準引用子の等式を書き出すとしたら、次のようになるでしょう。
\[\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} e_1 \hspace{2pt} e_2) &= \mathsf{App}(\mathsf{App}(\mathsf{Constr} \hspace{2pt} \texttt{"App"}) (\mathsf{q} \hspace{2pt} e_1)) (\mathsf{q} \hspace{2pt} e_2)\ \mathsf{q}(\mathsf{Lam} \hspace{2pt} e) &= \mathsf{App} (\mathsf{Constr} \hspace{2pt} \texttt{"Lam"}) (\mathsf{q} \hspace{2pt} e) \end{aligned}]
これをチャーチエンコーディングに翻訳すると、次のようになります。
\[\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} e_1 \hspace{2pt} e_2) &= a (a (v \hspace{2pt} \underline{1}) (\mathsf{q} \hspace{2pt} e_1)) (\mathsf{q} \hspace{2pt} e_2)\ \mathsf{q}(l \hspace{2pt} e) &= a (v \hspace{2pt} \underline{0}) (\mathsf{q} \hspace{2pt} e) \end{aligned}]
ここで、$\mathsf{qn}$ はチャーチ数用の準引用子です（同様に導出されます）。私たちのチャーチエンコーディング規約 $\lambda v a l. \cdots$ によって決定される、$v, a, l$ と $v \hspace{2pt} \underline{2}, v \hspace{2pt} \underline{1}, v \hspace{2pt} \underline{0}$ の対応に注意してください。
これら3つの等式は、ASTのツリー構造に対する畳み込みを記述しています。チャーチエンコーディングは自然に畳み込みを処理するため、これらの等式を単一の項に簡単に変換できます。
すべてをまとめる
これらの構成は Rocq で実行および推論されました。これはこちらで見ることができます。
結果のクワインは、de Bruijn表記で以下に示されています。
((λ((λ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 (1 0)))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0)))))) ((1 ((1 ((1 (2 (λ(λ(1 (1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ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 0))))) ((1 ((1 ((1 (0 (0 (0 (0 ((1 ((1 (2 (λ(λ(1 0))))) ((1 (2 (λ(λ(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 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0))))))))))) (2 (λ(λ(1 (1 0)))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0)))))) ((1 ((1 ((1 (0 (0 (0 (0 ((1 (2 (λ(λ(1 0)))))) ((1 ((1 (2 (λ(λ(1 0)))))) ((1 (2 (λ(λ(1 (1 0))))))) (0 (0 ((1 (2 (λ(λ(1 0))))) (2 (λ(λ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 0)))))) (2 (λ(λ0)))))))))))) (2 (λ(λ(1 (1 0)))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0)))))))))))) (2 (λ(λ0)))))))))))
参考文献
Kleene Second Recursion Theorem: A Functional Pearl