コンテンツにスキップ

「論理プログラミング」の版間の差分

出典: フリー百科事典『ウィキペディア（Wikipedia）』
履歴の双方向閲覧
← 古い編集
削除された内容 追加された内容
ビジュアルウィキテキスト
More used with only one reference definition: 1 new reference and 1 new reference call.
 
(5人の利用者による、間の29版が非表示)
1行目: 1行目:
[[ファイル:Logical connectives Hasse diagram.svg|代替文=|境界|右|フレームなし|226x226ピクセル]]
{{プログラミング・パラダイム}}
{{プログラミング・パラダイム}}
'''論理プログラミング'''（Logic Programming）とは、[[数理論理学]]（記号論理学）を基礎にした[[プログラミングパラダイム]]、または[[数理論理学]]の[[コンピュータプログラミング]]への応用である。[[形式論理学|形式論理]]の[[論理式 (数学)|論理式]]を[[ソースコード]]の書式に投影することが基本になる。[[コンピュータプログラミング|プログラミング]]に適用するための幅広い解釈が加えられており、研究対象としての論理プログラミングは非常に多様である。


より一般的に受け入れられている論理プログラミングは、[[述語論理]]を基礎にし、問題領域の事実と規則を論理式モデル書式で表現して（ロジック）[[非決定性チューリングマシン|非決定性]]の[[演繹]]の[[導出原理]]を用いる（コントロール）というものである。この[[アルゴリズム]]スタイルで最も普及した論理プログラミング言語は「[[Prolog]]」である。
'''論理プログラミング'''（''Logic Programming''）は、[[述語論理]]を基礎にした[[プログラミング]]技法である。[[人工知能]]の研究を主な目的にして始められた分野である。[[パターンマッチング]]を基軸にしたプログラムコード実行順序の選択決定が特徴である。[[アルゴリズム]]を[[論理式 (数学)|論理式]]で宣言的に記述し、[[ホーン節|節形式]]で並べられた[[原子論理式]]を解釈する[[導出原理]]により手続き的に計算して求められた解答を[[推論]]するという、[[非決定性有限オートマトン|非決定性]]と[[失敗による否定]]を枠組みにした[[プログラミングパラダイム|パラダイム]]である。論理プログラミングは数々の応用的サブパラダイムに分類されて研究されている。


==概要==
1972年に初公開された「[[Prolog]]」が論理プログラミング言語の代表と見なされている。Prologは[[一階述語論理]]を背景にした[[ホーン節]]による宣言的記述と、SLD[[導出原理|導出]]による手続き的計算を特徴にしている。Prologを中心にした論理プログラミングの基礎は、{{仮リンク|ロバート・コワルスキ|en|Robert Kowalski|label=}}が1979年に上梓した『''Logic for Problem Solving』''でほぼ完成されて現在に到るまで引き継がれている。{{main|Prolog }}
論理プログラミングの基本は[[数理論理学]]のスタイルをコンピュータのプログラミングに持ち込むことにある。数学者や哲学者は論理を理論構築のツールとして選んだ。多くの問題は理論として自然に表現される。解決すべき問題とは、新たな仮説が既存の理論で説明できるかどうかを問うことと等しい。論理は問題が真か偽かを証明する方法を提供する。証明構築過程は明確であり、論理は問題に答える信頼できる方法と見なされている。論理プログラミングシステムはこの過程を自動化する。[[人工知能]]は論理プログラミングの開発に重要な影響を与えた。
==特徴==
論理プログラミングは、手続き型/関数型/オブジェクト指向とは一線を画している独特な書式を持つ。本稿では論理型言語の代表とされるPrologベースのものを扱う。なお、Prologファミリはどちらかというと変則的な手続き的導出に偏った言語なので、論理プログラミングの標準的全貌とまでは言えないのが実情である。ユニフィケーションと呼ばれるパターンマッチングと代入概念が一切無い変数束縛と再帰限定は宣言的な純粋関数型パラダイムを彷彿とさせるが、ファクトの登録/撤回という副作用の影響を全面的に受ける事になるユニフィケーションを通した変数束縛は全くの参照不透明になるのでこの点が手続き的となる。概形を掴むためにまず書式の見本例を以下に示す。
<syntaxhighlight lang="prolog" line="1">
canfly(X) :- bird(X), not(abnormal(X)).
abnormal(X) :- wounded(X).
bird(john).
bird(mary).
wounded(john).


この観点での論理プログラミングは、[[ジョン・マッカーシー]][1958]の''advice taker''の提案にまでさかのぼることができる。より一般的に受け入られている狭い意味での論理プログラミングは、述語論理式を非決定的なプログラミング言語とみなすもので、述語論理式は宣言的であると同時に手続き的にも解釈される。
?- canfly(X). %これがプログラム起点で（目標節）飛べるものを挙げよという質問になる
</syntaxhighlight>
<code>?-</code>はコマンドプロンプトであり、その<code>canfly(X)</code>で実行開始される。(1)目標節の<code>canfly(X)</code>は一行目の<code>canfly(X)</code>とマッチする。(2)その対偶先の<code>bird(X)</code>は三行目の<code>bird(john)</code>とマッチして<code>bird(X=john)</code>になる。(3)一行目の<code>abnormal(X=john)</code>は二行目の<code>abnormal(X)</code>とマッチする。(4)その対偶先の<code>wounded(X=john)</code>は五行目の<code>wounded(john)</code>とマッチするので一行目の<code>not</code>で偽になり反駁される。(5)ここで<code>bird</code>までバックトラックされて<code>X</code>が白紙化される。(6)一行目の<code>bird(X)</code>は四行目の<code>bird(mary)</code>とマッチして<code>bird(X=mary)</code>になる。(7)<code>abnormal(X=mary)</code>は反駁されるが、<code>not</code>で真になるので非反駁=成立になる。(8)一行目の<code>canfly(X=mary)</code>が成立して目標節も<code>canfly(X=mary)</code>となり、飛べるものはmaryという解が得られる。


