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

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

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

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