論理型言語#

パラダイム

教科書2.4章

講義1回分

序論#

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

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

1. \(\forall X \neg human(X) \vee mortal(X)\)等．

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

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

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

1. 現在の深層学習ベースではなく，探索と推論ベースの人工知能のこと．エキスパートシステムとも呼ばれる．

論理型言語の利用例#

論理型言語の利用のイメージを紹介する．具体的な処理内容や実現方法は一切考えないようにせよ．題材として徳川将軍家の家系図を採り上げる．

まず，プログラマが徳川家の家系図を何らかの方法を使って機械に入力する．以下は入力される情報の一例である．

• 徳川家の家祖は家康である
• 信康は家康の長男である
• 亀姫は家康の長女である
• 秀忠は家康の三男である
• ...

ユーザはこの機械に対して質問を行い，その回答を得る．

Q. 徳川家の家祖は家康ですか？
A. そうです．
Q. 家康の子供は誰ですか？
A. 信康と亀姫と秀忠と...です．
Q. 秀忠の母親は誰ですか？
A. 西郷局です．

さらにプログラマが江戸幕府に関する情報を入力しておけば，以下のような質問も可能になる．

Q. 江戸幕府の将軍は誰ですか？
A. 家康と秀忠と...です．
Q. 江戸幕府は何代まで続きましたか？
A. 15代です．徳川慶喜が大政奉還を行い終焉を迎えました．

このように様々な事実を機械に与えることで人工的な知能を得る，という考えが論理型言語の目指していたビジョンである．

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へ入力する質問は単一の述語である．

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

先の例ではmortal(socrates).が質問である．「ソクラテスは死ぬ」という命題は真か，という問いだと解釈せよ．

例題1：最大公約数#

最大公約数gcd/3を題材に，述語定義を説明する．gcd/3は述語gcdが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に対して最大公約数が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) :- A > 0, R is B mod A, gcd(R, A, C).#

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

1. 厳密には代入ではなくisという述語（RとB mod Aの関係）である．

gcd(8, 12, X)の計算は次のように行われる．→は式展開や実行結果である．解説のための要素である．

?- gcd(8, 12, X) % 8>0，Rは4，gcd(4, 8, X)を再帰的に推論
 → gcd(4, 8, X)  % 4>0，Rは0，gcd(0, 4, X)を再帰的に推論
 → gcd(0, 4, X)  % Aは0なので規則は不成立だが事実gcd(0, B, B)が成立
 → X = 4

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

単一化#

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

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

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

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

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

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

% Prologへの質問　　            成否          | Prologの出力
?- 1 = 1.                   % 成功 (R1)     | true.
?- X = 1.                   % 成功 (R2)     | X = 1.
?- X = A.                   % 成功 (R3)     | X = A.
?- p(1) = p(1).             % 成功 (R4->R1) | true.
?- p(X) = p(1).             % 成功 (R4->R2) | X = 1.

?- 2 = 3.                   % 失敗 (R1)     | false.
?- socrates = aristoteles.  % 失敗 (R1)     | false.
?- p(X) = r(X).             % 失敗 (R4)     | false.
?- p(X) = p(1, 2).          % 失敗 (R4)     | false.
?- p(2) = p(3).             % 失敗 (R4->R1) | false.

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

?- p(X, r(Y)) = p(A, r(3)). % 成功          | X = A, Y = 3.
?- p(Z, r(Z)) = p(A, r(3)). % 成功          | Z = A, A = 3.

?- p(X, Y, Z) = p(A, B, C).
?- p(X, Y, Z) = p(A, A, A).
?- p(X, 2, X) = p(5, A, A).

?- p(X, Y, Z) = p(A, B, C).  % 成功 | X = A, Y = B, Z = C
?- p(X, Y, Z) = p(A, A, A).  % 成功 | X = A, Y = A, Z = A
?- p(X, 2, X) = p(5, A, A).  % 失敗 | false.
   % ↑   ↖  ↖
   % X=5 A=2 5=2
   % ok  ok  ng

Prologは内部処理のトレースも可能である．質問に対して，単一化が繰り返されていることが確認できる．

gcd(8, 12, X)の内部処理は以下の通りである．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)は自分自身の述語を利用しているため，再帰呼び出し構造となっていることが見て取れる．CallとExitは常に同数である．

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, X)は「8と12の最大公約数がX」という結論を仮定し，事実や規則からその結論が真であるかを単一化によって推論している．真の場合は真となる条件X=4が出力される．

?- 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.  % カットに到達すると別解の探索はできない

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

?- sum(10, X). % 1～10までの合計は?
X = 55.

sum/2の定義は次の通り．

sum(0, 0).
sum(N, T) :- Ns is N - 1, sum(Ns, Ts), T is Ts + N.

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

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

カットを導入することで無限ループを回避できる．事実に単一化したならそれ以降の探索は不要である．

sum(0, 0) :- !.
sum(N, T) :- Ns is N - 1, sum(Ns, Ts), T is Ts + N.

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

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

sum(0, 0) :- !.
sum(N, T) :- N > 0, Ns is N - 1, sum(Ns, Ts), T is Ts + N.

例題2：家系図#

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

[親の親]      [親]      [子]

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

parent(maximilian, tom).  % maximilianはtomの親
parent(wilhelmina, tom).  % 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はtomの子である（＝tomの子は誰か？）
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はtomの母親である（＝tomの母親は誰か？）
X = wilhelmina.

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

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

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

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

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

• adaだけでなくtom自身も婚姻関係にあると判断されてしまう
• 答えが3回繰り返されている

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

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

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

2つ目の問題はバックトラックによるものである．「同じ子を共有する」という論理式だと子供の数だけ導出ができる．以下に示すような子供の数パターンの単一化ルートがあるためである．

• adaはtomと子harryを共有する．つまりadaはtomと婚姻関係だ．
• adaはtomと子jasonを共有する．つまりadaはtomと婚姻関係だ．
• adaはtomと子carlaを共有する．つまりadaはtomと婚姻関係だ．

このような場合はカットを導入すれば良い．婚姻関係を持つ相手は常に一人だと定義する．

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

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

まとめ#

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

《宿題》#

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(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, !.

% grandmother(GM, C) :- ???
% sister(S, X) :- ???

?-
bagof(C, child(C, tom), L1),
bagof(F, father(F, tom), L2),
bagof(W, married(tom, W), L3)

?-
bagof(GM, grandmother(GM, harry), L4)

?-
bagof(S, sister(S, harry), L5)

# Q1
L1 = [harry, jason, carla],
???

# Q2
grandmother(GM, C) :- ???

# Q3
sister(S, X) :- ???