論理型言語#

パラダイム

教科書2.4章

講義1回分

序論#

%%{init: {'flowchart': {'curve': 'linear', 'nodeSpacing': 40, 'rankSpacing': 40, 'padding': 5}}}%%
graph TD
  classDef focus stroke-width:4px
  パラダイム --> 命令型;
  パラダイム --> 宣言型;
  命令型 -->|ほぼ同義| 手続き型;
  命令型 --> オブジェクト指向;
  宣言型 --> 関数型;
  宣言型 --> 論理型;
  論理型:::focus;

論理型は宣言型パラダイムの一種であり，関数型と同様に手続きを記述しない．関数型の基本は関数の組み合わせであったが，論理型では論理式の組み合わせによってプログラムを表現する．数理論理学（特に一階述語論理）を理論的背景とする言語である．

本ページでは論理型言語Prologを中心に説明を進め，数理論理学としての説明は最小限に留める．分かりやすさを優先するためである．理論的側面や形式的側面よりも，プログラミング言語的な側面を中心に説明すると言い換えても良い．

関数型言語Lispと同様，Prologにも様々な処理系が存在しており組み込み関数等の微妙な差異がある．ここではSWI-Prologを用いる．サンプルプログラムを実行する際は注意せよ．オンラインのPrologコンパイラとしては One Compilerや Tutorials Pointを利用すると良い．

なお，論理型言語は1950年頃の人工知能分野(1)で用いられていたが現在ではほとんど使われていない．現代のプログラミング言語を深く理解するために，過去の言語を学んでいると考えよ．

1. 現在の深層学習ベースではなく，探索と推論ベースの人工知能のこと．

Prologによる三段論法#

まずは古典的な三段論法を題材に，Prologによる論理式の表現とその実行方法を説明する．プログラムの構文や用語は後述するので，論理型言語の雰囲気を掴み取ると良い．

以下は古典的な三段論法である．

• 大前提：全ての人間は死ぬ
• 小前提：ソクラテスは人間である
• 結論　：ゆえにソクラテスは死ぬ

大前提と小前提は既知の事実であり，簡単な論理式であるといえる(1)．このような2つの事実から結論を導く推論が三段論法である．

1. 述語論理では大前提はこのように記述する．\(\forall X \neg human(X) \vee mortal(X)\)

Prologでは大前提と小前提のような事実（論理式）をProlog処理系に与え，利用者が質問することでその処理結果，すなわち質問結果を得る．上記の論理式はPrologでは次のように記述される．

mortal(X) :- human(X).  % 全ての人間は死ぬ
human(socrates).        % ソクラテスは人間である

大文字で始まるXは変数，小文字で始まるsocratesは定数である．全ての論理式は常に.で終了する．mortal(X) :- human(X)は，任意のXが人間であるなら死ぬという論理式を表している．human(socrates)はsocratesが人間であるという論理式を表す．括弧の中が主語で，括弧の外の文字が述語（主語の動作や性質）だと考えると良い．

上記の事実をPrologに与え，以下のような質問を入力すると対応する答えが得られる．

?- mortal(socrates).  % ソクラテスは死ぬか？
true.
?- mortal(X).         % 死ぬのは誰か？
X = socrates.

?-Prolog処理系が吐き出す文字列であり，プログラマが入力する文字列ではない．ここで質問を受け付ける，という記号だと認識せよ．mortal(socrates)が質問であり，「ソクラテスは死ぬか？」という質問を意味している．これは命題が真であるかという問いに対応する．Prolog処理系はこの質問に対して既知の事実からの推論を試みる．最終的に質問の答えtrueが得られる．

さらにmortal(X)という質問をすると，この質問の答えを満たすXを表示する．この例では世界にはソクラテスしか存在していないため，答えは唯一である．もし論理式にアリストテレスを追加した場合は，

mortal(X) :- human(X).  % 全ての人間は死ぬ
human(socrates).        % ソクラテスは人間である
human(aristoteles).     % アリストテレスは人間である

複数の回答を得ることもできる．

?- mortal(X).
X = socrates ;       % まずはソクラテス，タブを押すと次の解を探す
X = aristoteles.     % アリストテレスも死ぬ

論理型言語は，論理式に基づいて推論を試みる言語である．

mortal(X) :- human(X).  % 全ての人間は死ぬ
human(socrates).        % ソクラテスは人間である
human(aristoteles).     % アリストテレスは人間である

?- human(socrates).
?- human(X).
?- human(platon).
?- mortal(platon).

