Realizabilityとは? わかりやすく解説

実現可能性 (論理学)

(Realizability から転送)

出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2023/09/28 17:51 UTC 版)

数理論理学において実現可能性realizability)とは、構成的証明から追加情報を抽出するために使用される方法の集まりである[1]。形式理論の論理式は「実現子」(realizer)と呼ばれるオブジェクトによって「実現」され、実現子の持つ情報が論理式の真理値についての情報を提供する。実現可能性には多くのバリエーションがあり、どの論理式のクラスが研究され、どのようなオブジェクトが実現子であるかは、それらバリエーションごとに異なる。

実現可能性は、直観主義論理BHK解釈英語版の形式化と見なせる。実現可能性を考えるとき、「証明」についての観念(BHK解釈では未定義のまま)は「実現子」についての形式的な観念に置き換えられる。ほとんどのバリエーションにおいて実現可能性は、研究対象の形式体系で証明可能なステートメントはすべて実現可能であるという定理から始まる。ただし、実現子は論理式について通常、形式的証明が直接提供するよりも多くの情報を提供する。

実現可能性は、直観主義的証明可能性への洞察を与えるだけでなく、直観主義理論における選言文特性と存在文特性(英語: Disjunction and existence propertiesの証明や、プルーフマイニング[定訳なし]のように証明からプログラムの抽出のために適用できる。また、実現可能性トポス(realizability topos)を介したトポス理論とも関連している。

例:自然数による実現可能性

クリーネによるオリジナル版の実現可能性の定義は、ハイティング算術英語版の論理式の実現子として自然数を用いる。自然数 n と式 A の間の関係「nA を実現する」を、ハイティング算術の言語で定義する。 ただし以下において、順序対 (n, m) はある固定された有効な対関数を使うことで単一の数値として扱う。また、各自然数 n に対して φn はインデックス n計算可能関数(すなわち、何らかの方法で列挙された計算可能関数の列 における n 番目の関数)である。

  • 自然数 n原子論理式 s = t を実現するとは、 s = t が真であることと同値。 従って、任意の自然数は恒真な等式を実現し、また矛盾した等式を実現する自然数はない。
  • 順序対 (n, m) が論理式 を実現するとは、nA を実現して、かつ mB を実現することと同値。つまり、連言の実現子とはそれを構成する各式の実現子の対である。
  • 順序対 (n, m) が論理式 を実現するとは、n が 0 または 1 で、かつ n が 0 ならば mA を実現して、n が 1 ならば mB を実現することと同値。従って、選言の実現子はそれを構成する式のどちらかを明示的に(n で)指してその実現子を(m で)提供するものである。
  • 自然数 n が論理式 を実現するとは、A を実現する任意の m について φn(m)B を実現することと同値である。従って、含意の実現子は仮定となる式の実現子を引数に取って帰結となる式の実現子を返す計算可能関数とみなせる。
  • 順序対 (n, m) が論理式 を実現するとは、mA(n) の実現子であることと同値である。すなわち、存在文の実現子はその存在量化についての明示的な証拠を、それに裏打ちされた論理式の実現子と共に提供する。
  • 自然数 n が論理式 を実現するとは、任意の m について φn(m) が定義されていて、かつ φn(m)A(m) を実現することと同値である。従って、全称文の実現子は自然数 m に対してそれによるインスタンスの実現子を提供する計算可能関数とみなせる。

この定義により、次の定理が得られる[2]

A をハイティング算術 (HA) の文とする。HAA が証明できるならばHAA を実現するような自然数 n が存在することが証明できる。

一方で、実現されるがHAで証明可能でない論理式が存在する。この事実はローズによって初めて示された[要検証][3]

このメソッドのさらなる解析は、HAが選言文特性と存在文特性(英語: Disjunction and existence propertiesを持つことの証明に使われる[4]

  • もしHA が証明できるなら、 HAA(n) が証明できるような自然数 n が存在する。
  • HA が証明できるなら、HAA が証明できるか、またはHAB が証明できる。

その後の展開

クライゼルは、型付きラムダ計算を実現子の言語として使用する、修正実現可能性modified realizability)を導入した。修正実現可能性は、マルコフの原理英語版が直観主義論理では導き出せないことを示す 1 つの方法である。一方で、以下に示す前提の独立性の原則を構成的に正当化することができる:

.

相対的実現可能性[5]は、実数に対する計算可能な操作のような、必ずしも計算可能ではないデータ構造に対する再帰的または再帰的列挙可能な要素の直観主義的な分析である。

応用

実現可能性はプルーフマイニング[定訳なし]で使用される方法の 1 つであり、一見非構成的な数学的証明から具体的な「プログラム」を抽出する。 Coqなどのいくつかの証明支援系(英語: Proof assistantには、実現可能性を使用したプログラム抽出が実装されている。

関連項目

脚注

参考資料

  • Birkedal, Lars; van Oosten, Jaap (2002). “Relative and modified relative realizability”. Annals of Pure and Applied Logic 118: 115-132. doi:10.1016/S0168-0072(01)00122-1. ISSN 0168-0072. 
  • Kleene, S. C. (1945). “On the interpretation of intuitionistic number theory”. Journal of Symbolic Logic 10 (4): 109–124. doi:10.2307/2269016. JSTOR 2269016. 
  • Kleene, S. C. (1973). "Realizability: a retrospective survey" from Mathias, A. R. D.; Hartley Rogers (1973). Cambridge Summer School in Mathematical Logic : held in Cambridge/England, August 1–21, 1971. Berlin: Springer. ISBN 3-540-05569-X Cambridge Summer School in Mathematical Logic : held in Cambridge/England, August 1–21, 1971. Berlin: Springer. ISBN <bdi>3-540-05569-X</bdi>., pp. 95–112.
  • Kreisel G. (1959). "Interpretation of Analysis by Means of Constructive Functionals of Finite Types", in: Constructivity in Mathematics, edited by A. Heyting, North-Holland, pp. 101–128.
  • van Oosten, Jaap (2002). “Realizability: a historical essay”. Mathematical Structures in Computer Science (Cambridge University Press) 12: 239-263. doi:10.1017/S0960129502003626. ISSN 0960-1295. 
  • Rose, G. F. (1953). “Propositional calculus and realizability”. Transactions of the American Mathematical Society 75 (1): 1–19. doi:10.2307/1990776. JSTOR 1990776. 

外部リンク

  • Realizability Jaap van Oostenによる、実現可能性および関連トピックに関する論文へのリンクのコレクション。

Realizability

出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2022/03/29 08:09 UTC 版)

実現可能性」の記事における「Realizability」の解説

実現可能性 (論理学) -- 数理論理学において、形式的な証明構成的実装モデル与え手法およびその概念

※この「Realizability」の解説は、「実現可能性」の解説の一部です。
「Realizability」を含む「実現可能性」の記事については、「実現可能性」の概要を参照ください。

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


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

辞書ショートカット

すべての辞書の索引

「Realizability」の関連用語

Realizabilityのお隣キーワード
検索ランキング

   

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



Realizabilityのページの著作権
Weblio 辞書 情報提供元は 参加元一覧 にて確認できます。

   
ウィキペディアウィキペディア
All text is available under the terms of the GNU Free Documentation License.
この記事は、ウィキペディアの実現可能性 (論理学) (改訂履歴)の記事を複製、再配布したものにあたり、GNU Free Documentation Licenseというライセンスの下で提供されています。 Weblio辞書に掲載されているウィキペディアの記事も、全てGNU Free Documentation Licenseの元に提供されております。
ウィキペディアウィキペディア
Text is available under GNU Free Documentation License (GFDL).
Weblio辞書に掲載されている「ウィキペディア小見出し辞書」の記事は、Wikipediaの実現可能性 (改訂履歴)の記事を複製、再配布したものにあたり、GNU Free Documentation Licenseというライセンスの下で提供されています。

©2025 GRAS Group, Inc.RSS