論理プログラミング

論理型プログラミング（Logic Programming）は、古典論理学の述語論理を基礎にしたプログラミング手法である。人工知能の研究を主な目的にして始められた分野である。パターンマッチングを基軸にしたプログラムコード実行順序の選択決定が特徴である。アルゴリズムを論理式（論理和・論理含意・論理積・同値・否定）の組み合わせで宣言的に記述し、節形式（冠頭・スコーレム・連言標準形）で並べられた原子論理式間のユニフィケーションとバックトラッキングの反復と再帰により手続き的に計算して求められた解答を導出するという、失敗による否定と非決定性を枠組みにしたパラダイムである。論理型プログラミングは数々の応用的サブパラダイムに分類されて研究されている。

1972年に初公開された「Prolog」が論理型プログラミング言語の代表と見なされている。Prologはホーン節による宣言的記述と、SLD導出による手続き的計算を特徴にしている。Prologを中心にした論理型プログラミングの基礎は、論理学者ロバート・コワルスキが1979年に上梓した『Logic for Problem Solving』でほぼ完成されて現在に到るまで引き継がれている。

詳細は「Prolog 」を参照

特徴

論理型プログラミングは、手続き型/関数型/オブジェクト指向とは一線を画している独特な書式を持つ。本稿では論理型言語の代表とされるPrologベースのものを扱う。概形を掴むためにまず書式の見本例を以下に示す。

canfly(X) :- bird(X), not abnormal(X).
abnormal(X) :- wounded(X).
bird(john).
bird(mary).
wounded(john).

?- canfly(X).  これがプログラムの起点になり（目標節）飛べるものを挙げよという質問になる

「?-」はコマンドプロンプトであり、そのcanfly(X)で実行開始される。(1)目標節のcanfly(X)は一行目のcanfly(X)とマッチする。(2)その含意先のbird(X)は三行目のbird(john)とマッチしてbird(X=john)になる。(3)一行目のabnormal(X=john)は二行目のabnormal(X)とマッチする。(4)その含意先のwounded(X=john)は五行目のwounded(john)とマッチするので一行目のnotで偽になり反駁される。(5)ここでバックトラックされてXが白紙化される。(6)一行目のbird(X)は四行目のbird(mary)とマッチしてbird(X=mary)になる。(7)abnormal(X=mary)は反駁されるが、notで真になるので非反駁=成立になる。(8)一行目のcanfly(X=mary)が成立して目標節もcanfly(X=mary)となり、飛べるものはmaryという解が得られる。

節形式

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

   H :-  B1, ..., Bn.

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

   B1 and ... and Bn 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 :-  Body1.
     ....
     H :-  Bodyk.

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

     H iff (Body1 or ... or Bodyk)

ここで、iff は同値（if and only if）を意味する。完全性を主張するには、等号と等号に関する公理を明確にする必要もある。完全性は非単調推論のためのマッカーシーのサーカムスクリプションや閉世界仮説に密接に関連する。

歴史

LISPとadvice taker

論理型プログラミングのルーツは、関数型プログラミングのそれと同様に、1958年にマサチューセッツ工科大学の計算機科学者ジョン・マッカーシーが開発したプログラミング言語「LISP」にまで求めることができる。LISP開発の主な動機は人工知能の研究であった。マッカーシーはLISP公開当初の設計を、記号式の再帰関数群とそれらの計算（Recursive Functions of Symbolic Expressions and Their Computation by Machine）という題目で説明している。同じく1958年にマッカーシーは、人工知能のキーポイントとなる常識推論（commonsense reasoning）の実現に向けたプログラミングパラダイム仮説も発表している。advice takerと題された以下の仮説は、論理型プログラミングの原型構想と言えるものであった。

述語論理に似た適切な形式言語を扱うプログラムは共通知識的有用ステートメントになる。プログラムとは前提リストから率直に結論を導き出せるものである。その結論は命令的判決または宣言的判決のどちらかになる。命令的判決ではそれに応じた機器操作も行われる。我々がadvice takerに期待するもの―それは最小限のステートメントで最大限の有用性が得られることである。ステートメントは最小限の知識定義しか要求しない。advice takerは保有知識と与えられたヒントから論理的に解答できる。解答は公式知識に基づく常識推論に沿ったものである。従って我々はこう言える。プログラムはcommon senseを備えていると。

clauseとresolutionの考案、Absysの発表