論理をベースにしたプログラミング言語として1971年に [[Planner]] のサブセットである Micro-Planner が開発された。表明とゴールからパターンによる手続き的計画を呼び出す機能を備えていたが、十分に形式化されていなかった<ref>Alain Colmerauer and Philippe Roussel, '''The birth of Prolog'''</ref>。Plannerと独立してより論理を重視した [[Prolog]] が開発され、コワルスキーにより述語論理式([[ホーン節]])のプログラム的解釈の考え方と結び付き、論理プログラミングの基本的な考え方が確立した<ref name="#1">Robert Kowalski. '''The Early Years of Logic Programming'''</ref>。Planner からの派生で、プログラミング言語 Poplerが開発された。Prolog からの派生言語としては、Mercury、Visual Prolog、[[Oz (プログラミング言語)|Oz]]、Fril などがある。バックトラッキングを使用しない[[並行論理プログラミング]]言語としてProlog からの派生した[[Concurrent Prolog]]、[[PARLOG]]、[[Guarded Horn Clauses|GHC]]、[[KL1]]などの各種言語（Shapiro [1989] に調査結果がある）がある。
=== 節形式 ===
本稿では節形式（''clausal form''）の代表格である[[ホーン節]]（''horn clause''）を扱う。ホーン節は単位節、確定節、目標節の三種に大別される。その構文は以下のようになる。headとbodyはどちらもリテラル（[[原子論理式]]）を指す。リテラルは論理プログラミングにおける[[ステートメント|基本文]]である。1個以上のリテラルを連ねてピリオドで閉じたものが節（''clause''）となる。headはユニフィケーション対象となるリテラルであり、bodyはユニフィケーション元となるリテラルである。
<syntaxhighlight lang="prolog">
head.　　　　　　　　　　　%単位節。データまたは再帰停止条件になる
head :- body1, body2, ‥.　%確定節。body1かつbody2ならばheadという意味
?- body, ‥.　　　　　　　 %目標節。このbodyは質問になる
</syntaxhighlight>全てのリテラルは述語記号（''predicate signature''）になるので、プログラム的にはリテラル＝述語記号である。述語記号の書式は<code>述語名(引数, 引数, ‥)</code>である。述語記号が持つ引数の個数は[[アリティ]]と呼ばれる。引数は定項引数（定数）と変項引数（変数）に分かれる。述語名は関手名（''functor''）と記号名（''operator''）に分かれる。関手名は任意のアトム（文字列）になるものであり、アリティは任意個数であり、[[ユニフィケーション]]されて命題定項になるものである。記号名は、等号式（<code>=</code>,<code>≠</code>）比較式（<code><</code>, <code>></code>, <code><=</code>, <code>>=</code>）束縛式（<code>:=</code>）であり、いずれも2アリティであり、ユニフィケーションされないで命題定項になるものである。束縛式は[[論理的同値|論理同値]]と同義であり変項（変数）束縛に用いられるが、実際にはユニフィケーションで束縛を行っている関手名の糖衣構文でもある。導出元になる述語記号は、その導出前は命題変項と同義存在であり、導出後は命題定項（真または偽）になる。


'''数理論理学適用の限界'''
'''単位節'''（''unit clause''）は、1個のheadリテラルから成る。変項引数を含まないリテラルはファクトと呼ばれる。ファクトはグローバルデータと考えてよいものであり、構造体（述語名＝タグ、引数＝フィールド）とも見れるものになる。空リストや0や1といった数値の引数を持つリテラルは、ユニフィケーション再帰停止条件として使われる。'''確定節'''（''definite clause''）は、1個のheadリテラルと1個以上のbodyリテラルから成る。headとbody群は[[論理包含]]記号<code>:-</code>で繋がれる。headは論理包含の後件であり、body群は前件である。headリテラルはユニフィケーション照合対象になり、bodyの各リテラルはユニフィケーション照合元になる。headリテラルの[[対偶 (論理学)|対偶]]である各bodyリテラルの導出が全て真になると、そのheadリテラルへのユニフィケーション元のリテラルも真になって成立し、そのリテラルの変項引数への双方向性束縛も成立する。'''目標節'''（''goal clause''）は、1個以上のbodyリテラルから成る。左からのbodyリテラルがユニフィケーション元になってプログラムは実行開始される。目標節の左端記号<code>?-</code>は<code>false :-</code>の省略形であり、いかなる目標節も最終的には偽になることを意味している。これはプログラムが[[非決定性有限オートマトン|非決定性]]であり、[[閉世界仮説]]または[[背理法]]のどちらかの枠組みで実行されることを表わしている。


