昨日の「ゲーデル化をどうするか？」の続きです。
内容：
「コード」という言葉
昨日の記事の途中「ゲーデル化をどうするか？ // プログラミング言語の利用」で、「コード」という言葉の多義性で“ウワーってなって”います。
ゲーデル化＝ゲーデル符号化の写像 G:S→D に対して、Sの要素を「コード」と呼ぶときもあれば、Dの要素を「コード」と呼ぶときもあるのです。「コード」という言葉は、ものすごくよく使うし、とても便利な言葉なんですが、混乱を避けるには使わないのが無難かな。
写像Gの余域である集合Dの要素は、漢字で「符号」と書き、encode/encodingは「符号化」、decode/decodingは「脱符号化」。D自体は「データ領域」「符号集合」「符号空間」とか呼びましょう。
では、写像Gの域である集合Sの要素は何と呼ぶ？ … … ウーン。Sはのっぺらぼうな集合じゃなくて、「原子記号、定数記号、項、論理式、証明」のような階層があるんですよね。みんなひっくるめて呼ぶときは … 「式」〈expression〉かな。データの種類としては文字列とみなすので、「テキスト」でもいいかな。論理ってさ*1、いうほど概念・用語が整理・整備されてないんだよね。
ゲーデル符号が自然数であることのメリット
「ゲーデル化をどうするか？」で、ゲーデル化＝ゲーデル符号化の値が自然数であるのは辛い、と書きました。しかしもちろん、符号が自然数であることによるメリットがあります。
扱うデータは自然数だけなので、集合（基本データ型）は、Nだけでこと足ります。関数は、f:Nn→N という形のものだけ考えれば十分です。データ領域を含む意味論的システムが単純であり、それに伴い構文論的システムもまた単純なもので済みます。単純さはメリットです。
「ゲーデル化をどうするか？」より：
構文的対象Aに対するG(A)は巨大な数になってしまい、...[snip]... ゲーデル数G(A)を見て、Aを想像するのもほぼ不可能です。
ゲーデル符号G(A)を見ても、もとの構文的対象Aがサッパリ分からないのはメリットと捉えることもできます。ゲーデル符号化は、構文的対象の無意味化／脱意味化という側面も持ちます。もともとは意味を持っていた構文的対象から意味を剥ぎ取って単なるデータにする働きがあります。G(A)を見ても意味が分からないことは、十分に無意味化／脱意味化されていることになります。
コード[構文的対象]とデータ[符号]があまりにもソックリだと、コード[構文的対象]とデータ[符号]の違いを意識できなかったり混乱したりするかも知れません。
ホモアイコニック言語を使ったゲーデル符号化（クォーティング）の難点は、無意味化／脱意味化の効果が薄いことです。意味が容易に想像できるデータに対して「意味を考えるな！」と言われても難しいんですよ。人間の意味的連想力って、ほんとに強烈で制御困難なんです*2。
ゲーデル化を具体的に定義したいわけ
ゲーデル自身が使ったゲーデル化（符号化）を「オリジナルのゲーデル化」と呼ぶことにします。オリジナルのゲーデル化は、 G:S→N という写像で、Nの演算や性質（算術〈arithmetic〉と呼ぶ）で組み立てられます。Gは、原理的には明確で簡単な関数です。が、現実的にはほぼ計算できません。
現実的（理論的じゃないよ！）に計算できるかどうかは、ゲーデルの不完全性定理にとってはどうでもいいことです。なんなら、「G:S→N という写像があったとしましょう」からスタートしてもいいかも知れません。Gの存在を信用できない人のために、具体的な定義を一応は出すだけで、値をホントに計算したいわけじゃないのです。
でも僕は、値をホントに計算したいのです。しかも手で。Gに対して、「定理の証明のための概念上の道具」とは若干別な用途を想定しています。Nとは限らない（つうか、Nじゃない）データ領域Dに対して、G:S→D を具体的に定義することは、Sの構造をハッキリと理解する助けになります。そして、具体的な式（項／論理式／証明）Aに対して、G(A)をホントに手で計算することは、システムに対する実感を得るのに効果があるからです。
以上の動機からは、写像Gは、明示的／具体的に定義される必要があるし、現実的に手で計算できる写像であることも要件です。オリジナルのゲーデル化ではうまくないですね。手で計算できないもん。
ツリー構造が良さそうなわけ
「ゲーデル化をどうするか？」で、テキストとしての式（構文的対象）をパーズしたツリーをデータにする案を述べました。まだ、決定ではなく案ですが。
ノードにラベル（文字列だと思ってください）をくっつけたツリー構造というのは、かなり馴染み深いデータ構造だと思います。実際によく利用されます。その操作や性質もよく知られています。小学生でも知っている自然数には負けますが、ポピュラーなデータ／データ領域と言っていいでしょう。
オリジナルのゲーデル化では、項や論理式は（下位の）記号の列とみなします。それはまーいいのですが、証明も論理式の列とみまします -- これはどうなの？ 「定理の証明のための概念上の道具」としてはそれでもいいでしょう。しかし、手で符号化／脱符号化を実際に計算する場合は嬉しくないです。
命題の列が証明であるのは、列内の命題が、それより前に出現する命題（複数でもよい）から、なんらかの推論規則で導出できる場合です。この基準で、命題列が最後の命題の証明になっているか／なってないかを判断できます。実際の（形式化してない）証明も、おおむね命題の列だと言えるでしょう。
でもね、命題の列としての証明というのは分かりにくい。自然演繹でもシーケント計算でも、（形式化された）証明は、ツリー構造に編成されています。証明をデータとして扱う場合、リストよりはツリーのほうがずっと扱いやすいです。この理由もあって、証明も含めた構文的対象の符号化データはツリーがいいと思うのです。
データ領域Dを、ラベル付きツリーの集合と決めると、自然数の加減乗除に対応するものは、ツリーに対する様々な操作です。ツリーの操作（演算）は、大雑把な合意はあるでしょうが、算術のように強い標準はないので、あらためてハッキリと決める必要があります。ツリーの算術を設定するわけです。
そんなわけで
自然数の算術の代わりにツリーの算術を確定して、ツリー算術の意味での計算可能性／定義可能性／表現可能性／構成可能性（どれも似たりよったり）を考えようかな*3、と思っています。ツリーの算術は自然数の算術ほどにポピュラーじゃないにしろ、学習負担はさほどではなく、表現力は相当に強力です。
先に述べた「符号が自然数であることによるメリット」は失われるけど、それはトレードオフだからしょうがない。あと、ちょっと懸念があるのは、「ゲーデル化をどうするか？」で触れた心理的インパクトかな。心理的な問題だから、優先度は高くないですけど。