?- human(socrates).
true.                % 推論すら不要でtrue
?- human(X).
X = socrates ;       % ソクラテスは人である（タブを押すと次の解へ）
X = aristoteles.     % アリストテレスも人である
?- human(platon).
false.               % プラトンが人かは分からない（知らない）
?- mortal(platon).
false.               % プラトンが死ぬかは分からない（知らない）

構文規則と用語#

Prologの構文規則をBNFを用いて説明する．ある程度簡単化している点に注意せよ．

Prologに与える論理式は節（clause）という単位で与えられる．命令型言語における文とほぼ同義である．節は事実（fact）と規則（rule）の2種類がある．

<節>　 ::= <事実> | <規則> ;
<事実> ::= <ヘッド>. ;
<規則> ::= <ヘッド> :- <ボディ>. ;

事実は常に真となる論理式であり，先の例の場合はhuman(socrates).が該当する．常に真であるためボディ部分は持たない．規則は特定の条件下で真となる論理式であり，mortal(X) :- human(X).が該当する．事実は以下のように記述することもできる．事実は恒真の規則，すなわち特殊な規則であるといえる．

human(socrates).          % 事実
human(socrates) :- true.  % 規則（上と等価）

ヘッドとボディは述語で構成される．

<ヘッド> ::= <述語> ;
<ボディ> ::= <述語> {, <述語>}* ; // (1)!
<述語>　 ::= <述語名>(<項> {, <項>}*) ;
<項>　　 ::= <変数> | <定数> | <数値> | <項> <演算子> <項> ... ;

1. {...}*は...の0回以上の繰り返し．

ヘッドは単一の述語であり，ボディは,で区切られた1個以上の述語である．述語（predicate）とは項（term）の間に成り立つ関係のことであり，真偽値を取る論理式である．述語はPrologにおける最も重要な構成要素である．簡単な述語の例を示す．

項は変数や定数などで構成される．変数は大文字で始まる文字列である（X等）．定数（アトムとも呼ばれる）は小文字で始まる文字列である（socrates等）．変数と定数はPrologの計算において厳密に区別されるため，大文字・小文字には気をつけること．

ボディに述語を複数記述した場合は，それら複数の述語が論理積andで接続されているとみなされる．例えば，father(F, C) :- parent(F, C), male(F).のボディ部分は父親という述語が真となる条件を示している．FがCの父親であるためには，FがCの親であり，Fが男である必要がある．2つの述語parent()とmale()がandで接続されている．

また同じヘッドを持つ述語を複数定義した場合は，それらは論理和orの関係を取る．先の例においてhuman(socrates). human(aristoteles).は この2名の哲学者がそれぞれ独立に人であることを示している．基本的に，述語は複数の規則の論理和で定義されることが多い．

Prologへ入力する質問は単一の述語である．

<質問> ::= <述語>. ;

最大公約数#

最大公約数gcd/3を題材に，述語定義を説明する．gcd/3は3つの引数を取る述語という意味である．Prologの文化である．gcd(A, B, C)はAとBの最大公約数Cを算出（推論）する論理式である．gcd/3への質問の例を以下に示す．

?- gcd(8, 12, X).
X = 4.

gcd/3は1つの事実と1つの規則によって定義される．

gcd(0, B, B).  % 事実
gcd(A, B, C) :- A > 0, R is B mod A, gcd(R, A, C).  % 規則

事実gcd(0, B, B)： Aが0のときに，全てのBに対して最大公約数CがBと同値になることを示している．つまりgcd(0, B, B)は常に真を返す．例えば，0と8の最大公約数は8であり，gcd(0, 8, 8)は真である．

以下のように書き換えることもできる．

gcd(0, B, B).
gcd(A, B, C) :- A = 0, B = C.  % 上と等価

規則gcd(A, B, C)：以下3つの述語のandで構成されており，どれか一つでも偽であればgcd(A, B, C)は偽となる．

• A > 0：単にAが正の整数という条件である．
• R is B mod A：常に真となる式であり，余りRがB mod Aと同じであるという関係を表している．Rへの代入のような振る舞いだとみなすこともできるが，厳密には代入ではなくisという述語（RとB mod Aの関係）である．この条件を満たすRを用いて，3つ目の述語gcd(R, A, C)が定義される．
• gcd(R, A, C)：これにより再帰的な推論が行われる．

  ?- gcd(8, 12, X) % 質問
   → gcd(4, 8, X)  % R=4，gcd(R, A, C)を再帰的に推論
   → gcd(0, 4, X)  % R=0，gcd(R, A, C)を再帰的に推論
   → X=4           % A=0なので，事実gcd(0, B, B)が成り立つ
  