ジョン・マッカーシーは数理論理学をコンピュータシステムの認識論の基礎として利用することを提案した。[[マサチューセッツ工科大学|MIT]]では[[マービン・ミンスキー]]と[[シーモア・パパート]]が主導して、マッカーシーとは異なる手続き的手法が開発された。[[Planner]] が開発されたとき、これら2つの手法の関係に関する疑問が生まれた。Robert Kowalski は「計算は推論に包含される」という命題を生み出した。彼はこれを 1988年の Pat Hayes の論文にあった言葉「計算は制御された推論である」が元になっているとしている。Kowalski や Hayes とは逆に、[[カール・ヒューイット]]は「論理的推論はオープンシステムの並行計算を実行することが不可能だ」という命題を生み出した。<!-- [[計算の不確定性]]参照 -->
=== 項 ===
項（''term''）は論理プログラミングにおける情報要素である。単純項は述語記号の引数またはリストの要素の二通りの形態で存在する。単純項はいわゆる動的型付けであり型注釈といった概念は無く、数値（整数、有理数、実数）かアトム（文字列）かの区別はシステム側が自動判別する。


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


==歴史==
* 定項（''constant term''）
論理プログラミングは、1950年代から盛んになった[[自動定理証明]]と、1958年公開言語「[[LISP]]」を最初の実践手段にしている。[[マサチューセッツ工科大学]]でLISPを開発した[[ジョン・マッカーシー]]は、{{仮リンク|Advice taker|en|Advice taker|label=}}という常識[[推論エンジン|推論]]仮説を発表している。
** アトム（''atom'' ）- 文字列のこと。この世に存在するあらゆる個体（''individual''）を特定するための任意名識別子である。
** 数値（''number'' ）- 計算可能な数値。実装レベルでは整数、有理数、実数（浮動小数点）などに分化されている。
* 変項（''variable term''）
** 自由変項（''free variable'' ）- 定項が束縛されていないもの。
** 束縛変項（''bound variable'' ）- 定項が束縛されているもの。その定項と論理同値になる。
* 関数記号（''function signature'' ）- 専ら計算記号で<code>+, -, *, /, ^, √, !,</code>などである。数値を引数にし1～2アリティである。関数記号はそのまま計算後の数値と同義になる。


{{quote|適切な形式言語（述語論理計算の一部に近い）を処理するプログラムは共通の”声明書”になる。基本プログラムは前提から直ちに結論を導き出す。その結論は宣言的かもしれないし命令的かもしれない。命令的結論が導出されたら、プログラムはそれに応じた動作もする。}}
'''複合項'''（''compound term''）


[[ジョン・マッカーシー]]は更にこう補足しており、これは最初の[[人工知能]]仮説のようである。
* ファクト（''fact'' ）- 事実。引数が全て定項の関手述語。
* 述語記号（''predicate signature''）
** 関手述語（''functor predicate'' ）- アトムを述語名とするもの。
** 記号述語（''operator predicate'' ）- 等号、不等号、比較、束縛式といった記号を述語名とするもの。
** 組込命令述語（''command predicate'' ）- 各種入出力やシステムコールなどのいわゆるAPI命令。カットオペレータも指す。
* リスト（''list'' ）- 項の集合の表現体。再帰するペア要素であり<code>[term|term]</code>と書式される。termは定項、変項、リストのどれかを指し<code>|</code>で連結する。空リストは<code>[]</code>である。


{{quote|我々がadvice takerに期待する主な利点は、その記号環境と探求物についての”声明”を作成するだけで、その動作が改良されるということである。”声明”の作成には、プログラム知識やadvice takerの事前知識をほとんど要求されないだろう。advice takerは事前知識に基づく広範囲な論理的帰結を取り揃えられると仮定できる。従って次のように言える。『事前知識を豊富に与えられ、自動演繹を行うプログラムは常識を備えている』|}}
=== 導出原理 ===


なお、マッカーシーは現代で言われる論理プログラミングの形態にはそれほど関与していない。
===失敗による否定===
=== 総論 ===
==歴史==


'''宣言的知識表現と手続き的知識表現'''
=== 自動定理証明とAdvice taker ===
論理プログラミングは[[自動推論]]分野に端を発しているものであり、そのルーツは1950年代から盛んになっていた[[コンピュータ]]による[[自動定理証明]]と、1958年に[[マサチューセッツ工科大学]]（MIT）の[[ジョン・マッカーシー]]が開発したプログラミング言語「[[LISP]]」にまで遡ることが出来る。LISP誕生の背景には[[自動推論]]の発展形としての[[人工知能]]（AI）に対する研究があり、[[自動定理証明]]における[[演繹法]]（=[[導出原理]]）をより汎用的な推論アルゴリズムに拡張しようとする試みがあった。マッカーシーはLISP公開当初の設計を、記号式の再帰関数群とそれらの計算（''recursive functions of symbolic expressions and their computation by machine''）という題目で説明している。同1958年にマッカーシーは、人工知能のキーポイントとなる常識推論（''commonsense reasoning''）の実現に向けたプログラミングパラダイム仮説も発表している。{{仮リンク|Advice taker|en|Advice taker|label=}}と題された以下の仮説は、論理プログラミングの原型構想と言えるものであった。
述語論理に似た適切な形式言語を扱うプログラムは共通有用ステートメントになる。プログラムとは数々の前提から率直に結論を導き出せるものである。その結論は命令的判決または宣言的判決のどちらかになる。命令的判決ではそれに応じた機器操作も行われる。我々がadvice takerに期待するもの―それは最小限のステートメントで最大限の有用性が得られることである。ステートメントは最小限の知識定義しか要求しない。advice takerは保有知識と与えられたヒントから論理的に解答できる。解答は公式知識に基づく常識推論に沿ったものである。従って我々はこう言える。プログラムはcommon senseを備えていると。


