エレファント・ビジュアライザー調査記録

ビジュアルプログラミングで数式の変形を表すことを考えていくブロクです。

人工知能的代数学(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} への証明に失敗しました。")

指定された変換パスを辿って証明を行います。


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

人工知能的代数学(14)

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

前回のプログラムの動作を確認するため
「以下の Python のコードは、「モノイドの左逆元と右逆元が一致する」ことを示す式の変形を表示するものです。proof_transformation で path を指定して調べる範囲を限定すると停止するのですが、path を指定しない場合は停止するかどうかわかりません。停止するかどうかを調べる方法はありますか」
アサーションを追加して調べることはできますか」
「すべてのアサーションが成功した場合、停止することを証明できますか」
「現在は step_max は必ず指定してこの回数で終了するようになっていますが、step_max は指定しなくてもよいとして、指定しないときは無限の回数実行されるとしてください(このようにコードが変更されているとしてください)。この状態のコードで無限の回数実行する(step_max を指定しない)とき、path を(正しく)指定したときは停止すると仮定してください。このとき、無限の回数実行するコード(step_max を指定しない)で、path を指定しない場合、停止することが証明できるようにさらにアサーションを追加してください。」
「このプログラムは以前は deque で実装されていました。このとき deque に追加した式の中で読み出されないものがあるため無限に実行される(のではないか)という現象が起こっていました。現在このプログラムはこれをリストで書き換えています。このような現象が起こらないことを確認するため

  • リストに追加した式は本当に追加されている
  • リストに入っている式はいつか必ず読み出すことができる

ということを確認するためのアサーションを追加してください。」
と入力すると、アサーションを追加してくれたのですが、動作が確認できるようにはなりませんでした。

「証明できる等式を入力したとき停止する」ことを示すためのアサーションはどうすれば良いか、今後検討してみます。

中間報告(18)

ブログに書く意味があるものは何かを ChatGPT で調べようと思ったのですが、なかなかうまくいきません。最近では Python の機能を調べるために使っています。Python の情報は詳しく教えてくれます。ウェブで検索すると古いバージョンの情報が出てくることがあるので、ChatGPT の方が安心して使えます。

ある時 Visual Studio のデザイナーが開けなくなったので Google Colabを 試してみました。Google Colab では Python で書くことになるのですが、Python は詳しくは知らないので ChatGPT で聞いてみたら答えてくれることがわかりました。(Google Colab でもできると思うのですがまだやっていません)

以前 Visual StudioPython を使えるようにしていたと思うので調べてみたら、使えるようになっていました。さらに Visual StudioPython の型チェックができることがわかりました。これはけっこう便利なので、今は Visual StudioPython を使っています。

Visual Studioのアップデートができるようになっていたのでアップデートしたところ、デザイナーが使えるようになりました。以前は(今となってはよくわからないのですが)デザイナーからボタンをダブルクリックして処理を追加した後、デザイナーを開くことができなくなったように思います。処理を追加したとき、デザイナーのコードのファイルには処理が追加されているのに通常のコードのファイルには何も追加されていなくて整合性がなくなったのが原因のように思われます。アップデート後、デザイナーのコードのファイルの処理をテキストエディターで削除したらデザイナーが開けるようになりました。

半群の右単位元と左単位元

ChatGPTで、半群の右単位元と左単位元が一致することの証明を書いてもらおうとしました。また、これを証明する式の変形を表示するプログラムを書いてもらおうとしました。これはうまくできませんでした。

その後プログラムの仕様を書いてもらいましたが、その際にプログラムの仕様と同様の説明をしました(これは意味があるのか疑問)。これを使ってプログラムを書き直してもらおうとしていたようですが、保留になっています。

指数関数

自然数の指数の定義を拡張して複素数の指数関数を定義する」ということをやっているのですが、保留中です。

関数型言語の拡張

関数型言語に無限に動作するための機能を追加する」ということをやっているのですが、保留中です。

関数プログラミングクロージャ

関数型言語の拡張」の続きで「変数を変更することができるクロージャーを変数を変更することができないクロージャーに変換する」ということをやっているのですが、保留中です。