構文規則を用いることで事実と規則の記述が可能となった．ただし，これらは単なる論理の集合（データ）であり，このデータからどのように質問に答えるかがProlog理解において重要である．次節ではProlog内部での推論処理を説明する．

導出と単一化#

プログラマが与えた事実や規則に基づいて，Prologは自動的に推論を実行して結果を返す．このときの操作は，与えられた述語を等価な別の述語に変換して，簡単化する操作である．この簡単化を導出（resolution）と呼ぶ．Prologでは単一化（unification）を導出の基本操作としている．ここでは導出，特に単一化の流れについて説明する．

単一化のルール#

単一化は，直感的には述語や項を矛盾が生じないように変換する操作である．単一化を試みて正しく変換できる場合もあれば，失敗する場合もある．失敗する場合は別の論理式が成立するかを探す．

単一化はx = yという式で表される．\(x\)と\(y\)は変数・定数・述語のいずれかの要素を取る記号である．x = yは2つの要素\(x\)と\(y\)の単一化を試みよ，という命令だと解釈すると良い．

単一化は以下のようなルールで実施される．いずれも\(x\)と\(y\)を入れ替えてもよい．

• R1. \(x\)が定数・\(y\)が定数：等しければ成功，異なれば失敗
• R2. \(x\)が変数・\(y\)が定数：常に成功する．変数\(x\)を値\(y\)で置き換える（具体化する）
• R3. \(x\)が変数・\(y\)が変数：常に成功する．変数\(x\)を変数\(y\)に置き換える
• R4. \(x\)が述語・\(y\)が述語：以下の全ての条件を満たせば成功して置き換える
  • 同じ述語名で引数の数が同じ
  • 各引数の単一化が成功
• 上記以外は失敗

単一化の具体例を以下に示す．Prolog上では質問の代わりに単一化を直接指示することもできる．

% Prologへの質問　　            成否          | Prologの出力
?- 1 = 1.                   % 成功 (R1)     | true.
?- X = 1.                   % 成功 (R2)     | X = 1.
?- X = A.                   % 成功 (R3)     | X = A.
?- f(1) = f(1).             % 成功 (R4->R1) | true.
?- f(X) = f(1).             % 成功 (R4->R2) | X = 1.
?- 2 = 3.                   % 失敗 (R1)     | false.
?- socrates = aristoteles.  % 失敗 (R1)     | false.
?- f(X) = g(X).             % 失敗 (R4)     | false.
?- f(X) = f(1, 2).          % 失敗 (R4)     | false.
?- f(2) = f(3).             % 失敗 (R4->R1) | false.

?- f(X, Y) = f(A, 3).       % 成功          | X = A, Y = 3.
?- f(X, X) = f(A, 3).       % 成功          | X = A, A = 3.
?- f(X, X) = f(1, 3).       % 失敗          | false.

?- f(X, g(Y)) = f(A, g(3)). % 成功          | X = A, Y = 3.
?- f(X, g(X)) = f(A, g(3)). % 成功          | X = A, A = 3.

f(X, Y, Z) = f(A, B, C).
f(X, 2, X) = f(5, A, A).

f(X, Y, Z) = f(A, B, C).  % 成功 | X = A, Y = B, Z = C
f(X, 2, X) = f(5, A, A).  % 失敗 | false.
% ↑  ↖   ↖
% x=5 A=2 X=A(5=2)なのでfail

Prologには個々の処理のトレースも可能である．質問に対して，単一化が繰り返されていることが確認できる．creepは這いずり回るという意味である．