1965年頃、[[スタンフォード大学]]の{{仮リンク|コーデル・グリーン|en|Cordell Green}}が、節形式（clausal form）のプログラムとその[[導出原理]]を考案した。これは{{仮リンク|ジョン・アラン・ロビンソン|en|John Alan Robinson}}の[[命題論理]]の[[単一化]]の[[演繹法]]を参考にしていた。1967年に[[アバディーン大学]]で開発された言語「{{仮リンク|Absys|en|Absys|label=}}」は最初期の論理プログラミングとして知られている。
=== 節形式と導出原理の確立 ===
マッカーシーは現在の論理プログラミングの姿に繋がるアイディアを直接出すことはなく、彼の[[自動推論]]＝[[人工知能]]研究はあくまでLISPの発展を通したものになった。1965年頃に当時[[スタンフォード大学]]に在籍していた{{仮リンク|コーデル・グリーン|en|Cordell Green}}が、節形式（''clausal form''）の論理式アルゴリズム書式を初めて発表した。グリーンは節形式を解釈するための[[導出原理]]（''resolution principle''）も考案し、双方を合わせた宣言的言語はLISPの試験的方言として実装されている。グリーンの導出原理は、{{仮リンク|ジョン・アラン・ロビンソン|en|John Alan Robinson}}が発表していた[[一階述語論理]]準拠の[[単一化]]を[[自動定理証明]]に組み込んだ[[命題論理]]背景の[[演繹法]]＝[[導出原理]]を参考にしていた。ここで論理的（''logical''）と手続き的（''procedual''）という典範上（''epitomize''）の対立が生まれた。自動定理証明の視点に立つロビンソンとグリーンによると、LISPのフォーム（リスト化された式）と関数再帰の多用は論理的ではない邪道（''cheating''）な手続き的であるとされ、ここから自動定理証明と人工知能研究の分岐も始まっている。人工知能研究を目的にした数々のLISP方言が考案されていく中で、1967年の[[アバディーン大学]]で現在の論理プログラミングの姿に近い初めての言語に位置付けられている「{{仮リンク|Absys|en|Absys|label=}}」が発表されている。


1960年代の論理プログラミングの進展を通して、[[数理論理学]]に忠実な[[宣言的知識|宣言的知識表現]]と、最適化アルゴリズムを取り入れる[[手続き的知識|手続き的知識表現]]のどちらを指針にするべきかという議題が提起されていた。宣言的の支持者は、[[スタンフォード大学]]と[[エディンバラ大学]]中心の{{仮リンク|ジョン・アラン・ロビンソン|en|John Alan Robinson}}、{{仮リンク|コーデル・グリーン|en|Cordell Green}}、{{仮リンク|バートラム・ラファエル|en|Bertram Raphael|label=}}、{{仮リンク|パット・ヘイズ|en|Pat Hayes|label=}}、{{仮リンク|ロバート・コワルスキ|en|Robert Kowalski|label=}}らであった。手続き的の支持者は、[[マサチューセッツ工科大学]]中心の[[マービン・ミンスキー]]、[[シーモア・パパート]]、[[カール・ヒューイット]]、[[ジェラルド・ジェイ・サスマン|ジェラルド・サスマン]]、[[テリー・ウィノグラード]]、{{仮リンク|ユージン・チャニアク|en|Eugene Charniak|label=}}らであった。
=== 宣言的表現 vs 手続き的表現 ===
1960年代を通して人工知能および論理プログラミング研究者たちの間では、宣言的表現と手続き的表現のどちらを採用するべきかという問題を巡って活発な議論が行われていた。この表現上（''representation''）の対立では、主に知識の埋込（''embedded of knowledge''）方法と[[二階述語論理]]の導入方式が対象になっていた。宣言的表現（''declarative''）を提唱したのは、[[スタンフォード大学]]と[[エディンバラ大学]]を中心にした研究者たちであり、ジョン・アラン・ロビンソン、コーデル・グリーン、{{仮リンク|バートラム・ラファエル|en|Bertram Raphael|label=}}{{仮リンク|パット・ヘイズ|en|Pat Hayes|label=}}{{仮リンク|ロバート・コワルスキ|en|Robert Kowalski|label=}}たちが名を連ねていた。それに対する手続き的表現（''procedural''）を提唱したのは、[[マービン・ミンスキー]]と[[シーモア・パパート]]が主導する[[マサチューセッツ工科大学]]在籍の研究者たちであった。宣言的表現を重視する研究者たちは[[自動定理証明]]に沿った[[論理学]]または[[数理論理学]]のアルゴリズムに忠実であることを望んでいた。手続き的表現を重視する研究者たちはプログラム実装に合わせて最適化されたアルゴリズムの導入に前向きだった。


=== Plannerの開発 ===
'''Plannerの登場'''
1969年、[[マサチューセッツ工科大学]]（MIT）の[[マービン・ミンスキー]]と[[シーモア・パパート]]が主導する研究チームの中で[[カール・ヒューイット]]が言語仕様をデザインした論理型言語「[[Planner]]」が初回稼働された。Plannerは[[メインフレーム]]運用を前提にした大規模な言語であり、画一的な定理証明手法の否定と手続き的な知識の埋め込み手法を理念にして、情報群および知識定義からの節形式への柔軟な変換表現と、[[前向き連鎖]]と[[後向き連鎖]]の双方を備えた柔軟な導出原理が実装されていた。Plannerの大規模さは運用できる環境を限定したので、1971年に[[ポータビリティ]]を重視したPlannerのサブセット版である「Micro-Planner」が、[[ジェラルド・ジェイ・サスマン|ジェラルド・サスマン]]、{{仮リンク|ユージン・チャニアク|en|Eugene Charniak|label=}}[[テリー・ウィノグラード]]らによって開発された。Micro-Plannerは主に自然言語解析に用いられて当時の著名な自然言語処理プログラムである[[SHRDLU]]を誕生させている。同時期に[[SRIインターナショナル]]の{{仮リンク|リチャード・ウォルディンガー|en|Richard Waldinger|label=}}らは、Planner処理系上で稼働する[[データマイニング]]の先駆的プログラムであるQA4を開発し、これは更に言語仕様を組み込んだ「QLISP」に拡張されて[[Interlisp]]上で実装された。