状態を持つラムダ計算

クロージャーの調査に代わって「状態モナドを持つラムダ計算を行うプログラミング言語の定義」をやっているのですが、保留中です。

人工知能的論理プログラミング

論理プログラミングでできることについていろいろ調べていましたが、その後「理想的な並行論理プログラミング言語」について調べています。そのために Prolog の動作を説明しようとしています。

人工知能代数学

「置換の分類」、「交換子の計算」、「マグマの左単位元と右単位元」、「モノイドの左逆元・右逆元」についてビジュアルプログラミングを適用することを考えています。保留中です。

「マグマの左単位元と右単位元」、「モノイドの左逆元・右逆元」は以前このブログで扱ったものとだいたい同じ内容です。今のままでは意味がないものとなっています。

上で述べた「半群の右単位元と左単位元」も引き継いだ内容となっています。

今は「モノイドの左逆元・右逆元」をモノイドを使って説明して、これを使って Prolog の動作を説明できないかと考えています。

人工知能写像の理論

群論の計算」の「写像による分類」(さらにその後の「写像の計算」)に書いたような写像と同値類の関係についてまとめています。現在はただまとめただけです。

群の準同型定理の説明をなるべく写像の性質と群の性質に分けて議論しようとしているのですが、保留中です。

人工知能的サーバー対ブラウザー

以前書いた「平方根を求めるプログラム」を ChatGPT で調べながら書きました。これも以前書いたものとほとんど同じものを書いています。このプログラムの mutable な変数を immutable な変数に変更するとどうなるかということを考えようとしているのですが、保留中です。

今後の予定

Prolog の処理系をモノイドを使って説明する予定です。これを使って「理想的な並行論理プログラミング言語」について調べます。

関数プログラミング」では、論理プログラミング言語を使って関数プログラミングを実現する方法を考えていました。これを上記の「理想的な並行論理プログラミング言語」を使って行う予定です。

関数プログラミングと無限論理多項式」では、クロージャーが使える言語を定義しました。これを使ってクロージャーの mutable な変数を immutable な変数に変更することを考えます。

「ラムダ計算と無限ラムダ多項式」では、上記のものから派生した言語を定義しました。これについても同様のことを考えます。

人工知能的代数学(13)

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

「モノイドの左逆元・右逆元」の問題について ChatGPT でやってみた記事の続きです。動くように書き直したところ、もとのプログラムはほぼなくなってしまいました。

この処理をモノイドを使って表し、Prolog の処理を記述するための参考にしたいと思っているのですが、モノイドの感じがまだあまりありません。

証明に必要な部分だけ実行するように変更

式の変形の各段階で、必要な一つの式以外はスキップするようにしました。こうするとちゃんと動くようになりました。しかしこの条件を外すと、止まらなくなるようです。どこか間違っているようですが、ロジックは合っているようなので後で調べることにします。

文字列の処理をリストに変更

文字列の処理のところをクラスとして定義して、クラスの中身をリストの処理に書き換えました。速度が改善できたかどうかはまだわかりません。まず止まるのかどうかを確かめなければなりません。

以前 JavaScript に書き換えたら速くなったことがあるので、これはやってみても良いと思います。

ディクショナリを連結リストに変更

この変更でディクショナリをコピーする必要がなくなるので少し速くなるはずです。

全体の流れを変更

全体の流れも「モノイドの左逆元・右逆元」のように、一段階ずつ進めるように変更しました。一段階の式の集まりをリストで表すように変更しました。しかしこれで止まるようになったかどうかはまだ確認できていません。

以下のように書き直しました。

# 半群の式の変形

from typing import Iterable, List, Tuple, Dict, Union
from typing import TypeVar, Generic, Iterable, Optional
import re

T = TypeVar('T')
U = TypeVar('U')
    
