論理プログラミング

出典: フリー百科事典『ウィキペディア（Wikipedia）』

論理プログラミング（Logic Programming）とは、表明とゴールからパターンによる手続き呼び出しを行うプログラミング手法。ジョン・マッカーシー[1958]で初めて数理論理学をプログラミングに使用することが提案された。最初の論理プログラミング言語は Planner であり、表明とゴールからパターンによる手続き的計画を呼び出す機能を備えていた。当時のメモリの少ないシステムで動作させるため。Planner はバックトラッキング制御構造を使っており、一度に1つの計算経路だけを格納しなければならなかった。その後、Planner を単純化した Prolog が開発された。これはゴールからのみパターンによる呼び出しを行う（バックトラッキングも行う）。Planner からの派生で、プログラミング言語 QA-4、Popler、Conniver、QLISP が開発された。Prolog からの派生言語としては、Mercury、Visual Prolog、Oz、Fril がある。バックトラッキングを使用しない並行論理プログラミング言語も Planner からの派生（Ether）と Prolog からの派生（Shapiro [1989] に調査結果がある）がある。

1 数理論理学的基礎
2 Prolog
- 2.1 論理プログラミングにおける否定
- 2.2 Prolog の実装
3 数理論理学のプログラミングへの利用の限界
4 並行論理プログラミング
5 高階論理プログラミング
6 適用分野
7 歴史
8 関連項目
9 参考文献
10 外部リンク

[編集] 数理論理学的基礎

論理プログラミングの基本は数理論理学のスタイルをコンピュータのプログラミングに持ち込むことにある。数学者や哲学者は論理を理論構築のツールとして選んだ。多くの問題は理論として自然に表現される。解決すべき問題とは、新たな仮説が既存の理論で説明できるかどうかを問うことと等しい。論理は問題が真か偽かを証明する方法を提供する。証明構築過程は明確であり、論理は問題に答える信頼できる方法と見なされている。論理プログラミングシステムはこの過程を自動化する。人工知能は論理プログラミングの開発に重要な影響を与えた。

[編集] Prolog

Prolog は 1972年にマルセイユのカルメラウアーが考案し、1974年にコワルスキーがさらに形式的に定義し、数理論理学に基づいた言語として発表した。Prolog のプログラムは一階述語論理のサブセットの論理式の集まりとして読むことができ、一階述語論理のモデル理論と証明理論を継承している。プログラムの節は次のように書かれる:

   H :-  B₁, ..., B_n.

これを宣言として読めば、以下の論理的含意に等しい：

   B₁ and ... and B_n implies H

ここで、節内の全変数（変項）は全称量化されている。手続き的な後方連鎖規則として見れば、H を証明するには、B₁ から B_n までを証明できれば十分であることがわかる。手続き的意味は線形導出法（LUSH または SLD導出法）による反駁証明によっても定式化できる。宣言的意味と手続き的意味の密接な関係は論理プログラミング言語の際立った特徴であるが、否定や論理和といった他の量化子をプログラム内に許すようになると関係は複雑になる。

[編集] 論理プログラミングにおける否定

論理プログラムが節 H :- B₁, ..., B_n から構成され、H, B₁, ..., B_n が全てアトミックな述語論理式であれば、このプログラムは確定(definite)していると呼ばれ、ホーン節プログラムであるともいう。確定した論理プログラムの手続き的意味と宣言的意味は、そのまま述語論理的に解釈できる。否定を含めると、古典的論理との関係はそれほど直接的ではなくなる。「失敗による否定; negation-as-failure」推論規則によれば、ゴール Q がプログラムによって証明できない場合、その否定 not(Q) は証明されたと見なされる。これは古典的論理学では全く正しくない。公理から Q も not(Q) も導けない可能性がある。結果として、この規則は論理的例外と実用的困難さをもたらした。後方連鎖証明規則に「失敗による否定」を加えても完全ではない。その場合、プログラムを宣言的に読んで得られる論理的結果の全てを証明することができない。しかし、ほとんどの Prolog 系言語は「失敗による否定」を \+ という文字列を使って実装している。