[trace] ?- gcd(8, 12, X).               % 単一化先の述語 | A  B  C  R
   Call: (12) gcd(8, 12, _254) ? creep  % gcd(A,B,C)   | 8 12  ?
   Call: (13) 8>0 ? creep               % A>0          | 8 12  ?
   Exit: (13) 8>0 ? creep               %              | 8 12  ?
   Call: (13) _3186 is 12 mod 8 ? creep % R is B mod A | 8 12  ?  ?
   Exit: (13) 4 is 12 mod 8 ? creep     %              | 8 12  ?  4
   Call: (13) gcd(4, 8, _254) ? creep   % gcd(R,A,C)   | 8 12  ?  4
                                        % gcd(A,B,C)   | 4  8  ?
   Call: (14) 4>0 ? creep               % A>0          | 4  8  ?
   Exit: (14) 4>0 ? creep               %              | 4  8  ?
   Call: (14) _7248 is 8 mod 4 ? creep  % R is B mod A | 4  8  ?  ?
   Exit: (14) 0 is 8 mod 4 ? creep      %              | 4  8  ?  0
   Call: (14) gcd(0, 4, _254) ? creep   % gcd(R,A,C)   | 4  8  ?  0
                                        % gcd(0,B,B)   | 0  4
   Exit: (14) gcd(0, 4, 4) ? creep      %              | 0  4
   Exit: (13) gcd(4, 8, 4) ? creep      %              | 4  8  4
   Exit: (12) gcd(8, 12, 4) ? creep     %              | 8 12  4
X = 4 ;

規則gcd(A, B, C)は自分自身の述語を利用しているため，再帰呼び出し構造となっていることが見て取れる．

a = 1
b = a * 2.0
c = str(5)

print(type(a))  # <class 'int'>
print(type(b))  # <class 'float'>
print(type(c))  # <class 'str'>

単一化はゴール節を起点とした，特殊なパターンマッチングだとみなすこともできる．これは目標から前提に向かって推論を行う後ろ向き推論法（backward reasoning）の一つである．事前に結論を仮定し，それが正しいかを推論していく方法である．

?- gcd(8, 12, 5).
?- gcd(8, 12, 4).
?- gcd(8, X, 4).

?- gcd(8, 12, 5).
false .            % R is B mod Aの時点で述語isが不成立（5 is 4）

?- gcd(8, 12, 4).
true .             % gcd(8, 12, X)と全く同じ導出過程が適用

?- gcd(8, X, 4).
ERROR: Arguments are not sufficiently instantiated
ERROR: In:
ERROR:   [13] _7934 is _7940 mod 8

バックトラックとカット#

単一化は複数の述語候補を取る場合がある．例えば，最大公約数gcd(8, 12, X)の処理の中で発生していた gcd(0, 4, X)は事実gcd(0, B, B)だけでなく，規則gcd(A, B, C) :- ...を選ぶこともできる．導出はプログラムの先頭から試されるため，この例ではgcd(0, B, B)への単一化が優先されていた．

Prologには述語の選択をバックトラック（backtrack，後戻り）する機能がある．導出の過程で単一化に失敗，または論理式が偽となった場合は，バックトラックが発生し別の述語への単一化が自動的に行われる．また，解が正しく得られた（証明に成功した）後でも，Prolog処理系へタブを入力することで，バックトラックを発生させ別の解を探させることができる．

?- gcd(0, 4, X).
   Call: (12) gcd(0, 4, _8698) ? creep% 事実gcd(0,B,B)への単一化に成功
   Exit: (12) gcd(0, 4, 4) ? creep    % X=4が即座に得られる
X = 4 ;                               % タブを押して別の解を探させる
   Redo: (12) gcd(0, 4, _8698) ? creep% 規則gcd(A,B,C)への単一化に成功
   Call: (13) 0>0 ? creep             % A>0への単一化に成功
   Fail: (13) 0>0 ? creep             % しかしA>0が偽でありFail
   Fail: (12) gcd(0, 4, _8698) ? creep% つまり規則への単一化は失敗
false.                                % 別の解は見つからない

Prologではバックトラックを強制的に制御する方法が設けられている．最大公約数のような例では解は一択に定まるため，事実gcd(0, B, B)への単一化に成功した時点でバックトラックは不要である．このような場合にはカットと呼ばれる特殊な述語!/0を用いる．カットに到達するとそれ以降のバックトラックは発生しない．

gcd(0, B, B) :- !.  % !を追加
gcd(A, B, C) :- A > 0, R is B mod A, gcd(R, A, C).

?- gcd(0, 4, X).
   Call: (12) gcd(0, 4, _7520) ? creep
   Exit: (12) gcd(0, 4, 4) ? creep
X = 4.                             % カットされたため別解の探索はできない

カットは別解探索の打ち切りだけでなく，計算効率の改善や無限ループの回避などのために利用される．次の例sumto/2は1からNまでの合計を算出する述語である．

sumto(1, 1).    % 1～1の合計は1
sumto(N, S) :- N1 is N-1, sumto(N1, S1), S is S1+N.

?- sumto(5, X). % 1～5までの合計は?
X = 15.