class Equation:
    def __init__(self, left: 'Exp', right: 'Exp'):
        self.left = left
        self.right = right
        
    def __str__(self) -> str:
        return str(self.left) + " = " + str(self.right)
        
    @staticmethod
    def from_string(equation: str) -> 'Equation':
        left, right = re.split(r"\s*\=\s*", equation)
        return Equation(Exp(left), Exp(right))
    
    def reverse(self) -> 'Equation':
        return Equation(self.right, self.left)
        
    def rule_change_name(self, index: int) -> 'Equation':
        left = Exp.product(list(Exp.change_name(self.left, index)))
        right = Exp.product(list(Exp.change_name(self.right, index)))
        return Equation(left, right)

class Exp:
    def __init__(self, exp: 'Union[str, Factor, List[Factor]]'):
        if isinstance(exp, str):
            self.factors: 'List[Factor]' = [Factor.from_str(s) for s in re.split(r"\s*\*\s*", exp) if s]
        elif isinstance(exp, Factor):
            self.factors: 'List[Factor]' = [exp]
        else:
            self.factors: 'List[Factor]' = exp
        
    def __str__(self) -> str:
        return " * ".join([str(f) for f in self.factors])
        
    def __repr__(self) -> str:
        return f"Exp({self.factors})"
        
    def __len__(self) -> int:
        return len(self.factors)
        
    def __add__(self, exp2: 'Exp') -> 'Exp':
        return Exp(self.factors + exp2.factors)
        
    def __eq__(self, exp2: object) -> bool:
        return isinstance(exp2, Exp) and self.factors == exp2.factors
        
    def __getitem__(self, index: 'Union[int, slice]') -> 'Exp':
        return Exp(self.factors[index])

    @staticmethod
    def product(factors: 'List[Factor]') -> 'Exp':
        return Exp(factors)

    def is_variable(self) -> bool:
        if len(self) != 1:
            return False
        return isinstance(self.factors[0], Variable)

    def change_name(self, index: int) -> 'Iterable[Factor]':
        for factor in self.factors:
            if isinstance(factor, Variable):
                yield Variable(factor.name + "_" + str(index))
            else:
                yield factor

    def subexpressions(self) -> 'Iterable[Tuple[Exp, Exp, Exp]]':
        for i in range(len(self.factors)):
            for j in range(i + 1, len(self.factors) + 1):
                yield Exp.product(self.factors[:i]), Exp.product(self.factors[i:j]), Exp.product(self.factors[j:])

class Factor:
    @staticmethod
    def from_str(factor: str) -> 'Factor':
        if len(factor) > 0 and factor[0].isupper():
            return Variable(factor)
        else:
            return Constant(factor)

class Variable(Factor):
    def __init__(self, name: str):
        self.name = name
        
    def __eq__(self, factor2: object) -> bool:
        return isinstance(factor2, Variable) and self.name == factor2.name

    def __str__(self) -> str:
        return str(self.name)

    def __repr__(self) -> str:
        return f"Variable({self.name})"

class Constant(Factor):
    def __init__(self, name: str):
        self.name = name

    def __eq__(self, factor2: object) -> bool:
        return isinstance(factor2, Constant) and self.name == factor2.name

    def __str__(self) -> str:
        return str(self.name)

    def __repr__(self) -> str:
        return f"Constant({self.name})"

class DictionaryNode(Generic[T, U]):
    def __init__(self, value: 'Tuple[T, Optional[U]]', next_node: 'Optional[DictionaryNode[T, U]]'):
        self.value = value
        self.next_node = next_node

    def __iter__(self):
        node = self
        while node is not None:
            yield node.value
            node = node.next_node

    def __str__(self):
        return "\n".join([f"{key} = {val}" for (key, val) in self]) + "\n"

    def __repr__(self):
        return str(self)

    def __getitem__(self, key: T) -> 'Optional[U]':
        thiskey, value = self.value
        if thiskey == key:
            return value
        elif self.next_node is None:
            return None
        else:
            return self.next_node[key]

    def keys(self) -> 'Iterable[T]':
        for key, _ in self:
            yield key