1969年、[[カール・ヒューイット]]設計の論理型言語「[[Planner]]」が[[マサチューセッツ工科大学]]で開発された。[[メインフレーム]]前提のPlannerの大規模さは運用できる環境を制限したので、1971年に[[ポータビリティ]]重視のサブセット版「Micro-Planner」が、[[ジェラルド・ジェイ・サスマン|ジェラルド・サスマン]]と[[テリー・ウィノグラード]]らによって開発された。
1971年にパパート、サスマン、チャニアク、ウォルディンガーといったMITの面々が[[エディンバラ大学]]を訪問し、彼らの成果物であるMicro-PlannerとSHRDLUを披露した。当時のエディンバラ大学は[[自動定理証明]]プロジェクト''Logic for computable functions''が始動されていた人工知能ロジック分野のメッカであった。パパートたちが披露した手続き的表現の導出原理を目の当たりにした{{仮リンク|パット・ヘイズ|en|Pat Hayes|label=}}は、[[自動定理証明]]を奉じる宣言的表現の導出原理は過去の遺物と化しているのではないかと考えるようになった。Micro-Plannerのサブセット版である「Pico-Planner」がエディンバラ大学でも直ちに実装されてその有用性が確認された。ヘイズは、自動定理証明の研究に従事していた{{仮リンク|ロバート・コワルスキ|en|Robert Kowalski|label=}}にPlannerを参考にするように勧めた。Plannerの研究を注意深く始めたコワルスキは、自身が構想していた節形式とそれに対するselective linear導出に近いものをPlannerの中に認め、ここからの着想が[[ホーン節|ホーア節]]とSLD導出の発表に繋がることになった。更にエディンバラ大学ではその価値を認めたPlannerでカバーできなかった仕様をも補完実装した論理型言語「Popler」が開発されている。


1971年、パパート、サスマン、チャニアクらの[[MIT]]勢が、[[エディンバラ大学]]を訪問してMicro-Plannerと[[SHRDLU]]を披露した。当時の同大学は、対話型[[自動定理証明]]プロジェクト「Logic for computable functions」が始動されていた論理プログラミングのメッカであった。Micro-Plannerなどを見た{{仮リンク|パット・ヘイズ|en|Pat Hayes|label=}}らは[[手続き的知識|手続き的]]の価値を認め、同大学でもMicro-Plannerのサブセット版を実装してその有用性を確認した。Plannerを研究した{{仮リンク|ロバート・コワルスキ|en|Robert Kowalski|label=}}は、[[アルフレッド・ホーン]]発案の[[ホーン節]]の論理プログラミング導入を提唱し、それへのSLD導出を考案している。更にエディンバラ大学ではPlannerのスーパーセット版「Popler」も開発された。
=== Prologの開発 ===
1971年、ロンドン開催の[[国際人工知能会議]]に出席して[[Planner]]に強い関心を抱いていた{{仮リンク|アラン・カルメラウアー|en|Alain Colmerauer|label=}}らは、{{仮リンク|ロバート・コワルスキ|en|Robert Kowalski|label=}}と[[テリー・ウィノグラード]]の両名からレクチャーを受けて、[[マルセイユ大学]]で従事していた[[自動推論]]各分野研究のための言語処理系の構築に着手した。彼らの決意は翌1972年に結実し、コワルスキが発表していた[[ホーン節]]とSLD導出を取り入れた論理プログラミング言語「[[Prolog]]」が誕生した。Prologに対する意見は分かれ、[[マサチューセッツ工科大学|MIT]]の[[カール・ヒューイット]]などはMicro-Plannerの複製品であると言及し、[[エディンバラ大学]]のコワルスキは論理プログラミングへの良いアプローチであると評した<ref>Robert Kowalski. '''The Early Years of Logic Programming'''</ref>。マルセイユ大学のカルメラウアーの下で実装された[[インタプリタ]]式の初版Prologは「Marseille Prolog」と呼ばれるようになった。Prologに注目したコワルスキの門弟である{{仮リンク|デビッド・ウォーレン|en|David H. D. Warren|label=}}がエディンバラ大学で再構築したものは「Edinburgh Prolog」と呼ばれ、よりモダン化された書式でPrologを普及させる原動力になった。ウォーレンは1977年に[[コンパイラ]]式のPrologも開発し、こちらは実装運用マシンに因んで「DEC-10 Prolog」と呼ばれ、Prolog言語仕様のスタンダードに位置付けられた。1979年、エディンバラ大学から[[インペリアル・カレッジ・ロンドン]]に移っていたコワルスキは、論理プログラミング基礎の集大成となる『''Logic for Problem Solving''』を上梓した。1983年、[[SRIインターナショナル]]に移籍していたウォーレンは、Prologコンパイラ実装のための標準処理系規範となる{{仮リンク|ウォーレン抽象マシン|en|Warren Abstract Machine|label=}}を策定してPrologの更なる普及に努めた。1986年に{{仮リンク|論理プログラミング協会|en|Association for Logic Programming|label=}}が設立され、[[ISO|IOS]]標準化に向けた準備も始められた。1987年にDEC-10 Prologの流れを汲む「{{仮リンク|SWI-Prolog|en|SWI-Prolog|label=}}」が[[アムステルダム大学]]の{{仮リンク|ジャン・ウィールメーカー|en|Jan Wielemaker|label=}}によって開発され、これが現在最も広く使われているProlog言語として知られている。


