論理プログラミング
| プログラミング・パラダイム |
|---|
論理プログラミング（Logic Programming）とは、数理論理学（記号論理学）を基礎にしたプログラミングパラダイム、または数理論理学のコンピュータプログラミングへの応用である。形式論理の論理式をソースコードの書式に投影することが基本になる。プログラミングに適用するための幅広い解釈が加えられており、研究対象としての論理プログラミングは非常に多様である。
より一般的に受け入れられている論理プログラミングは、述語論理を基礎にし、問題領域の事実と規則を論理式モデル書式で表現して（ロジック）非決定性の演繹の導出原理を用いる（コントロール）というものである。このアルゴリズムスタイルで最も普及した論理プログラミング言語は「Prolog」である。
概要
[編集]論理プログラミングの基本は数理論理学のスタイルをコンピュータのプログラミングに持ち込むことにある。数学者や哲学者は論理を理論構築のツールとして選んだ。多くの問題は理論として自然に表現される。解決すべき問題とは、新たな仮説が既存の理論で説明できるかどうかを問うことと等しい。論理は問題が真か偽かを証明する方法を提供する。証明構築過程は明確であり、論理は問題に答える信頼できる方法と見なされている。論理プログラミングシステムはこの過程を自動化する。人工知能は論理プログラミングの開発に重要な影響を与えた。
この観点での論理プログラミングは、ジョン・マッカーシー[1958]のadvice takerの提案にまでさかのぼることができる。より一般的に受け入られている狭い意味での論理プログラミングは、述語論理式を非決定的なプログラミング言語とみなすもので、述語論理式は宣言的であると同時に手続き的にも解釈される。
論理をベースにしたプログラミング言語として1971年に Planner のサブセットである Micro-Planner が開発された。表明とゴールからパターンによる手続き的計画を呼び出す機能を備えていたが、十分に形式化されていなかった[1]。Plannerと独立してより論理を重視した Prolog が開発され、コワルスキーにより述語論理式(ホーン節)のプログラム的解釈の考え方と結び付き、論理プログラミングの基本的な考え方が確立した[2]。Planner からの派生で、プログラミング言語 Poplerが開発された。Prolog からの派生言語としては、Mercury、Visual Prolog、Oz、Fril などがある。バックトラッキングを使用しない並行論理プログラミング言語としてProlog からの派生したConcurrent Prolog、PARLOG、GHC、KL1などの各種言語（Shapiro [1989] に調査結果がある）がある。
数理論理学適用の限界
ジョン・マッカーシーは数理論理学をコンピュータシステムの認識論の基礎として利用することを提案した。MITではマービン・ミンスキーとシーモア・パパートが主導して、マッカーシーとは異なる手続き的手法が開発された。Planner が開発されたとき、これら2つの手法の関係に関する疑問が生まれた。Robert Kowalski は「計算は推論に包含される」という命題を生み出した。彼はこれを 1988年の Pat Hayes の論文にあった言葉「計算は制御された推論である」が元になっているとしている。Kowalski や Hayes とは逆に、カール・ヒューイットは「論理的推論はオープンシステムの並行計算を実行することが不可能だ」という命題を生み出した。
論理的手法と手続き的手法の関係という問題の答えは、手続き的手法の数学的意味（表示的意味論）と論理の数学的意味（モデル理論）は異なる、ということである。
歴史
[編集]論理プログラミングは、1950年代から盛んになった自動定理証明と、1958年公開言語「LISP」を最初の実践手段にしている。マサチューセッツ工科大学でLISPを開発したジョン・マッカーシーは、Advice takerという常識推論仮説を発表している。
適切な形式言語（述語論理計算の一部に近い）を処理するプログラムは共通の”声明書”になる。基本プログラムは前提から直ちに結論を導き出す。その結論は宣言的かもしれないし命令的かもしれない。命令的結論が導出されたら、プログラムはそれに応じた動作もする。
ジョン・マッカーシーは更にこう補足しており、これは最初の人工知能仮説のようである。
我々がadvice takerに期待する主な利点は、その記号環境と探求物についての”声明”を作成するだけで、その動作が改良されるということである。”声明”の作成には、プログラム知識やadvice takerの事前知識をほとんど要求されないだろう。advice takerは事前知識に基づく広範囲な論理的帰結を取り揃えられると仮定できる。従って次のように言える。『事前知識を豊富に与えられ、自動演繹を行うプログラムは常識を備えている』
なお、マッカーシーは現代で言われる論理プログラミングの形態にはそれほど関与していない。
宣言的知識表現と手続き的知識表現
1965年頃、スタンフォード大学のコーデル・グリーンが、節形式（clausal form）のプログラムとその導出原理を考案した。これはジョン・アラン・ロビンソンの命題論理の単一化の演繹法を参考にしていた。1967年にアバディーン大学で開発された言語「Absys」は最初期の論理プログラミングとして知られている。
1960年代の論理プログラミングの進展を通して、数理論理学に忠実な宣言的知識表現と、最適化アルゴリズムを取り入れる手続き的知識表現のどちらを指針にするべきかという議題が提起されていた。宣言的の支持者は、スタンフォード大学とエディンバラ大学中心のジョン・アラン・ロビンソン、コーデル・グリーン、バートラム・ラファエル、パット・ヘイズ、ロバート・コワルスキらであった。手続き的の支持者は、マサチューセッツ工科大学中心のマービン・ミンスキー、シーモア・パパート、カール・ヒューイット、ジェラルド・サスマン、テリー・ウィノグラード、ユージン・チャニアクらであった。
Plannerの登場
1969年、カール・ヒューイット設計の論理型言語「Planner」がマサチューセッツ工科大学で開発された。メインフレーム前提のPlannerの大規模さは運用できる環境を制限したので、1971年にポータビリティ重視のサブセット版「Micro-Planner」が、ジェラルド・サスマンとテリー・ウィノグラードらによって開発された。
1971年、パパート、サスマン、チャニアクらのMIT勢が、エディンバラ大学を訪問してMicro-PlannerとSHRDLUを披露した。当時の同大学は、対話型自動定理証明プロジェクト「Logic for computable functions」が始動されていた論理プログラミングのメッカであった。Micro-Plannerなどを見たパット・ヘイズらは手続き的の価値を認め、同大学でもMicro-Plannerのサブセット版を実装してその有用性を確認した。Plannerを研究したロバート・コワルスキは、アルフレッド・ホーン発案のホーン節の論理プログラミング導入を提唱し、それへのSLD導出を考案している。更にエディンバラ大学ではPlannerのスーパーセット版「Popler」も開発された。
Prologの登場
1972年、マルセイユ大学のアラン・カルメラウアーらは、コワルスキらの助言を得てホーン節とSLD導出をベースにした論理型言語「Prolog」を開発した。Prologに対する意見は分かれ、カール・ヒューイットなどはMicro-Plannerの複製品であると言い、コワルスキは論理プログラミングへの良いアプローチであると評した[2]。カルメラウアーの元祖版は「Marseille Prolog」と呼ばれる。コワルスキの門弟デビッド・ウォーレンのエディンバラ大学開発版は「Edinburgh Prolog」と呼ばれ、その系譜の1977年開発版「DEC-10 Prolog」がPrologの標準形になった。1979年にコワルスキはインペリアル・カレッジ・ロンドンで論理プログラミング基礎大全『Logic for Problem Solving』を上梓した。
1983年、ウォーレンはSRIインターナショナルでProlog言語処理系標準モデルのウォーレン抽象マシンを策定し、Prologの普及に努めた。1986年に論理プログラミング協会が設立された。1987年にDEC-10系譜の「SWI-Prolog」がアムステルダム大学のジャン・ウィールメーカーによって開発され、これが現在最も使われているPrologになっている。
1980年代の日本の情報工学分野ではProlog研究が盛んに行われており、人工知能コンピュータ開発を目的にした第五世代コンピュータ計画の中心になっていた。
特徴
[編集]論理と制御
[編集]論理プログラミングでは「ロジック（論理）＋コントロール（制御）＝アルゴリズム（算法）」とされている。ロジックとは、数理論理学の論理式を特定の解釈で投影したプログラム書式表現を指す。これの代表例はファクト（事実）とルール（規則）を列挙するものであり、ルールは論理包含を主体にする。コントロールとは、そのロジックに対して、一定のファクトまたは特定のゴール（目標）を起点にした任意の問題条件を与えて、一定の解決条件を導出（resolution）することを指す。これを問題解決と言う。ロジックとコントロールの融合は、多様な定理証明戦略を表現する[3]。
最も普及しているProlog系の論理プログラムで使われる導出原理は、論理式をこれ以上解消できない所まで変形させていく演繹や簡約である。そこでのロジックはホーン節で表現されており、コントロールにはSLD導出が使われている。
問題解決
[編集]
問題解決（problem solving）とその実践の導出原理は、数理論理学の膨大な知識から様々なものが存在する。ここではシンプルなロジックの代表格のホーン節を例にする。ホーン節は最大1個の正リテラルを持つ選言標準形をベースにしており、命題論理のホーン節は、素直にAND-OR木に投影できる。（右図はこの説明には不向きだが、これしか無かったのであしからず）右図のAND-OR木では、最上ノードのPがゴールになり、末端ノードのT・U・R・Sはファクトになって、このように解釈できる。
if Q and R then P, if S then P, if T then Q, if U then Q.
それへの導出原理は、ファクトから問題解決する前向き連鎖と、ゴールから問題解決する後向き連鎖に大別される。前向き連鎖は、与えられたファクトから様々な別のファクトをゴールとして解答する演繹手法である。TとRを与えるとPが解答される。Sを与えるとPが解答される。前向き連鎖はエキスパートシステムなどに使われている。後向き連鎖は、与えられたゴールがファクトかどうかを解答する演繹手法である。Pを与えるとその前件のRおよびQのそのまた前件のTがファクトなのでPはファクトと解答される。後向き連鎖は論理型言語の代表Prologに使われている。
述語論理のホーン節は、AND-OR木の各ノードが命題から述語になるので複雑になる。各ノードの述語記号の項は、定項と変項に分かれるが、定項がファクトで、変項が単一化によるファクトに束縛可能なら、そのノードは述語から命題になれる。
失敗による否定
[編集]論理プログラムが節 H :- B1, ..., Bn から構成され、H, B1, ..., Bn が全てアトミックな述語論理式であれば、このプログラムは確定(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）を意味する。完全性を主張するには、等号と等号に関する公理を明確にする必要もある。完全性は非単調推論のためのマッカーシーのサーカムスクリプションや閉世界仮説に密接に関連する。
知識表現
[編集]知識表現（knowledge representation）は、宣言的知識と手続き的知識に大別される。例えば「空から水」への知識は、宣言的では「雨」と表現され、そこから手続き的では「傘をさす」などと表現される。俗説になるが宣言的知識はintelligence、手続き的知識はwisdomとも言われる。Prologのホーン節と後向き連鎖のSLD導出と失敗による否定の非単調論理の論理プログラミングは、宣言的知識と手続き的知識の混合とされている。
Prolog
[編集]Prolog は 1972年にマルセイユのカルメラウアーが考案し、1974年にコワルスキーがさらに形式的に定義し、数理論理学に基づいた言語として発表した。Prolog のプログラムは一階述語論理のサブセットの論理式の集まりとして読むことができ、一階述語論理のモデル理論と証明理論を継承している。プログラムの節は次のように書かれる:
H :- B1, ..., Bn.
これを宣言として読めば、以下の論理的含意に等しい：
B1 and ... and Bn implies H
ここで、節内の全変数（変項）は全称量化されている。手続き的な後方連鎖規則として見れば、H を証明するには、B1 から Bn までを証明できれば十分であることがわかる。手続き的意味は線形導出法（LUSH または SLD導出法）による反駁証明によっても定式化できる。宣言的意味と手続き的意味の密接な関係は論理プログラミング言語の際立った特徴であるが、否定や論理和といった他の量化子をプログラム内に許すようになると関係は複雑になる。
Prolog の実装
最初に実装された Prolog処理系は1972年に開発された Marseille Prolog である。Prolog が実用的なプログラミング言語として使われるきっかけとなったのは 1977年にエジンバラで David Warren がコンパイラ処理系を開発したことであった。Edinburgh Prolog は他の記号処理言語（Lispなど）と処理速度を比較して遜色ない性能であることを世に示した。Edinburgh Prolog はデファクトスタンダードとなり、後の ISO での Prolog 標準化に影響を与えた。
派生分野
[編集]並行論理プログラミング
[編集]Keith Clark、Hervé Gallaire、Steve Gregory、Vijay Saraswat、Udi Shapiro、Kazunori Ueda（上田和紀）らは、共有変数のユニフィケーション機能とメッセージのためのデータ構造ストリーム機能を備えた並行論理プログラミング言語を開発した。数理論理学に基づく並行プログラミングの基礎を築くための研究であるが、これが第五世代コンピュータの基盤ともなった。
並行論理プログラミングは制約論理プログラミングと結び付き、制約で並行実行を制御する並行制約プログラミングとして統合され、 Saraswatらにより理論化が行われた。KahnとSaraswatは並行制約プログラミングの枠内での制約の設定でアクターモデルが実現できることから、アクターモデルは並行制約プログラミングの特別なケースだと主張した[4]。
制約論理プログラミング
[編集]述語記号の項に、制約も含めるようにしている。制約（constraint）とは値（元・要素・個体）を”関係性”で表現したものであり、決定変数の集合で定義される計算対象である。
高階論理プログラミング
[編集]述語記号の項に、述語記号も含めるようにしている。例えば、p(A, B, C) :- q(A, foo), r(B, bar), C.では、Cを別個の述語記号にできる。テンプレートメタ的な書式も扱っており、例えばp(A, B, C) :- (C)(A, B)では、Cが述語名でAとBがその項になる。
関数論理プログラミング
[編集]述語記号と関数記号の双方をリテラルにしている。
オブジェクト指向論理プログラミング
[編集]ファクトとルールをまとめたモジュールを扱っている。module.predicate(A, B, C)のように表記できる。モジュールは、オブジェクト指向由来の継承と多態性を備えている。既存の上位モジュールを継承して新規の下位モジュールを定義できる。上位モジュールの変数に下位モジュールを代入してサブタイピングするのが多態性である。例えばvar.predicate(A, B, C)では、上位変数varに下位モジュールAを代入するとAのpredicateと解釈され、同変数に下位モジュールBを代入するとBのpredicateと解釈される。
線形論理プログラミング
[編集]線形論理を扱っている。
帰納論理プログラミング
[編集]仮説論理プログラミング
[編集]適用分野
[編集]- エキスパートシステム
- 特定応用分野の巨大なモデルから、推奨や回答を生成するプログラム
- 自動定理証明
- 既存の理論から新たな定理を生成するプログラム
関連項目
[編集]脚注
[編集]- ^ Alain Colmerauer and Philippe Roussel, The birth of Prolog
- ^ a b Robert Kowalski. The Early Years of Logic Programming
- ^ R.A.Kowalski (July 1979). “Algorithm=Logic Control”. Communications of the ACM 22 (7): 424–436. doi:10.1145/359131.359136.
- ^ Kenneth Kahn, and Viyaj Saraswat, Actors as a Special Case of Concurrent Constraint Programming
参考文献
[編集]- 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.