class Dictionary:
    def __init__(self, src: 'Optional[Dictionary]'=None):
        if src is None:
            self.node: 'Optional[DictionaryNode[str, Exp]]' = None
        else:
            self.node: 'Optional[DictionaryNode[str, Exp]]' = src.node # コピー

    def __str__(self):
        if self.node is None:
            return ""
        else:
            return str(self.node)

    def __repr__(self):
        return str(self)

    def __getitem__(self, key: str) -> 'Exp':
        if self.node is None:
            return Exp([])
        else:
            val = self.node[key]
            if val is None:
                return Exp([])
            else:
                return val
    
    def __setitem__(self, key: str, value: 'Exp'):
        self.node = DictionaryNode((key, value), self.node)

    def keys(self) -> 'Iterable[str]':
        if self.node is None:
            return []
        else:
            return self.node.keys()

    def define(self, key: str, value: 'Exp') -> 'Dictionary':
        new_dic = Dictionary(self)
        new_dic[key] = value
        return new_dic

class Unifier:
    def __init__(self):
        self.unifier_dic: 'Dictionary' = Dictionary()
        
    def __str__(self) -> str:
        return str(self.unifier_dic)

    def define(self, key: 'Exp', value: 'Exp') -> 'Unifier':
        key_str = str(key)
        new_unifier = Unifier()
        new_unifier.unifier_dic = self.unifier_dic.define(key_str, value)
        return new_unifier
        
    def unify(self, exp1: 'Exp', exp2: 'Exp') -> 'Iterable[Unifier]':
        if len(exp1) == 0 and len(exp2) == 0:
            yield self
        elif len(exp1) == 0 or len(exp2) == 0:
            pass
        elif exp1[0].is_variable():
            if str(exp1[0]) in self.unifier_dic.keys():
                yield from self.unify(self.unifier_dic[str(exp1[0])] + exp1[1:], exp2)
            else:
                for i in range(1, len(exp2) + 1):
                    new_unifier = self.define(exp1[0], exp2[:i])
                    yield from new_unifier.unify(exp1[1:], exp2[i:])
        elif exp2[0].is_variable():
            yield from self.unify(exp2, exp1)
        elif exp1[0] == exp2[0]:
            yield from self.unify(exp1[1:], exp2[1:])

    def get_value(self, exp: 'Exp') -> 'Exp':
        if len(exp) == 0:
            return Exp("")
        elif exp[0].is_variable():
            if str(exp[0]) in self.unifier_dic.keys():
                return self.get_value(self.unifier_dic[str(exp[0])] + exp[1:])
            else:
                return exp[:1] + self.get_value(exp[1:])
        else:
            return exp[:1] + self.get_value(exp[1:])

    def apply_rule(self, expr: 'Exp', rule: 'Equation', step_count: int) -> 'Iterable[Tuple[Exp, Unifier]]':
        name_changed_rule = rule.rule_change_name(step_count)
        pattern = name_changed_rule.left
        replacement = name_changed_rule.right
        
        for left, subexp, right in expr.subexpressions():
            for new_unifier in self.unify(subexp, pattern):
                new_exp = left + replacement + right
                yield new_exp, new_unifier

def proof_transformation_by_step(target: Exp, rules: 'List[Equation]', current_ext_exps: 'List[Tuple[Exp, Unifier]]', steps: 'Dict[str, List[str]]', step_count: int, path: 'Optional[List[str]]') -> 'Optional[List[Tuple[Exp, Unifier]]]':
    new_ext_exps: 'List[Tuple[Exp, Unifier]]' = []
    for current_expr, unifier in current_ext_exps:
        
        if path is not None:
            exp_str = str(unifier.get_value(current_expr))
            if step_count < len(path) and exp_str != path[step_count]:
                continue
        
        for _ in unifier.unify(current_expr, target):
            transformation_steps = steps[str(unifier.get_value(current_expr))]
            print(f"証明成功: {' = '.join(transformation_steps)}")
            return None # 成功のとき
        
        for rule in rules:
            for new_expr, new_unifier in unifier.apply_rule(current_expr, rule, step_count):
                current_expr_value = str(unifier.get_value(current_expr))
                new_expr_value = str(new_unifier.get_value(new_expr))
                new_ext_exps.append((new_expr, new_unifier))
                new_steps = steps[current_expr_value] + [new_expr_value]
                steps[new_expr_value] = new_steps
    
    return new_ext_exps