マッカーシーは現在の論理型プログラミングの姿に繋がるアイディアを直接出すことはなかった。彼の人工知能研究はあくまでLISPの発展を通したものであり、彼がLISPに導入したパターンマッチング、関数の再帰、シンボル型、アトムといった機能は、論理型言語の基礎になっている。1965年頃に当時スタンフォード大学在籍の計算機科学者コーデル・グリーンが、原子論理式を連ねた節形式のプログラム書式を初めて発表した。グリーンは節形式を解釈するための導出手法（resolution）も考案し、双方を合わせた宣言的言語はLISPの試験的方言として実装されている。グリーンの導出手法は数学者ジョン・ロビンソンが考案していた命題導出を参考にしていた。AI目的のLISP方言が考案されていく中で、1967年のアバディーン大学で現在の論理型プログラミングに近いものを意識した初めての言語に位置付けられている「Absys」が発表された。Absysでは失敗による否定、リストを形成する集約演算子、束縛変数リセットのバックトラックなどの機能が導入されていた。

宣言的表現 vs 手続き的表現

Plannerの開発

これに対して、当時MITに在籍していたマービン・ミンスキーとシーモア・パパートは、彼とは異なる手続き的手法の開発を主導した。より一般的に受け入られている狭い意味での論理プログラミングは、述語論理式を非決定的なプログラミング言語とみなすもので、述語論理式は宣言的であると同時に手続き的にも解釈される。論理をベースにしたプログラミング言語として1971年に Planner のサブセットである Micro-Planner が開発された。表明とゴールからパターンによる手続き的計画を呼び出す機能を備えていたが、十分に形式化されていなかった。Planner が開発されたとき、これら2つの手法の関係に関する疑問が生まれていた。Robert Kowalski は「計算は推論に包含される」という命題を生み出した。彼はこれを 1988年の Pat Hayes の論文にあった言葉「計算は制御された推論である」が元になっているとしている。

Prologの開発

Plannerと独立してより論理を重視した Prolog が開発され、コワルスキーにより述語論理式(ホーン節)のプログラム的解釈の考え方と結び付き、論理プログラミングの基本的な考え方が確立した。最初に実装された Prolog処理系は1972年に開発された Marseille Prolog である。Prolog が実用的なプログラミング言語として使われるきっかけとなったのは 1977年にエジンバラで David Warren がコンパイラ処理系を開発したことであった。Edinburgh Prolog は他の記号処理言語（Lispなど）と処理速度を比較して遜色ない性能であることを世に示した。Edinburgh Prolog はデファクトスタンダードとなり、後の ISO での Prolog 標準化に影響を与えた。

他方でコワルスキやヘイズとは逆に、カール・ヒューイットは「論理的推論はオープンシステムの並行計算を実行することが不可能だ」という命題を生み出した。論理的手法と手続き的手法の関係という問題の答えは、手続き的手法の数学的意味（表示的意味論）と論理の数学的意味（モデル理論）は異なる、ということである。また、Planner からの派生でプログラミング言語 Poplerが開発された。

Prolog からの派生言語としては、Mercury、Visual Prolog、Oz、Fril などがある。バックトラッキングを使用しない並行論理プログラミング言語としてProlog からの派生したConcurrent Prolog、PARLOG、GHC、KL1などの各種言語（Shapiro [1989] に調査結果がある）がある。

論理型プログラミングの派生

並行論理

詳細は「並行論理プログラミング 」を参照

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

制約論理

詳細は「制約論理プログラミング 」を参照

並行制約論理

詳細は「並行制約プログラミング 」を参照

並行論理プログラミングは制約論理プログラミングと結び付き、制約で並行実行を制御する並行制約プログラミングとして統合され、 Saraswatらにより理論化が行われた。KahnとSaraswatは並行制約プログラミングの枠内での制約の設定でアクターモデルが実現できることから、アクターモデルは並行制約プログラミングの特別なケースだと主張した。

従来の拡張およびマイナー派生分野

高階論理

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

適用分野

エキスパートシステム

特定応用分野の巨大なモデルから、推奨や回答を生成するプログラム

自動定理証明

既存の理論から新たな定理を生成するプログラム

関連項目

• 古典論理学
• 形式手法
• 宣言型プログラミング
• 関数型プログラミング

参考文献

• Alain Colmerauer and Philippe Roussel, ’The birth of Prolog', in The second ACM SIGPLAN conference on History of programming languages, p. 37-52, 1992.
• 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.
• Kenneth Kahn, and Viyaj Saraswat, Actors as a Special Case of Concurrent Constraint Programming, Xerox Technical Report, 1990.

外部リンク

• Logic Programming Virtual Library entry
• Bibliographies on Logic Programming
• Association for Logic Programming (ALP)
• Theory and Practice of Logic Programming journal
• Logic programming in Oz