人工知能的代数学(15) - エレファント・ビジュアライザー調査記録

モノイドの左逆元・右逆元(4)

いったんプログラムの説明を書いて、その説明を元に説明を書いてもらうことにします。

変数の全体 $V$ と定数の全体 $C$ で自由生成された半群を $M$ とおきます(変数は大文字から始まる文字列、定数は小文字から始まる文字列、演算子は $*$ とします)。変数の重複を避けるため、変数は可算個あるとします。 $s: V \to M$ を拡張して半群の準同型 $s: M \to M$ とすることができます。 $s: V \to M$ を拡張した半群の準同型 $s: M \to M$ の全体を $S(M)$ とおきます。

「 $m \in M$ を $n \in M$ に変換する規則」 $r$ に対応する写像 $f_r: M \to P(M)$ ( $P(M)$ は $M$ のべき集合)を以下のように定義します。

まず $m$ と $n$ に現れる変数をどこにも現れていない変数で置き換えたものを $m'$ と $n'$ とします。

$s(x) = s(m')$ を満たす $s \in S(M)$ が存在するとき、 $s(x) = s(m')$ を満たす最小の $s$ (mgu)が存在します。このとき $f_r(x) = \{s(n')\}$ と定義します。 $s(x) = s(m')$ を満たす $s$ が存在しないときは $f_r(x)$ は空集合とします。

$g_r: M \to P(M)$ を $g_r(x) = \{u * v' * w \mid x = u * v * w \ かつ \ v' \in f_r(v)\}$ とおきます( $u, w$ は空でもよい)。

$h_r: P(M) \to P(M)$ を $\displaystyle h_r(X) = \bigcup_{x \in X} g_r(x)$ とおきます。

「 $m \in M$ を $n \in M$ に変換する規則」からなる集合 $R$ に対して $p: P(M) \to P(M)$ を $\displaystyle p(X) = \bigcup_{r \in R} h_r(x)$ とおきます。

$a \in M$ 、 $b \in M$ に対して $b \in p^k(\{a\})$ となる $k$ が存在することは $R$ に属する規則によって「 $a = a_1 = a_2 = \cdots = a_{k-1} = b$ 」と変形できることを表しています。

以下は、規則の集合 $R$ (実際には等式の両方向への変形)と等式 $a = b$ を指定して式の変形「 $a = a_1 = a_2 = \cdots = a_{k-1} = b$ 」を求めるプログラムです。このような変形ができない場合は停止しなくても良いとします。 $k$ を制限する最大値 step_max と $a, a_1, a_2, \cdots, a_{k-1}, b$ の列を表す path を指定することができます。

一つの解が得られた後、別の解を求めることができます。規則の逆方向の変形もできるため、解は無限に存在します。規則は部分式に対して適用されるため、逆方向の変形をしても元に戻るとは限りません。変数は別の変数で置き換えられることがあるため、同じ式を表すものでも変数が異なることがあります。これらのことから無意味な変形を省くには手間がかかります。プログラムが終了するかどうかを調べるのは難しいです。

この説明を書いた後に、前回のプログラム(step_max を省略できるようにしたもの)の説明を書いてもらいました。以下のようになります。

モノイドを使った説明を書きたいのですが、それは実現できていません。この点は今後検討します。

以下は、指定された半群の式の変形プログラムの詳細な説明です。
半群の式の変形プログラム

クラスと関数の概要

`Equation` クラス

左辺 (`left`) と右辺 (`right`) からなる等式を表します。

メソッド:

`__init__(self, left: 'Exp', right: 'Exp')`: 等式の初期化。

`__str__(self) -> str`: 等式を文字列として表示。

`from_string(equation: str) -> 'Equation'`: 文字列から等式を生成。

`reverse(self) -> 'Equation'`: 等式の左右を反転。

`rule_change_name(self, index: int) -> 'Equation'`: 等式の変数名を一意に変更。

`Exp` クラス

式を表します。変数と定数の積のリストとして構成されます。

メソッド:

`__init__(self, exp: 'Union[str, Factor, List[Factor]]')`: 式の初期化。

`__str__(self) -> str`: 式を文字列として表示。

`__len__(self) -> int`: 式の長さを取得。

`__add__(self, exp2: 'Exp') -> 'Exp'`: 式同士の結合。

`__eq__(self, exp2: object) -> bool`: 式の等価性の判定。

`is_variable(self) -> bool`: 式が変数かどうかの判定。

`change_name(self, index: int) -> 'Iterable[Factor]'`: 式の変数名を変更。

`subexpressions(self) -> 'Iterable[Tuple[Exp, Exp, Exp]]'`: 式の部分式を生成。

`Factor` クラス

式の要素（変数または定数）を表します。

メソッド:

`from_str(factor: str) -> 'Factor'`: 文字列から要素を生成。

`Variable` クラス (`Factor`を継承)

変数を表します。

メソッド:

`__init__(self, name: str)`: 変数の初期化。

`__eq__(self, factor2: object) -> bool`: 変数の等価性の判定。

`__str__(self) -> str`: 変数を文字列として表示。

`Constant` クラス (`Factor`を継承)

定数を表します。

メソッド:

`__init__(self, name: str)`: 定数の初期化。

`__eq__(self, factor2: object) -> bool`: 定数の等価性の判定。

`__str__(self) -> str`: 定数を文字列として表示。

`DictionaryNode` クラス

辞書のノードを表します。

メソッド:

`__init__(self, value: 'Tuple[T, Optional[U]]', next_node: 'Optional[DictionaryNode[T, U]]')`: ノードの初期化。

`__iter__(self)`: ノードのイテレータ。

`__str__(self)`: ノードを文字列として表示。

`__getitem__(self, key: T) -> 'Optional[U]'`: ノードから値を取得。

`keys(self) -> 'Iterable[T]'`: ノードのキーを取得。

`Dictionary` クラス

辞書を表します。

メソッド:

`__init__(self, src: 'Optional[Dictionary]'=None)`: 辞書の初期化。

`__str__(self)`: 辞書を文字列として表示。

`__getitem__(self, key: str) -> 'Exp'`: 辞書から値を取得。

`__setitem__(self, key: str, value: 'Exp')`: 辞書に値を設定。

`keys(self) -> 'Iterable[str]'`: 辞書のキーを取得。

`define(self, key: str, value: 'Exp') -> 'Dictionary'`: 新しい辞書を定義。

`Unifier` クラス

式の単一化を表します。

メソッド:

`__init__(self)`: 単一化の初期化。

`__str__(self) -> str`: 単一化を文字列として表示。

`define(self, key: 'Exp', value: 'Exp') -> 'Unifier'`: 新しい単一化を定義。

`unify(self, exp1: 'Exp', exp2: 'Exp') -> 'Iterable[Unifier]'`: 式の単一化を行う。

`get_value(self, exp: 'Exp') -> 'Exp'`: 単一化された値を取得。

`apply_rule(self, expr: 'Exp', rule: 'Equation', step_count: int) -> 'Iterable[Tuple[Exp, Unifier]]'`: 規則を適用して式を変形。

メインロジック

`proof_transformation_by_step` 関数

指定された変換規則に従い、ターゲット式へ変換するステップを行います。

引数:

`target`: 変換後の式。

`rules`: 変換規則のリスト。

`current_ext_exps`: 現在の式と単一化のリスト。

`steps`: 変換ステップを保持する辞書。

`step_count`: 現在のステップ数。

`path`: 変換のパス。

返り値: 次のステップの式と単一化のリスト。

`proof_transformation` 関数

式の変換証明を実行します。

引数:

`goal`: 目標とする等式。

`rules`: 変換規則のリスト。

`step_max`: 最大ステップ数。

`path`: 変換のパス。

返り値: 証明の成否。
実行例
変換規則の定義
equations: 'List[str]' = [
    "e * X = X",
    "X * e = X",
    "x_l * x = e",
    "x * x_r = e"
]
これらの規則を使って式を変形します。
入力式と目標式
goal_string = "x_l = x_r"
goal_equation = Equation.from_string(goal_string)
この等式を証明することを目指します。
証明の実行
path = ["x_l", "x_l * e", "x_l * x * x_r", "e * x_r", "x_r"]
if not proof_transformation(goal_equation, rules, 5, path):
    print(f"{goal_equation.left} から {goal_equation.right} への証明に失敗しました。")
指定された変換パスを辿って証明を行います。

このプログラムは、半群の構造を持つ式に対して、指定された規則に基づいて変形を行い、目標とする等式を証明します。変数の一意性を保ちつつ部分式の変形を行うことで、複雑な式の変形も扱えるようになっています。