def proof_transformation(goal: Equation, rules: 'List[Equation]', step_max: int, path: 'Optional[List[str]]' = None) -> bool:
    unifier = Unifier()
    start = goal.left
    ext_exps: 'Optional[List[Tuple[Exp, Unifier]]]' = [(start, unifier)]
    steps: 'Dict[str, List[str]]' = {str(start): [str(start)]}
    
    for step_count in range(step_max):
        ext_exps = proof_transformation_by_step(goal.right, rules, ext_exps, steps, step_count, path)
        if ext_exps is None:
            return True # 成功
    
    return False

# 変換規則
equations: 'List[str]' = [
    "e * X = X",
    "X * e = X",
    "x_l * x = e",
    "x * x_r = e"
]

rules: 'List[Equation]' = []

for equation in equations:
    rule = Equation.from_string(equation)
    rules.append(rule)
    rules.append(rule.reverse())

# 入力式と目標式
goal_string = "x_l = x_r"
#goal_string = "x_l = x_l * e"
#goal_string = "e * x_r = x_r"
goal_equation = Equation.from_string(goal_string)

print("規則")
for rule in rules:
    print(rule)
print(f"証明する等式: {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} への証明に失敗しました。")

人工知能的代数学(12)

モノイドの左逆元・右逆元

「モノイドの左逆元・右逆元」の問題について ChatGPT でやってみました。以下のように入力しました。

以下のような半群の式の変形をするプログラムを書いてください:
変数の全体  V と定数の全体  C で自由生成された半群 M とおきます。
(変数は大文字から始まる文字列、定数は小文字から始まる文字列、演算子 * とします)

 M の元を等式によって変形するとします。
例:
 e * X = X
 X * e = X
 a_L * a = e
 a * a_R = e
これを式を変形する規則と考えます。(左辺から右辺へ、右辺から左辺へ)
 r_1: e * X → X
 r_2: X → e * X
 r_3: X * e → X
 r_4: X → X * e
 r_5: a_L * a → e
 r_6: e → a_L * a
 r_7: a * a_R → e
 r_8: e → a * a_R
これらの規則により等式
 a_L = a_R
を証明する問題を例として考えます。

 M の元  x に対して  x の部分式の全体を  S(x) とおきます。
規則  r: r_L → r_R
に対して  M から  P(M) ( M のべき集合)への写像  g_r
 S(x) の元  y  r_L のユニフィケーションが成功したとき
(変数を式で置き換える写像  σ が存在して  σ(y) = σ(r_L) のとき)
このような写像のうち最小の置き換えとなるものが存在します。
この写像 σ とします。
 g_r(x)  x  y の部分を  r_R で置き換えたもの、
 x = y_L * y * y_R のとき( y_L  y_R はなくてもよい)  y_L * r_R * y_R
 σ による像  σ(y_L * r_R * y_R) をすべて含むとします。

ユニフィケーションを行うとき、変数が重複しないようにするため、
たとえば変数 A の名前を、最初の式のときは A_0、
1回目の変形のときの規則の変数は A_1、
2回目の変形のときの規則の変数は A_2、……
のように変更していくことにします。

 P(M) から  P(M) への写像  h_r
 M の部分集合  X に対して
 h_r(X)  X のすべての元  x に対する  g_r(x) の和集合とします。

 P(M) から  P(M) への写像  p
 M の部分集合  X に対して
 p(X) をすべての  r_i に対する  h_{r_i}(X) の和集合とします。

 q_L = q_R という等式は
 p  k 回適用した  p^k(\{q_L\}) の中に
 q_R との間にユニフィケーションが成功する元が存在するとき
(そのような  k が存在するとき)
証明できます。

このとき
 q_L = 1回目の変形の結果 = 2回目の変形の結果 = … = k-1回目の変形の結果 = q_R
という式の変形を表示するプログラムを書いてください。

