同値性の決定不可能性
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/04/12 16:37 UTC 版)
2つのラムダ式を入力とし、それらが同値であるかどうかを判定するアルゴリズムは存在しない。これは決定不可能性が示された歴史的に最初の問題である。ここで使われる「アルゴリズム」という言葉も、もちろんきちんと定義されなければならない。チャーチは自身の証明の中で帰納的関数をその定義に用いたが、現在ではこれは適切なその他のアルゴリズムの定義と等価であることが知られている。 チャーチの証明ではこの問題を、あたえられたラムダ式に正規形が存在するかどうかという問題に帰している。正規形とは、それ以上簡約のできない同値なラムダ式のことである。チャーチの証明ではまず、この問題が決定可能である、つまり、ラムダ式で表現可能であると仮定する。クリーネによる結果とゲーデル数のラムダ式表現を用いることによってチャーチは、対角線論法によりパラドキシカルなラムダ式 e を構成した。この e を、それ自身を表すゲーデル数に適用すると矛盾が導かれる。 詳しくいえば次のようである。まず X {\displaystyle X} を正規形の存在性を判定するラムダ式とする。 A {\displaystyle A} を2つのラムダ式のゲーデル数から、それらを適用してできるラムダ式を計算する関数を表すラムダ式、 N {\displaystyle N} を自然数からそれを表すラムダ式の表現のゲーデル数を求める関数を表すラムダ式とする。すなわち、 A ⌜ x ⌝ ⌜ y ⌝ → β ⌜ ( x y ) ⌝ {\displaystyle A\ulcorner x\urcorner \ulcorner y\urcorner \to ^{\beta }\ulcorner (xy)\urcorner } N ⌜ x ⌝ → β ⌜ ⌜ x ⌝ ⌝ {\displaystyle N\ulcorner x\urcorner \to ^{\beta }\ulcorner \ulcorner x\urcorner \urcorner } が成り立つ。ここで ⌜ x ⌝ {\displaystyle \ulcorner x\urcorner } はラムダ式 x {\displaystyle x} のゲーデル数を表すラムダ式の表現である。いま、ラムダ式 e {\displaystyle e} を e := λ x . if X ( A x ( N x ) ) then Ω else λ y . y {\displaystyle e:=\lambda x.{\text{ if }}X(Ax(Nx)){\text{ then }}\Omega {\text{ else }}\lambda y.y} と定める。ここで Ω {\displaystyle \Omega } は正規形を持たないラムダ式 ( λ x . x x ) ( λ x . x x ) {\displaystyle (\lambda x.xx)(\lambda x.xx)} である。自己適用 e ⌜ e ⌝ {\displaystyle e\ulcorner e\urcorner } を計算すると次のようになる。 e ⌜ e ⌝ {\displaystyle e\ulcorner e\urcorner } if X ( A ⌜ e ⌝ ( N ⌜ e ⌝ ) ) then Ω else λ y . y {\displaystyle {\text{ if }}X(A\ulcorner e\urcorner (N\ulcorner e\urcorner )){\text{ then }}\Omega {\text{ else }}\lambda y.y} if X ( A ⌜ e ⌝ ⌜ ⌜ e ⌝ ⌝ ) then Ω else λ y . y {\displaystyle {\text{ if }}X(A\ulcorner e\urcorner \ulcorner \ulcorner e\urcorner \urcorner ){\text{ then }}\Omega {\text{ else }}\lambda y.y} if X ⌜ e ⌜ e ⌝ ⌝ then Ω else λ y . y {\displaystyle {\text{ if }}X\ulcorner e\ulcorner e\urcorner \urcorner {\text{ then }}\Omega {\text{ else }}\lambda y.y} もし e ⌜ e ⌝ {\displaystyle e\ulcorner e\urcorner } が正規形を持つならば、 e ⌜ e ⌝ {\displaystyle e\ulcorner e\urcorner } は Ω {\displaystyle \Omega } にベータ簡約される。するとチャーチ・ロッサーの定理より、 Ω {\displaystyle \Omega } は e ⌜ e ⌝ {\displaystyle e\ulcorner e\urcorner } と共通のラムダ式にベータ簡約できるから、 Ω {\displaystyle \Omega } は正規形を持つ。これは矛盾。したがって e ⌜ e ⌝ {\displaystyle e\ulcorner e\urcorner } は正規形を持たない。すると e ⌜ e ⌝ {\displaystyle e\ulcorner e\urcorner } は λ x . x {\displaystyle \lambda x.x} にベータ簡約されることになる。ラムダ式 λ x . x {\displaystyle \lambda x.x} は正規形であるので、やはり矛盾。したがって X {\displaystyle X} のようなラムダ式は存在しない。
※この「同値性の決定不可能性」の解説は、「ラムダ計算」の解説の一部です。
「同値性の決定不可能性」を含む「ラムダ計算」の記事については、「ラムダ計算」の概要を参照ください。
- 同値性の決定不可能性のページへのリンク