完全ではないものの、プログラムとしての完全性（completion）という意味では「失敗による否定」規則は（ある制限下で）健全な推論規則であると言える。論理プログラムの完全性は Keith Clark が最初に定義した。おおまかに言えば、それはプログラム内の左辺に同じ述語のある全節の集合である。例えば、以下のようなものである:

     H :-  Body₁.
     ....
     H :-  Body_k.

これらは次の1つの論理式と等価である。

     H iff (Body₁ or ... or Body_k)

ここで、iff は等価（if and only if）を意味する。完全性を主張するには、等号と等号に関する公理を明確にする必要もある。完全性は非単調推論のためのマッカーシーの「限定; circumscription」技法や「閉じた世界; closed world」という前提に密接に関連する。

[編集] Prolog の実装

最初に実装された Prolog処理系は1972年に開発された Marseille Prolog である。Prolog が実用的なプログラミング言語として使われるきっかけとなったのは 1977年にエジンバラで David Warren がコンパイラ処理系を開発したことであった。Edinburgh Prolog は他の記号処理言語（Lispなど）と処理速度を比較して遜色ない性能であることを世に示した。Edinburgh Prolog はデファクトスタンダードとなり、後の ISO での Prolog 標準化に影響を与えた。

[編集] 数理論理学のプログラミングへの利用の限界

ジョン・マッカーシーは数理論理学をコンピュータシステムの認識論の基礎として利用することを提案した。MITではマービン・ミンスキーとシーモア・パパートが主導して、マッカーシーとは異なる手続き的手法が開発された。Planner が開発されたとき、これら2つの手法の関係に関する疑問が生まれた。Robert Kowalski は「計算は推論に包含される」という命題を生み出した。彼はこれを 1988年の Pat Hayes の論文にあった言葉「計算は制御された推論である」が元になっているとしている。Kowalski や Hayes とは逆に、カール・ヒューイットは「論理的推論はオープンシステムの並行計算を実行することが不可能だ」という命題を生み出した。

論理的手法と手続き的手法の関係という問題の答えは、手続き的手法の数学的意味（表示的意味論）と論理の数学的意味（モデル理論）は異なる、ということである。

[編集] 並行論理プログラミング

Keith Clark、Hervé Gallaire、Steve Gregory、Vijay Saraswat、Udi Shapiro、Kazunori Ueda（上田和紀）らは、共有変数のユニフィケーション機能とメッセージのためのデータ構造ストリーム機能を備えたProlog風のメッセージパッシングシステムを開発した。数理論理学に基づく並行プログラミングの基礎を築くための研究であるが、これが第五世代コンピュータの基盤ともなった。

アクターモデルと同様、Prolog 風の並行システムはメッセージパッシングに基づいているため、同様の非決定性を内包している。このため、カール・ヒューイットや Gul Agha [1988] は Prolog 風並行システムは演繹的でも論理的でもないと主張した。

[編集] 高階論理プログラミング

一部の研究者は高階述語論理に基づいた高階論理プログラミングへと拡張を行った（述語の変項化など）。そのような言語としては Prolog の拡張である HiLog や λProlog がある。

[編集] 適用分野

エキスパートシステム: 特定応用分野の巨大なモデルから、推奨や回答を生成するプログラム
自動定理証明: 既存の理論から新たな定理を生成するプログラム

[編集] 歴史

論理プログラミングは人工知能の研究から生まれた考えであり、ジョン・マッカーシー [1958] の次の引用が確認されている最初の言明である。

「適切な形式言語（おそらく述語計算の一部）を処理するプログラムは共通の手段となる。基本プログラムは前提から直ちに結論を導き出す。その結論は宣言的かもしれないし命令的かもしれない。命令的な結論が導かれるなら、そのプログラムはその結論に対応した動作をする」

ジョン・マッカーシーは彼の提案を以下のように補足した。

「我々が advice taker に期待する主な利点は、その記号環境と探しているものについてセンテンスを入力するだけでシステムの動作が改良される点である。そのようなセンテンスを入力するにあたって、プログラムや advice taker に関する事前知識はほとんど必要としないだろう。advice taker は事前に教え込まれた知識から論理的に導き出される広範囲な能力を有していると仮定することができる。したがって、次のように言うことができるだろう。『事前知識を豊富に与えられ、自動演繹を行うプログラムは、常識を備えている』」