すると以下のようなプログラムが返ってきました。

import re
from collections import deque

# 変換規則
rules = [
    (r'e \* (X\d+)', r'\1'),
    (r'(X\d+) \* e', r'\1'),
    (r'(a_L) \* (a)', r'e'),
    (r'(a) \* (a_R)', r'e'),
]

# 入力式と目標式
start_expr = "a_L"
target_expr = "a_R"

# 変形ステップを保存するためのキュー
queue = deque([(start_expr, 0)])
seen = set([start_expr])
steps = {start_expr: []}

def apply_rule(expr, rule, step_count):
    pattern, replacement = rule
    matches = list(re.finditer(pattern, expr))
    
    new_expressions = []
    for match in matches:
        new_expr = expr[:match.start()] + re.sub(pattern, replacement, expr[match.start():match.end()]) + expr[match.end():]
        # 変数名をユニークにする
        new_expr = re.sub(r'([A-Z])(\d*)', lambda m: m.group(1) + str(step_count), new_expr)
        new_expressions.append(new_expr)
    
    return new_expressions

def proof_transformation(start, target, rules):
    step_count = 0
    while queue:
        current_expr, step_count = queue.popleft()
        
        if current_expr == target:
            return steps[current_expr]
        
        for rule in rules:
            new_expressions = apply_rule(current_expr, rule, step_count)
            for new_expr in new_expressions:
                if new_expr not in seen:
                    seen.add(new_expr)
                    queue.append((new_expr, step_count + 1))
                    steps[new_expr] = steps[current_expr] + [new_expr]
    
    return None

# 証明の実行
transformation_steps = proof_transformation(start_expr, target_expr, rules)

if transformation_steps:
    print(f"証明成功: {start_expr} = {' = '.join(transformation_steps)} = {target_expr}")
else:
    print(f"{start_expr} から {target_expr} への証明に失敗しました。")

これはまず、変数は任意の式と一致するというのが実装されていないし、等式の左辺から右辺、右辺から左辺の両方に変形できるというのも実装されていないところが間違っています。変数名の重複を避けるために変数名を変更するというところがちゃんとできていません。そのほかいろいろ間違っているので、全体の流れは残して修正しました。

# 半群の式の変形(文字列版)

from collections import deque
from typing import Deque, Iterable, List, Tuple, Dict, MutableSet
import re

def separate_equation(equation: str) -> 'Tuple[str, str]':
    left, right = re.split(r"\s*\=\s*", equation)
    return left, right

def make_equation(lhs: str, rhs: str) -> str:
    return lhs + " = " + rhs

def factorize(exp: str) -> 'List[str]':
    return re.split(r"\s*\*\s*", exp)

def product(factors: 'List[str]') -> str:
    nonempty_factors = [s for s in factors if s] # 空ではない文字列を取り出す
    return " * ".join(nonempty_factors)

def is_variable(factor: str) -> bool:
    if len(factor) == 0:
        return False
    return factor[0].isupper()

def exp_change_name(exp: str, index: int) -> 'Iterable[str]':
    for factor in factorize(exp):
        if is_variable(factor):
            yield factor + "_" + str(index)
        else:
            yield factor

def rule_change_name(rule: str, index: int) -> 'Tuple[str, str]':
    left, right = separate_equation(rule)
    return product(list(exp_change_name(left, index))), product(list(exp_change_name(right, index)))

def subexpressions(exp: str) -> 'Iterable[Tuple[str, str, str]]':
    factors = factorize(exp)
    for i in range(len(factors)):
        for j in range(i + 1, len(factors) + 1):
            yield product(factors[:i]), product(factors[i:j]), product(factors[j:])

