ぶっちゃけgenericってなによって話。

これ、書いてみます。まあ、比喩なので完璧なものでないことは断っておきます。

Twitter / kururu_goedel: genericっていうのは、ぶっちゃけ「ground mod ...

例えば何かリーズナブルなプログラミング言語にオラクルとしてなにか計算不可能な自然数から自然数への関数gを付け加えるとしましょう。これだけだとひどく不自然な話に見えますが、人間からの入力とか不確定な実験の結果とかが入り込んでくるとすればそんなに変な話ではないかと。
このgを使ってプログラムを書くことを考えます。gはオラクルとして与えられているということ以外は普通の関数なので、例えばg(0)+g(1)を返す関数だとかを書くことができます(えーと、その程度にはまともな言語を使っていることにして)。そして、g(n), g(n+1), ..., g(n+100)が全て0となるようなnがあったら1、そうでなければ無限ループ、みたいなのも。
無限ループして止まらないのは良いとしましょう。それは普通のプログラミングでもよく起こることですから。でも、この関数の返値はgの有限部分では決まりません。もちろん上記のようなnが存在すればそこで関数は止まります。ですが、例えばg(0), g(1), ..., g(一億)とかまで計算してまだ存在していなくても、もっと大きいところでは成り立っているかもしれません。この関数が止まるか止まらないかはオラクルさんの気分次第です。

これがgenericityを使って避けたい状況なんです。つまり、gを使って書ける(出力が有限な)関数の返値は、全てgの有限個の入力に対する返値を見えてやればわかる、と。そうなるようにオラクルに制限をつけるわけです。どのような制限かというと、「プログラムで書けるような、gの有限個の値で起きないことを確定できないようなことは全て起きている」ということです。例えば上記の100個連続して0が出れば1というような関数を考えましょう。オラクルを決定する権限のある人ならば、gの値をどれだけ多く確定してもそれが有限である限り、まだ確定されていない部分をとって100個0を並べてこの関数を停止させることができます。だから、genericであるならば、この現象はどこかしらで起きて、この関数は終了して1を返すわけです。

このことによって、比喩を止めて強制法のほうに戻ると、Vの中である程度コントロールできるような形でVの拡張V[G]を得られるようになるわけです。えーと、これで伝わるかはわかりませんが、予定時間を10分で書くはずが時間が30分オーバーしているのでこれでおしまいにしておきます。もっと強制法っぽい説明はまた今度ということで。