'''Prologの登場'''
1980年代の日本の[[情報工学]]分野では、[[Prolog]]を中心にした論理プログラミングに対する積極的な研究が行われていた。1970年代後半に[[SRIインターナショナル]]に留学していた日本人研究員が目にしたPrologテクノロジを、当時の[[電子技術総合研究所]]に持ち帰ったのがその発端と言われている。同研究所で[[自動推論]]部門と[[自然言語処理]]部門を担当する重職に就いていた[[渕一博]]が、Prolog系の潜在力を重要視するようになり、彼を中心にした研究グループの提案が採用されて1982年に[[新世代コンピュータ技術開発機構]]が設立された。[[第五世代コンピュータ]]（=第五世代言語）と銘打たれたそのプロジェクトの目標には、当時の欧米で取り沙汰されていた[[第四世代言語]]の更に一歩先を行くという壮大な夢が込められていた。これには約十年の歳月と総額570億円の国家予算が投入された。なお{{仮リンク|第三世代言語|en|Third-generation programming language|label=}}は[[高水準言語]]を指し、[[第四世代言語]]は現在でも明確に確立されないままだが[[ドメイン固有言語]]のサブセットとも言われる。[[第五世代コンピュータ|第五世代言語]]は[[人工知能]]準拠の総合[[処理系]]に該当し、その成就に向けて日本の研究者たちは[[述語論理]]を基礎にした[[プログラミングパラダイム]]に日本の[[情報工学]]分野の行く末を決める命運を託した。


1972年、[[マルセイユ大学]]の{{仮リンク|アラン・カルメラウアー|en|Alain Colmerauer|label=}}らは、{{仮リンク|コワルスキ|en|Robert Kowalski|label=}}らの助言を得て[[ホーン節]]とSLD導出をベースにした論理型言語「[[Prolog]]」を開発した。Prologに対する意見は分かれ、[[カール・ヒューイット]]などはMicro-Plannerの複製品であると言い、コワルスキは論理プログラミングへの良いアプローチであると評した<ref name="#1"/>。カルメラウアーの元祖版は「Marseille Prolog」と呼ばれる。コワルスキの門弟{{仮リンク|デビッド・ウォーレン|en|David H. D. Warren|label=}}の[[エディンバラ大学]]開発版は「Edinburgh Prolog」と呼ばれ、その系譜の1977年開発版「DEC-10 Prolog」がPrologの標準形になった。1979年にコワルスキは[[インペリアル・カレッジ・ロンドン]]で論理プログラミング基礎大全『''Logic for Problem Solving''』を上梓した。
==論理プログラミングの派生==
=== 並行論理 ===
{{main|並行論理プログラミング }}Keith Clark、Hervé Gallaire、Steve Gregory、Vijay Saraswat、Udi Shapiro、Kazunori Ueda（上田和紀）らは、共有変数の[[ユニフィケーション]]機能とメッセージのためのデータ構造ストリーム機能を備えた[[並行論理プログラミング]]言語を開発した。数理論理学に基づく[[並行プログラミング]]の基礎を築くための研究であるが、これが[[第五世代コンピュータ]]の基盤ともなった。


1983年、ウォーレンは[[SRIインターナショナル]]でProlog言語処理系標準モデルの{{仮リンク|ウォーレン抽象マシン|en|Warren Abstract Machine|label=}}を策定し、Prologの普及に努めた。1986年に{{仮リンク|論理プログラミング協会|en|Association for Logic Programming|label=}}が設立された。1987年にDEC-10系譜の「{{仮リンク|SWI-Prolog|en|SWI-Prolog|label=}}」が[[アムステルダム大学]]の{{仮リンク|ジャン・ウィールメーカー|en|Jan Wielemaker|label=}}によって開発され、これが現在最も使われているPrologになっている。
* [[Concurrent Prolog]]
* [[PARLOG]]
* [[Guarded Horn Clauses|GHC]]
* [[KL1]]


1980年代の日本の[[情報工学]]分野では[[Prolog]]研究が盛んに行われており、人工知能コンピュータ開発を目的にした[[第五世代コンピュータ]]計画の中心になっていた。
=== 制約論理 ===
{{main|制約論理プログラミング }}


=== 並行制約論理 ===
== 特徴 ==
{{main|並行制約プログラミング }}並行論理プログラミングは[[制約論理プログラミング]]と結び付き、制約で並行実行を制御する[[並行制約プログラミング]]として統合され、 Saraswatらにより理論化が行われた。KahnとSaraswatは並行制約プログラミングの枠内での制約の設定で[[アクターモデル]]が実現できることから、アクターモデルは並行制約プログラミングの特別なケースだと主張した<ref>Kenneth Kahn, and Viyaj Saraswat, '''Actors as a Special Case of Concurrent Constraint Programming'''</ref>。


