はじめに
自己言及、再帰、不動点 etc. こういった術語は論理学や計算論でしばしば目にするし、互いに関連しあって独特の世界を構築していることはなんとなく知っている人も多いと思います。
不動点定理を使ってそれらを統一的にスッキリ見せましょうという資料をウェブサーフィンしていると見つけたので、要点を整理します。参考文献はRIMSの資料です:
完全に理解できているとは思わないのでツッコミやご指導あればコメントください。
要点
不動点定理: A→Bなる任意の関数を、A×A→Bなる万能関数φで定義できるならば、B→Bなる任意の関数fの不動点を構成できる: f(φ(x,x)) の指標をaとすると φ(a,a) がf の不動点となる。
ラッセルのパラドックス: Sをすべての集合の集合と仮定する。S×S→2なる関数 if y∈x then T else F は万能関数である。従って不動点定理より2→2なる任意の関数、特に否定演算が不動点を持つことになるが、これは直ちに矛盾を帰結する。
カントールの対角線論法: 2^X から X への単射が存在すると仮定する。これは X から 2^X への全射 Ψ が存在することと同値。ここで if y∈ψ(x) then T else F なる X×X→2 な関数は万能関数となる。したがって2→2なる任意の関数、特に否定演算が不動点をもつがこれは直ちに矛盾を帰結する。
Yコンビネータとラッセルのパラドックス: ラムダ計算におけるYコンビネータ (λf. (λx. f (x x)) (λx. f (x x))) とラッセルのパラドックスは不動点定理を介して同一のものを表す。すなわち
- λx.P に {x | P x}
- (M N) に N ∈ M
- f M に ¬M
を対応付けることができ,そうすると (Y f) は {x|x ∉ x} ∈ {x|x ∉ x} が対応するので、 (Y f) = f (Y f) はラッセルのパラドックスそのものとなる。
詳細/証明
不動点定理の証明のようなもの: a の定義から, φ(a,x) = f(φ(x,x)) これに a を適用すると φ(a,a)=f(φ(a,a)) を得るがこれは φ(a,a) が fの不動点であることを自明に示す。
ラッセルのパラドックスでの万能関数の確認: 任意の関数g:S→2に対して {x∈S | g(x)=T} がgの指標になる。本当にそうなっているかを確認するためには、代入してみればよい。つまり if y∈{x∈S | g(x)=T} then T else F が g に一致するかをみればよい。任意のSの元yに対してg(y) がT or F なので、場合分けをして考えれば両者の値が一致することは容易に示せる。
否定演算が矛盾を帰結するとは？: 否定演算が2→2な演算なのはすぐわかる。否定演算が不動点を持つということは neg(a) = a なる a∈2 が存在することになるが T も F もそれを満たさない。
単射と全射の補題の証明: 「AからBへの単射が存在する」⇔「BからAへの全射が存在する」の証明。（⇒の証明）自明。求めたい写像の、単射のImageへの制限が単射の逆写像となるようにとればよい。（⇐の証明）自明。
カントールの対角線論法での万能関数の確認: 任意の関数 g:X→2について あるa∈X が存在して g = if y∈Ψ(a) then T else F となることを示せばよい。Ψの全射性から Ψ(a) = {x∈X | g(x)=T} となるような a∈X が存在する。これを代入すると、示すべきは g = if y∈ {x∈X | g(x)=T} then T else F となる。これは上述のラッセルの例と全く同一なので、証明略。