この例では別解を探索させると無限ループが発生する．sumto(1, X)という述語に対して，事実と規則の両方への単一化が可能であり，規則側で無限ループが発生する．

?- sumto(5, X). % 1～5までの合計は?
X = 15 ;        % さらにタブを押して別解を探させる
ERROR: Stack limit (1.0Gb) exceeded
...

カットを導入することで無限ループを回避できる．

sumto(1, 1) :- !.
sumto(N, S) :- N1 is N-1, sumto(N1, S1), S is S1+N.

バックトラックを制御する述語として，強制的に述語を失敗させるfailも存在する．

?- sumto(-5, X). % 1～5までの合計は?
ERROR: Stack limit (1.0Gb) exceeded
...

sumto(1, 1) :- !.
sumto(N, S) :- N > 0, N1 is N-1, sumto(N1, S1), S is S1+N.

例題#

家系図に関する論理式を題材として，述語を作る方法を考える．以下のような家系図を定義する．

[親の親]      [親]      [子]

maximilian
     ├------ tom
wilhelmina    ├------┬ harry
             ada     ├ jason
                     └ carla

parent(maximilian, tom).  % マクシミリアンはトムの親
parent(wilhelmina, tom).  % ウィルヘルミナはトムの親
parent(tom, harry).
parent(tom, jason).
parent(tom, carla).
parent(ada, harry).
parent(ada, jason).
parent(ada, carla).

male(maximilian).   male(tom).   male(harry).   male(jason).
female(wilhelmina). female(ada). female(carla).

子供child/2という関係を表す述語は次のように定義できる．親parent/2の逆である．

child(C, P) :- parent(P, C).

?- child(X, tom). % Xはトムの子である
X = harry ;
X = jason ;
X = carla.

父親father/2と母親mother/2は次のとおり．性別を論理式に加えれば良い．

father(F, C) :- parent(F, C), male(F).
mother(M, C) :- parent(M, C), female(M).

?- mother(X, tom).  % Xはトムの母親である
X = wilhelmina.

同じ子供を共有している場合は結婚married/2だと定義できる(1)．

1. 現実世界は離婚や養子などより複雑な関係がありうるが，ここでは単純化する．

married(H, W) :- child(C, H), child(C, W).

?- married(tom, W).  % Wはトムと結婚の関係にある
W = tom ;            % バグ？
W = ada ;
W = tom ;            % バグ？
W = ada ;
W = tom ;            % バグ？
W = ada ;

married/2は2つの問題がある．

• 答えが3回繰り返されている
• エイダだけでなくトム自信も結婚関係にあると判断されてしまう

2つ目の問題は論理式のバグである．2項が異なるという述語\==/2を加えれば良い．

married(H, W) :- child(C, H), child(C, W), H \== W.

?- married(tom, W).  % Wはトムと結婚の関係にある
W = ada ;
W = ada ;
W = ada ;

1つ目の問題はバックトラックによるものである．「同じ子を共有する」という論理式だと子供の数だけ導出が可能である．このような場合はカットを導入すれば良い．

married(H, W) :- child(C, H), child(C, W), H \== W, !.

?- married(tom, W).  % Wはトムと結婚の関係にある
W = ada.

まとめ#

論理型言語についてPrologを用いて説明した．論理型言語では論理式の組み合わせによってプログラムを実現する．

《宿題》#

parent(maximilian, tom).  parent(wilhelmina, tom).
parent(tom, harry).       parent(ada, harry).
parent(tom, jason).       parent(ada, jason).
parent(tom, carla).       parent(ada, carla).
male(maximilian).    male(tom).   male(harry).   male(jason).
female(wilhelmina).  female(ada). female(carla).

child(C, P)   :- parent(P, C).
father(F, C)  :- parent(F, C), male(F).
mother(M, C)  :- parent(M, C), female(M).
married(H, W) :- child(C, H), child(C, W), H \== W, !.

grandfather(GF, C) :- true.  %% TODO
brother(B1, B2) :- true.     %% TODO

:- initialization(main).
main :-
 child(C, tom),          write('child       = '), write(C),  nl,
 father(F, tom),         write('father      = '), write(F),  nl,
 married(tom, W),        write('married     = '), write(W),  nl,
 grandfather(GF, harry), write('grandfather = '), write(GF), nl,
 brother(B1, harry),     write('brother     = '), write(B1), nl,
 halt.

# Q1
child       = harry
???

# Q2
grandfather(GF, C) :- ???

# Q3
brother(B1, B2) :- ???