=== 論理と制御 ===
* [[Oz (プログラミング言語)|Oz]]
論理プログラミングでは「ロジック（論理）＋コントロール（制御）＝アルゴリズム（算法）」とされている。ロジックとは、[[数理論理学]]の[[論理式 (数学)|論理式]]を特定の解釈で投影したプログラム書式表現を指す。これの代表例はファクト（事実）とルール（規則）を列挙するものであり、ルールは[[論理包含]]を主体にする。コントロールとは、そのロジックに対して、一定のファクトまたは特定のゴール（目標）を起点にした任意の問題条件を与えて、一定の解決条件を導出（resolution）することを指す。これを問題解決と言う。ロジックとコントロールの融合は、多様な[[自動定理証明|定理証明]]戦略を表現する<ref>{{cite journal|author=R.A.Kowalski|date=July 1979|title=Algorithm=Logic + Control|journal=Communications of the ACM|volume=22|issue=7|pages=424–436|doi=10.1145/359131.359136|s2cid=2509896}}</ref>。
*Fril


最も普及している[[Prolog]]系の論理プログラムで使われる[[導出原理]]は、[[論理式 (数学)|論理式]]をこれ以上解消できない所まで変形させていく[[演繹]]や簡約である。そこでのロジックは[[ホーン節]]で表現されており、コントロールにはSLD導出が使われている。
=== 仮定論理 ===
=== 帰納論理 ===


=== 問題解決 ===
=== 従来の拡張およびマイナーな派生 ===
[[ファイル:Andortree.png|サムネイル|200x200ピクセル|and-or木]]
問題解決（problem solving）とその実践の[[導出原理]]は、[[数理論理学]]の膨大な知識から様々なものが存在する。ここではシンプルなロジックの代表格の[[ホーン節]]を例にする。[[ホーン節]]は最大1個の正リテラルを持つ[[選言標準形]]をベースにしており、[[命題論理]]のホーン節は、素直に{{仮リンク|AND-OR木|en|And-or tree|label=}}に投影できる。（右図はこの説明には不向きだが、これしか無かったのであしからず）右図のAND-OR木では、最上ノードのPがゴールになり、末端ノードのT・U・R・Sはファクトになって、このように解釈できる。


<code>if Q and R then P</code>, <code>if S then P</code>, <code>if T then Q</code>, <code>if U then Q</code>.
==== 高階論理 ====
一部の研究者は[[高階述語論理]]に基づいた高階論理プログラミングへと拡張を行った（述語の変項化など）。


それへの[[導出原理]]は、ファクトから問題解決する[[前向き連鎖]]と、ゴールから問題解決する[[後向き連鎖]]に大別される。前向き連鎖は、与えられたファクトから様々な別のファクトをゴールとして解答する演繹手法である。TとRを与えるとPが解答される。Sを与えるとPが解答される。前向き連鎖は[[エキスパートシステム]]などに使われている。後向き連鎖は、与えられたゴールがファクトかどうかを解答する演繹手法である。Pを与えるとその前件のRおよびQのそのまた前件のTがファクトなのでPはファクトと解答される。後向き連鎖は論理型言語の代表[[Prolog]]に使われている。
* {{仮リンク|λProlog|en|ΛProlog}}
* HiLog


[[述語論理]]の[[ホーン節]]は、AND-OR木の各ノードが命題から述語になるので複雑になる。各ノードの述語記号の項は、定項と[[変項]]に分かれるが、定項がファクトで、変項が[[単一化]]によるファクトに束縛可能なら、そのノードは述語から命題になれる。
==== メタ論理 ====


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


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


H :- Body<sub>1</sub>.
==== トランザクション論理 ====
....
H :- Body<sub>k</sub>.


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


H iff (Body<sub>1</sub> or ... or Body<sub>k</sub>)
* Mercury


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


=== 知識表現 ===
* Visual Prolog
知識表現（knowledge representation）は、[[宣言的知識]]と[[手続き的知識]]に大別される。例えば「空から水」への知識は、宣言的では「雨」と表現され、そこから手続き的では「傘をさす」などと表現される。俗説になるが宣言的知識はintelligence、手続き的知識はwisdomとも言われる。[[Prolog]]の[[ホーン節]]と[[後向き連鎖]]のSLD導出と[[失敗による否定]]の[[非単調論理]]の論理プログラミングは、宣言的知識と手続き的知識の混合とされている。


==関連項目==
==Prolog==
{{ main|Prolog }}
*[[自動推論]]
[[Prolog]] は 1972年にマルセイユのカルメラウアーが考案し、1974年にコワルスキーがさらに形式的に定義し、数理論理学に基づいた言語として発表した。Prolog のプログラムは[[一階述語論理]]のサブセットの論理式の集まりとして読むことができ、一階述語論理のモデル理論と証明理論を継承している。プログラムの節は次のように書かれる:
*[[自動定理証明]] - 既存の理論から新たな定理を生成するプログラム

*[[自然言語処理]]
H :- B<sub>1</sub>, ..., B<sub>n</sub>.
*[[エキスパートシステム]] - 特定応用分野の巨大なモデルから、推奨や回答を生成するプログラム

*[[人工知能]]
これを宣言として読めば、以下の論理的含意に等しい：
*[[宣言型言語|宣言型プログラミング]]

B<sub>1</sub> and ... and B<sub>n</sub> implies H

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

'''Prolog の実装'''

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

== 派生分野 ==

===並行論理プログラミング===
{{ main|並行論理プログラミング }}

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