def unify_factors(exp1: 'List[str]', exp2: 'List[str]', unifier: 'Dict[str,str]') -> 'Iterable[Dict[str, str]]':
    if len(exp1) == 0 and len(exp2) == 0:
        yield unifier
    elif len(exp1) == 0 or len(exp2) == 0:
        pass
    elif is_variable(exp1[0]):
        if exp1[0] in unifier:
            yield from unify_factors([unifier[exp1[0]]] + exp1[1:], exp2, unifier)
        else:
            for i in range(1, len(exp2) + 1):
                new_unifier = unifier.copy()
                new_unifier[exp1[0]] = product(exp2[:i])
                yield from unify_factors(exp1[1:], exp2[i:], new_unifier)
    elif is_variable(exp2[0]):
        yield from unify_factors(exp2, exp1, unifier)
    elif exp1[0] == exp2[0]:
        yield from unify_factors(exp1[1:], exp2[1:], unifier)

def unify(exp1: str, exp2: str, unifier: 'Dict[str,str]') -> 'Iterable[Dict[str, str]]':
    factors1 = factorize(exp1)
    factors2 = factorize(exp2)
    yield from unify_factors(factors1, factors2, unifier)
    
def get_value(exp: 'List[str]', unifier: 'Dict[str, str]') -> 'List[str]':
    if len(exp) == 0:
        return []
    elif is_variable(exp[0]):
        if exp[0] in unifier:
            return get_value([unifier[exp[0]]] + exp[1:], unifier)
        else:
            return exp[:1] + get_value(exp[1:], unifier)
    else:
        return exp[:1] + get_value(exp[1:], unifier)

def get_value_string(exp: str, unifier: 'Dict[str, str]') -> str:
    factors = factorize(exp)
    return product(get_value(factors, unifier))

def apply_rule(expr: str, rule: str, step_count: int, unifier: 'Dict[str, str]') -> 'Iterable[Tuple[str, Dict[str, str]]]':
    name_changed_rule = rule_change_name(rule, step_count)
    pattern, replacement = name_changed_rule
    
    for left, subexp, right in subexpressions(expr):
        for new_unifier in unify(subexp, pattern, unifier):
            new_exp = product([left, replacement, right])
            yield new_exp, new_unifier

def proof_transformation(start: str, target: str, rules: 'List[str]'):
    step_count = 0
    while queue:
        current_expr, step_count, unifier = queue.popleft()
        
        for _ in unify(current_expr, target, unifier):
            return steps[get_value_string(current_expr, unifier)]
        
        for rule in rules:
            for new_expr, new_unifier in apply_rule(current_expr, rule, step_count, unifier):
                if new_expr not in seen:
                    current_expr_value = get_value_string(current_expr, unifier)
                    new_expr_value = get_value_string(new_expr, new_unifier)
                    seen.add(new_expr)
                    queue.append((new_expr, step_count + 1, new_unifier))
                    new_steps = steps[current_expr_value] + [new_expr_value]
                    steps[new_expr_value] = new_steps
    
    return None

# 変換規則
equations: 'List[str]' = [
    "e * X = X",
    "X * e = X",
    "x_l * x = e",
    "x * x_r = e"
]

rules: 'List[str]' = []

for equation in equations:
    left, right = separate_equation(equation)
    rules.append(left + " = " + right)
    rules.append(right + " = " + left)

# 入力式と目標式
goal_equation = "x_l = x_r"
start_expr, target_expr = separate_equation(goal_equation)

unifier: 'Dict[str, str]' = {}

# 変形ステップを保存するためのキュー
queue: 'Deque[Tuple[str, int, Dict[str, str]]]' = deque([(start_expr, 0, unifier)])
seen: 'MutableSet[str]' = set([start_expr])
steps: 'Dict[str, List[str]]' = {start_expr: []}

print("規則")
for rule in rules:
    print(rule)
print(f"証明する等式: {goal_equation}")

# 証明の実行
transformation_steps = proof_transformation(start_expr, target_expr, rules)

if transformation_steps:
    print(f"証明成功: {start_expr} = {' = '.join(transformation_steps)}")
else:
    print(f"{start_expr} から {target_expr} への証明に失敗しました。")

これは実行すると止まらないのですが、途中までは正しく動いているようなので、たぶん正しく動いています。

文字列の処理が時間がかかりすぎるのではないかと思われますので、まず文字列の処理のところをクラスとして定義して、クラスの中身をリストの処理に書き換えてみたら速度が改善できるのではないかと思っています。