[編集] 関連項目

[編集] 参考文献

John McCarthy. Programs with common sense Symposium on Mechanization of Thought Processes. National Physical Laboratory. Teddington, England. 1958.
Fisher Black. A deductive question answering system Harvard University. Thesis. 1964.
James Slagle. Experiments with a Deductive Question-Answering Program CACM. December, 1965.
Cordell Green. Application of Theorem Proving to Problem Solving IJCAI 1969.
Carl Hewitt. Planner: A Language for Proving Theorems in Robots IJCAI 1969.
Gerry Sussman and Terry Winograd. Micro-planner Reference Manual AI Memo No, 203, MIT Project MAC, July 1970.
Carl Hewitt. Procedural Embedding of Knowledge In Planner IJCAI 1971.
Terry Winograd. Procedures as a Representation for Data in a Computer Program for Understanding Natural Language MIT AI TR-235. January 1971.
Bruce Anderson. Documentation for LIB PICO-PLANNER School of Artificial Intelligence, Edinburgh University. 1972
Bruce Baumgart. Micro-Planner Alternate Reference Manual Stanford AI Lab Operating Note No. 67, April 1972.
Julian Davies. Popler 1.6 Reference Manual University of Edinburgh, TPU Report No. 1, May 1973.
Jeff Rulifson, Jan Derksen, and Richard Waldinger. QA4, A Procedural Calculus for Intuitive Reasoning SRI AI Center Technical Note 73, November 1973.
Robert Kowalski Predicate Logic as a Programming Language Memo 70, Department of Artificial Intelligence, Edinburgh University. 1973.
Drew McDermott and Gerry Sussman. The Conniver Reference Manual MIT AI Memo 259A. January 1974.
Earl Sacerdoti, et al. QLISP: A Language for the Interactive Development of Complex Systems AFIPS National Computer Conference. 1976.
Bill Kornfeld and Carl Hewitt. The Scientific Community Metaphor IEEE Transactions on Systems, Man, and Cybernetics. January 1981.
Bill Kornfeld. The Use of Parallelism to Implement a Heuristic Search IJCAI 1981.
Bill Kornfeld. Parallelism in Problem Solving MIT EECS Doctoral Dissertation. August 1981.
Bill Kornfeld. Combinatorially Implosive Algorithms CACM. 1982
Carl Hewitt. The Challenge of Open Systems Byte Magazine. April 1985.
Robert Kowalski. The limitation of logic Proceedings of the 1986 ACM fourteenth annual conference on Computer science.
Ehud Shapiro (Editor). Concurrent Prolog MIT Press. 1987.
Robert Kowalski. The Early Years of Logic Programming CACM. January 1988.
Ehud Shapiro. The family of concurrent logic programming languages ACM Computing Surveys. September 1989.
Carl Hewitt and Gul Agha. Guarded Horn clause languages: are they deductive and Logical? International Conference on Fifth Generation Computer Systems, Ohmsha 1988. Tokyo. Also in Artificial Intelligence at MIT, Vol. 2. MIT Press 1991.
Shunichi Uchida and Kazuhiro Fuchi Proceedings of the FGCS Project Evaluation Workshop Institute for New Generation Computer Technology (ICOT). 1992.
Carl Hewitt. The repeated demise of logic programming and why it will be reincarnated What Went Wrong and Why: Lessons from AI Research and Applications. Technical Report SS-06-08. AAAI Press. March 2006.
J. W. Lloyd. Foundations of Logic Programming (2nd edition). Springer-Verlag 1987.

[編集] 外部リンク

"http://ja.wikipedia.org../../../%E8%AB%96/%E7%90%86/%E3%83%97/%E8%AB%96%E7%90%86%E3%83%97%E3%83%AD%E3%82%B0%E3%83%A9%E3%83%9F%E3%83%B3%E3%82%B0.html" より作成

カテゴリ: プログラミングパラダイム | 理論計算機科学 | 数理論理学