コンビネータ計算の非決定性とは? わかりやすく解説

Weblio 辞書 > 辞書・百科事典 > ウィキペディア小見出し辞書 > コンビネータ計算の非決定性の意味・解説 

コンビネータ計算の非決定性

出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2021/09/10 14:50 UTC 版)

コンビネータ論理」の記事における「コンビネータ計算の非決定性」の解説

一般的なコンビネータ項正規形を持つかどうか二つコンビネータ項が同じかどうか判定できない。これは、対応するラムダ項における非決定性と同じである。直接的な証明は以下のようになる。まず、以下の項を見てみよう。 Ω = (S I I (S I I)) この項は正規形持たない。なぜなら、以下に示すようにこれは自分自身簡約するからである。 (S I I (S I I)) = (I (S I I) (I (S I I))) = (S I I (I (S I I))) = (S I I (S I I)) そして、明らかにこれ以上短い式を作る簡約はない。正規形検出するコンビネータNを考えてみよう。 (N x) => T, if x has a normal form F, otherwise. (TとFはチャーチエンコーディングにおける真理値表現する。λx.λy.xとλx.λy.yで、コンビネータの形ではT = K and F = (K I)である。)そして、 Z = (C (C (B N (S I I)) Ω) I) (S I I Z)という項を考えてみよう。(S I I Z)は正規形を持つだろうか?それはもしこのようにしたとき、こうなる。 (S I I Z) = (I Z (I Z)) = (Z (I Z)) = (Z Z) = (C (C (B N (S I I)) Ω) I Z) (definition of Z) = (C (B N (S I I)) Ω Z I) = (B N (S I I) Z Ω I) = (N (S I I Z) Ω I) 今、Nを(S I I Z)に適用する必要がある。(S I I Z)が正規形を持つか、そうでないか。もしそれ正規形を持つならば、以下のように簡約される。 (N (S I I Z) Ω I) = (K Ω I) (definition of N) = Ω しかし、Ωは正規形持たないため、矛盾している。もし、(S I I Z)が正規形持たないならば、このように簡約する。 (N (S I I Z) Ω I) = (K I Ω I) (definition of N) = (I I) I (S I I Z)の正規形は単にIであり、また矛盾生む。したがって仮定した正規形コンビネータNは存在できないライスの定理におけるコンビネータ論理の例(原文:The combinatory logic analogue)が言うのは、完全で非自明な述語存在しないという事である。ある述語コンビネータであるということは適用の際にTrueFalseどちらか返すということである。もし2つNA=TNB=F満たすような2つ引数A,Bが存在するとき、その述語Nは非自明であるという。また、NMいかなる引数Mについても正規形をしているとき、そしてその時限り述語Nが完全であるという。ライスの定理の例は、全ての完全な述語自明であると述べている。この定理の証明はかなり単純である。 証明:背理法よる。完全で非自明な述語存在仮定し、N と呼ぶことにする。 Nは非自明であるから以下を満たすコンビネータA,Bが存在する。 (N A) = T(N B) = F Define NEGATION ≡ λx.(if (N x) then B else A) ≡ λx.((N x) B A)Define ABSURDUM ≡ (Y NEGATION) 不動点定理により、ABSURDUM ≡ (Y NEGATION) = (NEGATION (Y NEGATION)) ≡ (NEGATION ABSURDUM)を満たすABSURDUM = (NEGATION ABSURDUM)が与えられる。 Nは完全であるから以下の2つのうちどちらか満たす。 (N ABSURDUM) = F (N ABSURDUM) = T 場合1: F = F = (N ABSURDUM) = N (NEGATION ABSURDUM) = (N A) = T これは矛盾である。 場合2: T = (N ABSURDUM) = N (NEGATION ABSURDUM) = (N B) = F これもまた矛盾である。 故に、 (N ABSURDUM) は真であってもであってもNが完全で非自明な述語であることに反する。QED。 この論証不明定理からすぐに、正規形をもつ条件を満たすかどうか決定することができる完全な述語存在しないことが導かれる。さらに、 (EQUAL A B) = T if A = B and(EQUAL A B) = F if AB. でのEQUALのような完全な述語存在しないことも言える。もしもEQUAL存在したならば、全てのAについて λx.(EQUAL x A) は完全で非自明な述語なければならない。 この結果コンビネータ論理決定不能性を意味しないことに注意しなければならない。これらの結果のいうところは、コンビネータそれ自身引数取り(ある条件を満たす性質判定するコンビネータ存在しないということであり、計算論的な意味の不能性を意味するわけではない実際コンビネータ構文的等価性上の定理によればコンビネータにより判定することはできないコンビネータ論理の定義には異な変数記号体系内で区別するような規則何一つとして含まれてはいない)が、明らかに計算可能である。コンビネータ論理決定不能性を示すには、コンビネータゲーデル数用いて自然数コーディングの上で、ゲーデル数を表すコンビネータ引数取り(ある条件を満たす性質判定するコンビネータ存在しないということ証明すればよい。一般に非自明かつweak同値性に関して閉じたn-項関係は決定不能である。それゆえ上述たような述語は、ゲーデル数用いてもなお表現できない。その証明最初に述べた証明多少変更するだけで得られる一方で、あるゲーデル数に対してコンビネータ構文的等価性判定するコンビネータ構成するともできる

※この「コンビネータ計算の非決定性」の解説は、「コンビネータ論理」の解説の一部です。
「コンビネータ計算の非決定性」を含む「コンビネータ論理」の記事については、「コンビネータ論理」の概要を参照ください。

ウィキペディア小見出し辞書の「コンビネータ計算の非決定性」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。 お問い合わせ



英和和英テキスト翻訳>> Weblio翻訳
英語⇒日本語日本語⇒英語
  

辞書ショートカット

すべての辞書の索引

「コンビネータ計算の非決定性」の関連用語

コンビネータ計算の非決定性のお隣キーワード
検索ランキング

   

英語⇒日本語
日本語⇒英語
   



コンビネータ計算の非決定性のページの著作権
Weblio 辞書 情報提供元は 参加元一覧 にて確認できます。

   
ウィキペディアウィキペディア
Text is available under GNU Free Documentation License (GFDL).
Weblio辞書に掲載されている「ウィキペディア小見出し辞書」の記事は、Wikipediaのコンビネータ論理 (改訂履歴)の記事を複製、再配布したものにあたり、GNU Free Documentation Licenseというライセンスの下で提供されています。

©2025 GRAS Group, Inc.RSS