全体の流れも「モノイドの左逆元・右逆元」のように直すことも検討しています。

人工知能的論理プログラミング(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")

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

人工知能的サーバー対ブラウザー(5)

今回は ChatGPT で Python から F# に書き換えたのですが、これはそのままでは動かなくて、かなり書き直しました。

このプログラムの mutable な変数を mutable ではないものに変更するとどうなるか、ということを考えたいのですが、これはなかなか難しそうです。以前このブログで取り上げたときも、とくに何もできていませんでした。今回も同じことになりそうなので、ブログに書く意味があるのか、と思いますがいちおう ChatGPT をちょっと使ったということで書いておくことにします。

open System
open System.Collections.Generic

let formatDecimal (dec: int seq) =
    let declist: int list = Seq.toList dec
    let head = declist.Head
    let tail = declist.Tail |> List.map string |> String.concat ""
    sprintf "%d.%s" head tail

// decimal 型に対するべき乗演算子
let rec ( ** ) (d: decimal) (exp: int) = 
    if exp = 0 then
        1M
    elif exp > 0 then
        d ** (exp - 1) * d
    else
        d ** (exp + 1) / d

// 数値クラスの定義
type Numbers(number: decimal, squareDifference: decimal, scale: int) =
    let mutable number = number
    let mutable squareDifference = squareDifference
    let mutable scale = scale
    member _.Copy() = Numbers(number, squareDifference, scale)
    member _.GetNextDecimalDigit() =
        let two = decimal 2
        Seq.head (seq {
            for dd in [9..-1..0] do
                let zd = decimal dd * (decimal 10 ** -scale)
                let numberSqDiff = number * zd * two + zd * zd
                if numberSqDiff <= squareDifference then
                    number <- number + zd
                    squareDifference <- squareDifference - numberSqDiff
                    scale <- scale + 1
                    yield dd
            })

// 数値ジェネレータークラス
type NumbersGenerator() =
    let generator =
        let number = decimal 0
        let squareDifference = decimal 3
        let nums = Numbers(number, squareDifference, 0)
        seq { while true do yield nums.GetNextDecimalDigit() }
    member _.GetNextDecimalDigit() =
        generator |> Seq.head
    member _.GenerateDecimal() =
        generator

// 数値サーバークラス
type NumbersServer() =
    let mutable currentNumbers =
        Numbers(decimal 0, decimal 3, 0)
    let generatorServer =
        Seq.unfold (fun n -> Some(n, n)) currentNumbers
    member _.GetNumbers() = currentNumbers
    member _.SetNumbers(numbers: Numbers) =
        currentNumbers <- numbers

// 計算クラス
type Calc() =
    let count = 21
    let generator = NumbersGenerator()
    let generatorServer = NumbersServer()
    let mutable resultNumber = decimal 0
    
    member _.RepeatGenerator() =
        for e in [0 .. count - 1] do
            let zd = (decimal (generator.GetNextDecimalDigit())) / (10M ** e)
            resultNumber <- resultNumber + zd
        resultNumber.ToString()

    member _.RepeatServer() =
        for e in [0 .. count - 1] do
            let numbers = generatorServer.GetNumbers()
            let dd = numbers.GetNextDecimalDigit()
            generatorServer.SetNumbers(numbers)
            resultNumber <- resultNumber + (decimal dd) / (10M ** e)
        resultNumber.ToString()

    member _.IterateGenerator() =
        let dec = Seq.take count (generator.GenerateDecimal())
        formatDecimal dec

    member _.IterateServer() =
        let initialNumbers = Numbers(decimal 0, decimal 3, 0)
        let dec = Seq.take count (Seq.unfold (fun (n: Numbers) -> let nn = n.Copy() in Some(nn.GetNextDecimalDigit(), nn)) initialNumbers)
        formatDecimal dec

// テスト出力
printfn "%s" (Calc().RepeatGenerator())
printfn "%s" (Calc().RepeatServer())
printfn "%s" (Calc().IterateGenerator())
printfn "%s" (Calc().IterateServer())