並行論理プログラミングは[[制約論理プログラミング]]と結び付き、制約で並行実行を制御する[[並行制約プログラミング]]として統合され、 Saraswatらにより理論化が行われた。KahnとSaraswatは並行制約プログラミングの枠内での制約の設定で[[アクターモデル]]が実現できることから、アクターモデルは並行制約プログラミングの特別なケースだと主張した<ref>Kenneth Kahn, and Viyaj Saraswat, '''Actors as a Special Case of Concurrent Constraint Programming'''</ref>。

* [[Concurrent Prolog]]、[[PARLOG]]、[[Guarded Horn Clauses|GHC]]、[[KL1]]
* [[Oz (プログラミング言語)|Oz]]、{{仮リンク|アリス言語|en|Alice (programming language)|label=Alice}}、{{仮リンク|ToonTalk|en|ToonTalk|label=}}

=== 制約論理プログラミング ===
{{main|制約論理プログラミング}}述語記号の項に、{{仮リンク|制約（数学）|en|Constraint (mathematics)|label=制約}}も含めるようにしている。制約（constraint）とは値（元・要素・個体）を”関係性”で表現したものであり、決定変数の集合で定義される計算対象である。

* {{仮リンク|B-Prolog|en|B-Prolog|label=}}、{{仮リンク|Ciao言語|en|Ciao (programming language)|label=Ciao}}、{{仮リンク|ECLiPSe|en|ECLiPSe|label=}}、{{仮リンク|Fril|en|Fril|label=}}

===高階論理プログラミング===
述語記号の項に、述語記号も含めるようにしている。例えば、<code>p(A, B, C) :- q(A, foo), r(B, bar), C.</code>では、Cを別個の述語記号にできる。テンプレートメタ的な書式も扱っており、例えば<code>p(A, B, C) :- (C)(A, B)</code>では、Cが述語名でAとBがその項になる。

* {{仮リンク|λProlog|en|ΛProlog}}、{{仮リンク|HiLog|en|HiLog|label=}}

=== 関数論理プログラミング ===
述語記号と関数記号の双方をリテラルにしている。

* {{仮リンク|Mercury言語|en|Mercury|label=Mercury}}、{{仮リンク|Curry (programming language)|en|Curry (programming language)|label=Curry}}

=== オブジェクト指向論理プログラミング ===
ファクトとルールをまとめた[[モジュール]]を扱っている。<code>module.predicate(A, B, C)</code>のように表記できる。モジュールは、[[オブジェクト指向]]由来の[[継承 (プログラミング)|継承]]と[[多態性]]を備えている。既存の上位モジュールを[[継承 (プログラミング)|継承]]して新規の下位モジュールを定義できる。上位モジュールの変数に下位モジュールを代入して[[サブタイピング]]するのが[[多態性]]である。例えば<code>var.predicate(A, B, C)</code>では、上位変数<code>var</code>に下位モジュールAを代入するとAの<code>predicate</code>と解釈され、同変数に下位モジュールBを代入するとBの<code>predicate</code>と解釈される。

* {{仮リンク|Visual Prolog|en|Visual Prolog}}

=== 線形論理プログラミング ===
[[線形論理]]を扱っている。

=== 帰納論理プログラミング ===
[[帰納推論]]を扱っている。これまでの[[演繹論理|演繹推論]]とは別種になる。

=== 仮説論理プログラミング ===
[[仮説的推論|仮説推論]]を扱っている。これまでの[[演繹論理|演繹推論]]とは別種になる。

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

==関連項目==
*[[数理論理学]]
*[[述語論理]]
*[[非単調論理]]
*[[導出原理]]
*[[ホーン節]]
*[[Prolog]]
*[[Planner]]
*[[第五世代コンピュータ|第五世代コンピュータ計画]]


== 脚注 ==
== 脚注 ==
173行目: 200行目:


{{プログラミング言語の関連項目}}
{{プログラミング言語の関連項目}}
{{Normdaten}}

{{DEFAULTSORT:ろんりふろくらみんく}}
{{DEFAULTSORT:ろんりふろくらみんく}}

[[Category:論理プログラミング|*]]
[[Category:論理プログラミング|*]]
[[Category:プログラミングパラダイム]]
[[Category:プログラミングパラダイム]]

2022年6月10日 (金) 22:00時点における最新版

プログラミング・パラダイム

命令型プログラミング

宣言型プログラミング

マルチパラダイム

論理プログラミング（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導出が使われている。

問題解決

[編集]
and-or木

問題解決（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 」を参照

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と解釈される。

線形論理プログラミング

[編集]

線形論理を扱っている。

帰納論理プログラミング

[編集]

帰納推論を扱っている。これまでの演繹推論とは別種になる。

仮説論理プログラミング

[編集]

仮説推論を扱っている。これまでの演繹推論とは別種になる。

適用分野

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

関連項目

[編集]

脚注

[編集]
[脚注の使い方]
  1. ^ Alain Colmerauer and Philippe Roussel, The birth of Prolog
  2. ^ a b Robert Kowalski. The Early Years of Logic Programming
  3. ^ R.A.Kowalski (July 1979). “Algorithm=Logic + Control”. Communications of the ACM 22 (7): 424–436. doi:10.1145/359131.359136. 
  4. ^ 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.

外部リンク

[編集]
コンピュータ・プログラミング言語の関連項目
言語水準
言語処理系
言語分類
その他
関連項目
「https://ja.wikipedia.org/w/index.php?title=論理プログラミング&oldid=89962034」から取得