素人だということを言い訳に妄想を垂れ流してみる

d.y.d. - おもしろいみろん経由で、d.y.d. - メモ化と不動点にたどり着いて、ここの部分が腑に落ちなくて、ちょっと考えていました。

ちなみにfib_makerなど再帰関数を定義する関数を渡すと、その不動点を計算する関数、なんてものもプログラムとして書くことができて、こんな風になります。こうやって定義したフィボナッチ関数はちゃんと普通に使えます。

function fix(G) {
	return G( function(x){ return fix(G)(x) } )
}
fib = fix(fib_maker)
print( fib(1), fib(2), fib(3), fib(4), fib(5) )  // 1 2 3 5 8

どうしてこう処理されるかは、（けっこう時間かかっちゃったんですが）わかったんですよ。でもやっぱりムニムニと気持ち悪い。なんでかなといえば簡単なことで、fix(G)の定義にfix(G)を使っているからなんですな。Axiom of Foundationを空気のように思っているZF人間にはこういうのがどうにも怖いわけです。まあ、それだけなら私の順応性の問題だけなのですが。
以降、言葉の細かい定義を無視して印象論で語ります。(ZF)集合論的にこれを一番普通に書き直せば、(ω+1)ステージの超限帰納法になるわけですよ。任意有限回の操作を続けるだけではなくて、それを貼り合わせた最終的な関数を作るところまでプログラムに書けちゃっているわけです。ここがどうにも衝撃的で。もちろん、具体的な自然数が与えられたときにごりごりと計算していくだけで何にも無限的操作はなされてないんだよ、生成無限的な解釈で十分なんだよ、と考えることは可能でしょうけれども、それ以上のことがありえるのではないかと妄想中なわけです。
までの順序数は、なんだかんだで表現可能なわけでコンピュータで扱えてもなんら不思議はないわけです。それを超えてもdefinableなところなら普通になんとかなるでしょう。でも、は非可算なのだから、十分大きい可算順序数はコンピュータ上のオブジェクトとして表現することは不可能なわけです。しかしながら、あんなに簡単にlimit stageを越えられるのならば、なんらかの一様な形で表現された順序数をオラクルにして表現不可能なステージまで続く超限帰納法を実現するような関数が書けてもおかしくないんじゃないかなどと。実際にコンピュータ上でそのような超限帰納法を実行することは不可能であるにしても。
実行不可能なのにそんなことを考えることに意味があるかといえば、もしそのプログラムに対する形式的証明が可能ならば意味があるのではないかと思うわけです。つまり、その超限帰納法を実現する関数がどの入力に対しても期待されたような動作をすると証明できるならば、その事実は表現不可能な長さの超限帰納法にまで適用されるのではないかと。

いや、もちろんZFだって帰納的に公理化できているのだから普通にprover作って超限帰納法がある性質を満たすかどうか証明することはできるはずなわけですよ。でも実は、ある程度以上に高階な証明支援機能を持つ言語は、すでにそういうレベルに達しちゃっているのかもしれないなと。

とかいう妄想に悩まされていたので、とりあえず書いてすっきりしておこうかなと。