モノイドの左逆元・右逆元(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} への証明に失敗しました。")
