レイフィケーションとゲーデル符号化

ゲーデル符号化、記号とかその解釈とか - 檜山正幸のキマイラ飼育記 メモ編 ：

本来、ゲーデル符号＝ゲーデル数は論理式とか証明とかに対して付けられている。構文領域から数領域への関数。だけど、構文領域に意味論があるなら（たいていはある）、意味領域から数領域への関数だと思ってもよいだろう。

いや、意味領域内の符号化（符号空間への単射）までゲーデル符号化と呼ぶのはやっぱりマジイ気もしてきた。混乱を招きそうだ。

なんらかの項（構文的なモノ）の全体をTermとして、符号の空間をKとする。G:Term→Kはゲーデル符号化と呼んでいいだろう。ここで、像集合 G(Term)⊆K への所属は実効的に判定できて、部分的逆写像 G^~: K⊃G(Term)→ Term が定義できる、という条件がある。要するに、「nはゲーデル数である」とか「nは項tのゲーデル数である」とかが計算でちゃんと決着が付く。

Termに意味関数【-】:Term→Denoがあるとして、g(【t】) = G(t) となる g:Deno→K があればいいが、たいていそんなものはない。そうじゃなくて、c:Deno→Termを使って、【c(a)】= g(a) とする。cは意味に対して構文を一意に割り当てることだから、正規形だと思ってよい。

特に、適当な領域Dがあって、D⊆Term（定数として）、Deno = D^D のときが問題になる。g:D^D→D をゲーデル符号化と呼ぶのが適切か？ Term上のゲーデル符号化と正規化のアルゴリズムがあれば、gを定義できるが、、、これはやっぱりゲーデル符号化と呼ばない方が無難だよな。

このケースではレイフィケーションがいいんじゃないのかな。それと、反射的（reflexive）とかEPペアとかレトラクトとかも、用語と定義を整理したほうがいいな。

• 「λ代数、万能対象」も参照。