人工知能的論理プログラミング(9) - エレファント・ビジュアライザー調査記録

論理プログラミング調査

Prolog の動作を説明しようとしたとき、正しく説明できているかどうかわかりにくいという問題があります。また、自分が考えている説明が正しいのかどうかもよくわかりません。この問題を解決するために、モノイドを使って説明することを考えます。

「Prolog のプログラムを論理式とみなして、論理積が作るモノイドを使って Prolog の動作を説明してください」と ChatGPT で入力すると、答えはやってほしいことと違うし、漠然としたものでした。説明するのが難しくて聞いているのでこれ以上説明するのは難しいのですが、少し詳しく書いてみることにします。少なくともモノイドの構成要素は書いたほうが良いようです。

「Prolog の動作は、ゴールの『述語の項』とHorn節をユニフィケーションにより組み合わせて、『述語の項』の論理積に変換するものと考えることができます。

この一回の動作によって、『述語の項』の論理積の各『述語の項』を『述語の項』の論理積に変換することができます。この結果は『述語の項』の論理積となります。これはモノイドのある元を別の元に変換するものと考えることができます。

この動作を繰り返すことによって、最終的に単位元に一致したとき、プログラムは終了します。

この動作をモノイドの考え方を使ってわかりやすく説明してください。」
と入力しましたが、答えはあまりわかりやすくありませんでした。もう少し詳しく書いてみることにしました。

以下のように入力しました。

『述語の項』の全体を $T$ とおきます。 $T$ で自由生成されたモノイドを $M$ とおきます。
『一つのHorn節』による『一回の変換』を表す $T$ から $M$ への写像を $f$ とおきます。 $f$ は生成元について定義されているので $M$ に拡張することができます。この $M$ から $M$ への写像も $f$ で表します。
この写像を $M$ から $P(M)$ への写像とみなしたものを $g$ とおきます。( $P(M)$ は $M$ のべき集合) $g$ の像はユニフィケーションが成功したものだけとします。(または『代入』による整合性があるものすべてとします) ユニフィケーションが失敗したときは空集合とします。(または false だけの集合とします)
『Horn節』は複数あるため、すべての『Horn節』に対して『一回の変換』を行うことを表す $P(M)$ から $P(M)$ への写像 $h$ が存在します。( $h$ はすべての『Horn節』に対する $g$ の像の和集合を得る )
$h$ を $P(M)$ から $P(M)$ への写像とみなしたものを $p$ とおきます。
ゴールの『述語の項』から始めて、 $p$ を繰り返して得られた像の中に単位元が存在すればプログラムは終了します。

この動作をモノイドを使って説明してください。

以下のような答えが返ってきました。

この問題をモノイドの観点から説明するために、以下のように定義と説明を整理します。

定義と前提条件

1. $T$ ：述語の項の全体集合。
2. $M$ ： $T$ から自由生成されたモノイド。
3. $f$ ： $T$ から $M$ への写像で、一つの Horn節による一回の変換を表すもの。

$f : T \to M$

$f$ は $M$ へ拡張可能。

4. $g$ ： $f$ を $M$ から $P(M)$ への写像とみなしたもの。ユニフィケーションが成功した場合にのみ像を持つ。

$g : M \to P(M)$

5. $h$ ：すべての Horn 節に対する $g$ の像の和集合を取る $P(M)$ から $P(M)$ への写像。

$h : P(M) \to P(M)$

6. $p$ ： $h$ を $P(M)$ から $P(M)$ への写像とみなしたもの。

モノイドを用いた Prolog の動作

Prolog プログラムにおけるゴール解決をモノイドの構造と写像の観点から説明します。

初期状態

初期ゴールを表す述語の項 $G$ が与えられます。これは $M$ の元と考えることができます。

変換の繰り返し

1. $f$ の適用：

$f$ は述語の項 $t$ に対して、一つの Horn 節を用いて変換を行います。これは述語の項 $t$ を新たな述語の項 $m$ に変換する操作です。

2. $g$ の適用：

$g$ は $f$ を $M$ から $P(M)$ への写像として拡張したものです。述語の項 $t$ に対して、ユニフィケーションが成功した場合のみ、その変換結果の集合を返します。失敗した場合は空集合を返します。

3. $h$ の適用：

$h$ はすべての Horn 節に対する $g$ の像の和集合を取ります。これは、述語の項の集合に対して、すべての Horn 節による一回の変換を適用する操作です。

4. $p$ の適用

$p$ は $h$ を $P(M)$ から $P(M)$ への写像としたもので、複数の Horn 節に対して繰り返し変換を行うプロセスを表します。

プログラムの終了

初期ゴール $G$ から始めて、 $p$ を繰り返し適用します。

各ステップで、現在のゴール集合 $S \subseteq M$ に対して $p$ を適用し、新たなゴール集合 $S' \subseteq P(M)$ を得ます。

このプロセスを繰り返すことで、ゴール集合が更新されていきます。

もし、ある時点でゴール集合 $S$ に単位元（真、true）が含まれる場合、その時点でプログラムは成功し終了します。

