Entries

スポンサーサイト
[EDIT]
上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

-件のコメント

コメントの投稿

新規
非公開にする

-件のトラックバック

トラックバックURL
http://harukazehajime.blog115.fc2.com/tb.php/139-b7aa60ea
この記事に対してトラックバックを送信する(FC2ブログユーザー)
論理プログラミング
[EDIT]
OCamlの記事の途中ですが、溜めに溜めたデータをすべて吹っ飛ばしてしまったので、気力が帰ってくるまでほかの記事を、ということで論理プログラミングについて書きながら待つことにします(^^;
最近記事も重くなってきてますし、ちょっと気分転換というか(笑)
論理プログラミングに関する知識はほとんどないので、間違いなどあったら指摘していただければと思います。

論理プログラミングは数理論理学をプログラミングに取り入れ、さらに人工知能と密接に関わっているため、関数型言語以上に異質な存在に映るでしょう。
ある仮説・問題(=命題)について、すでに証明された問題(=定理・前提)で証明できるかをプログラミングで行うということが論理プログラミングの背景にあります。

例えば、コンピュータによって証明された有名な問題として、
ある図形について「隣り合った図形同士は同じ色にならない」という条件の下、できる限り少ない色数で図形を塗り分けるには「4色あれば十分」
という「4色問題」があります。これは過去の経験則から導き出された「5色で塗り分けられる」という前提が活用されました。

論理プログラミングは命題と定理の関係を記述するのに利用されます。例えば「AとはBとCである」とか、「CはDかEの何れかである」といったことを記述するわけですね。
この二つの前提から、「AはDかEの何れかである。これはAがCと等しいからである」ということが導き出せます。命題を証明したり、新しい解を導き出したりするのは自動です。
もうちょっと具体的な例を、論理プログラミング言語の代表格であるPrologのソースコードとともに挙げてみます。

まずは先ほどの例をプログラミングしてみましょう。%のうしろはコメントになります。
%AとはBとCである
a :- b, c.
%CはDかEの何れかである
c :- d.
c :- e.
:- の左辺を頭部(命題)、右辺を本体(すでに証明された命題)と呼びます。
実際のところは関数型言語のように、それぞれの項に付随する情報を書き加えることが多いです。
cat(tama). %tamaはcatである
cat(tom). %tomもcatである
pet(X) :- cat(X) %catはpetである。Xは変数である
ここでPrologに対して、タマはペットかどうか質問してみます。
?- pet(tama).
Yes
Prologがpetはcatであり、catがtamaと結びつけられているかどうかを判断してYesと答えます。つまり逆説的に答えを導き出したことになります。論理プログラミングは「本体がすべて真であれば頭部は真である」という解釈をするため、この辿りかたが普通になります。
今度はペットに誰がいるかを答えさせてみます。
?- pet(X).
X=tama
pet(X)を満たすcat(X)を導き出し、さらにcat(X)を満たす項を見つけてタマを変数Xに代入しました。
一般的なプログラミング言語ではここで終わってしまうでしょう。でもトムもこの条件を満たします。この問題に対応できるよう、論理プログラミングは複数の答えを導き出すことができます。
X=tamaで止まっているところでセミコロンを入力すると、次の答えを導き出します。
X=tama;
X=tom
ほかの答を求める機能を「バックトラック」、複数の答を持ちえることを「非決定性」といいます。

バックトラックについては「やりなおし」という意味合いがあって、先ほどの例では
pet(X)はcat(X)であり、cat(X)を満たすのは最初に見つかるcat(tama)である
でバックトラックを行うとcat(tama)を答えから取り除いて、もういちどcat(X)を満たす項を探してcat(tom)に辿り着いた、という形になります。
Prologは木という表現でデータを保持し、答えを探しています。数学にある木と同じと考えても差し支えありません。
→ pet(X)
 |
cat(X)
/ \
cat(tama) cat(tom)
pet(X)という入力があると、pet(X) = cat(X)であることから矢印が左に移動します。
pet(X)
 |
 → cat(X)
/ \
cat(tama) cat(tom)
さらにcat(X) = cat(tama) or cat(tom)であり、木の辿り方は左に近い方からというルールから、さらに左に移動し、末端であることから答えとして出力します。
pet(X)
 |
  cat(X)
/ \
→ cat(tama) cat(tom)
ここでバックトラックを行うと選択肢からcat(tama)を取り除いて、矢印は一旦上に戻ります。
pet(X)
 |
 → cat(X)
/ \
  cat(tom)
再びcat(X)を満たすものを探し、cat(tom)に辿り着きます。
pet(X)
 |
  cat(X)
/ \
   → cat(tom)
この状態でさらにバックトラックを行うと答えがなくなります。答がなくなってもエラーとしてプログラムを止めることはなく、答が見つからないと表示してユーザの入力を待ちます。

論理プログラミングにおけるもうひとつの重要な機能がユニフィケーションと呼ばれるものです。ユニフィケーションは先ほどの木構造の探索や入力とソースコードの比較、変数への代入など、論理プログラミングを成り立たせるほとんどの処理を行います。ユニフィケーションは次のようなルールの下で処理を行っていきます。
1. 入力された項と定義された項において、項の片方が変数でもう一方が変数でない場合、変数はもう一方の項と同一と見なす(変数への代入)
2. 同様にそれぞれの項において項の両方が変数ならば、両方の変数は同一と見なす
3. それぞれの項がアトム(変数でないもの)の場合、それぞれが完全に一致した場合に成功する
4. それぞれの項が複合項(f(A)という形式)で、引数(括弧の中。アリティという)が同じ形式である場合、すべての要素で1~4のユニフィケーションが成功する場合に成功する

member(X, [X|_]). % Xがリストの先頭要素と同じ場合
member(X, [_|Y]) :- member(X, Y) % それ以外の場合
この定義に対して次のように質問してみます。
?- member(Z, [tama,tom]).
Z=tama
変数Zにtamaが代入されました。

まずひとつめの定義member(X, [X|_])において、入力member(Z, [tama, tom])との関係は
・ZはXと同じものである………ユニフィケーション2
・Xと[tama, tom]についてはXを[tama, tom]とみなす………ユニフィケーション1
・入力と定義は複合項でアリティは互いに変数とリストである………ユニフィケーション4
 - 変数Zと変数Xは同一………ユニフィケーション1
 - リスト[X|_]とリスト[tama, tom]は互いにリストというアトムである………ユニフィケーション3
 - リスト[X|_]とリスト[tama, tom]はX=tama, _=tom………ユニフィケーション2
・アリティの全要素が満されるから複合項もtrueである………ユニフィケーション4が成功
・変数 _ は捨てて、これまでのユニフィケーションの結果からZ=tamaである
という結論に至り出力します。この状態でバックトラックを行うと
・member([X|_])の項から探査木を一段戻る
・ユニフィケーションが成功する次の頭部を探す
 - member(X, [_|Y])とmember(Z, [tama, tom])でユニフィケーションに成功
 - [_|Y]と[tama, tom]は_=tama, Y=tomで、変数 _ は捨てる………ユニフィケーション1
 - 本体がmember(X, Y)であり、_ が捨てられたmember(Z, [tom])とユニフィケーションに成功
・この結果を引き継いでmember(X, [X|_])とmember(Z, [tom])をユニフィケーション
・X=Zで、[X|_]と[tom]はX=tom, _=nil………ユニフィケーション1
・_ を捨ててX=tom、X=ZよりZ=tomである

論理プログラミングに込み入った条件に見合った答えを導き出す機能を付け加えたのが制約論理プログラミングで、制約プログラミングの始祖です。
論理プログラミングの根本的な制約は「ユニフィケーションできるか」だけで、それ以外の制約を付け加えるために制約プログラミングが考案されたということができます。
関連記事

0件のコメント

コメントの投稿

新規
非公開にする

0件のトラックバック

トラックバックURL
http://harukazehajime.blog115.fc2.com/tb.php/139-b7aa60ea
この記事に対してトラックバックを送信する(FC2ブログユーザー)

Appendix

プロフィール

さくらゆーな

Author:さくらゆーな
鉄道熱が再燃して、撮影に模型にいろいろやってます。
最近反核運動に偏ってるのを反省したいけど
知れば知るほど極悪非道な界隈で止まらない…

カレンダー

07 | 2017/08 | 09
- - 1 2 3 4 5
6 7 8 9 10 11 12
13 14 15 16 17 18 19
20 21 22 23 24 25 26
27 28 29 30 31 - -

+ アーカイブ
 

最近の記事

カテゴリー

検索フォーム


キーワード

カウンター

トータルカウンター
現在の閲覧者数:

ads3

Mac ソフトのことなら act2.com

Make a donate

もしこのブログを気に入っていただけたら上記アフィリエイトプログラムか下のPayPalでブログ・サイトの維持にご協力ください。

donationPrice

ブロとも申請フォーム

この人とブロともになる

ブログランク

上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。