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

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

ビジュアルプログラミング(4)

数学とソフトウェアのページ」の「群の完備化」自体の説明を詳しく書いていなかったのでここに書いておきます。

群の完備化」はスマートフォンで使いやすいように「Word Problem」から説明等を省略してコンパクトにしたものです。説明は「Word Problem」の方を見てください。

【電子復刻版】bit 1988年04月号(通巻230号)」の記事「新しいプログラミング・パラダイム⑥ 項書換えシステムと完備化手続き」では群の公理を表す等式の集合から書き換え規則の集合を求める方法について書かれています。

等式を書き換え規則とみなすときの変換の方向(等式の左辺から右辺に変換するか、右辺から左辺に変換するか)を決める方法を適当に決めることによって、「wikipedia:クヌース・ベンディックス完備化アルゴリズム」で行うことができるということが書かれています。

群の完備化」はこれを実装したものなのですが、
【電子復刻版】bit 1988年04月号(通巻230号)」では変換の方向については書かれていないようなので、その部分は間違っているかもしれません。等式をうまく選択していけば終了するのですが、任意の順序で選択したときに終了するかどうかは不明です。

「群の完備化」の説明

(1)から(3)の部分

ここでは等式の集合から書き換え規則の集合に変換することができます。

(1)のリストには等式の集合が表示されています。(2)のリストには(1)のリストから得られる書き換え規則の集合が表示されています。(2)のリストは最初は空です。

(1)のリストから選択するか、(2)のボタンを押すと、選択された等式が書き換え規則になり(2)のリストに追加されます。このとき(2)のリストは正規化されます。

(2)のリストによって任意の式が正規化できるようになっていないときは、新しく付け加えられた書き換え規則が付け加えられたとき正規化されるべき等式が(1)のリストに追加されます。

(4)から(7)の部分

(5)の領域に等式を入力して(6)のボタンを押すと、(7)の領域に等式の両辺が(2)の書き換え規則の集合で正規化された等式が表示されます。(4)のリストを選択すると(5)の領域に等式を入力することができます。