逆に、繰り返し適用しても単位元が得られない場合、プログラムは失敗と見なされます。
具体例での動作

次に具体的な例を用いて、上記の操作をモノイドの視点から見てみます。
例：プログラムとゴール
p(X) :- q(X), r(X).
q(a).
r(a).
ゴール: $?- p(X)$
1. 初期状態:

初期ゴール $G = p(X)$ をモノイド $M$ の元とみなします。

2. $f$ の適用:

ゴール $p(X)$ に対して、Horn 節 $p(X) \leftarrow q(X), r(X)$ を適用し、 $p(X) \to q(X) ∧ r(X)$ に変換します。

これは $f(p(X)) = q(X) ∧ r(X)$ です。

3. $g$ の適用:

$g$ はこの変換結果を $P(M)$ の元として扱います。

4. $h$ の適用:

$h$ は、すべての Horn 節に対して適用されるため、ゴールが複数の述語の項に展開されます。

この場合、 $h(p(X)) = \{ q(a), r(a) \}$ になります。

5. $p$ の適用:

新たなゴール集合 $\{ q(a), r(a) \}$ に対して、さらに $h$ を適用します。

$q(a)$ と $r(a)$ は事実としてプログラムに含まれているため、それぞれのユニフィケーションは成功し、単位元 true に一致します。

6. 終了条件の確認:

ゴール集合に単位元 true が含まれるため、プログラムは成功し終了します。
まとめ

このように、Prolog の動作をモノイドの観点から説明すると、ゴールの変換過程を写像 $f$ や $g$ 、それを拡張した $h$ や $p$ を用いて体系的に理解することができます。最終的に、単位元（真、true）に到達することを目指してゴールを変換し続けるプロセスが、Prolog のゴール解決のメカニズムです。

「この処理を行うプログラムを書いてください」と入力すると以下のような答えが返ってきました。

from typing import List, Tuple, Set, Dict, Union

# 述語の項を表すクラス
class Term:
    def __init__(self, name: str, args: List[Union[str, 'Term']] = []):
        self.name = name
        self.args = args
    
    def __eq__(self, other):
        return isinstance(other, Term) and self.name == other.name and self.args == other.args
    
    def __hash__(self):
        return hash((self.name, tuple(self.args)))
    
    def __repr__(self):
        if self.args:
            return f"{self.name}({', '.join(map(str, self.args))})"
        else:
            return self.name

# Horn節を表すクラス
class HornClause:
    def __init__(self, head: Term, body: List[Term]):
        self.head = head
        self.body = body
    
    def __repr__(self):
        return f"{self.head} :- {', '.join(map(str, self.body))}"

# ユニフィケーションを行う関数
def unify(term1: Term, term2: Term, subst: Dict[str, Term] = {}) -> Union[Dict[str, Term], None]:
    if term1 == term2:
        return subst
    elif isinstance(term1, str):
        return unify_var(term1, term2, subst)
    elif isinstance(term2, str):
        return unify_var(term2, term1, subst)
    elif isinstance(term1, Term) and isinstance(term2, Term):
        if term1.name != term2.name or len(term1.args) != len(term2.args):
            return None
        for arg1, arg2 in zip(term1.args, term2.args):
            subst = unify(arg1, arg2, subst)
            if subst is None:
                return None
        return subst
    return None

def unify_var(var: str, term: Term, subst: Dict[str, Term]) -> Union[Dict[str, Term], None]:
    if var in subst:
        return unify(subst[var], term, subst)
    elif term in subst:
        return unify(var, subst[term], subst)
    else:
        subst[var] = term
        return subst

# Horn節を適用する関数
def apply_horn_clause(clause: HornClause, goal: Term) -> Union[List[Term], None]:
    subst = unify(clause.head, goal)
    if subst is not None:
        return [substitute(term, subst) for term in clause.body]
    return None

def substitute(term: Term, subst: Dict[str, Term]) -> Term:
    if isinstance(term, str):
        return subst.get(term, term)
    elif isinstance(term, Term):
        return Term(term.name, [substitute(arg, subst) for arg in term.args])
    return term

# Prologのゴール解決のメインループ
def resolve_goals(clauses: List[HornClause], goals: List[Term]) -> bool:
    while goals:
        goal = goals.pop(0)
        new_goals = []
        for clause in clauses:
            result = apply_horn_clause(clause, goal)
            if result is not None:
                new_goals.extend(result)
        if not new_goals:
            return False
        goals.extend(new_goals)
    return True

# 述語の項とHorn節の定義
clauses = [
    HornClause(Term("p", ["X"]), [Term("q", ["X"]), Term("r", ["X"])]),
    HornClause(Term("q", ["a"]), []),
    HornClause(Term("r", ["a"]), [])
]

# 初期ゴール
goals = [Term("p", ["X"])]

# ゴール解決の実行
result = resolve_goals(clauses, goals)
print("Success" if result else "Failure")

これはちゃんと動いているかどうかわかりませんし、モノイドを使っているかどうかもわからないので、これを元に改善していきたいと思います。