f# - 変形による一体化

Question

Franz Baader と Tobias Nipkow による"Term Rewriting and All That" ( WoldCat ) を使用して、 AST変換で使用する F#の統合アルゴリズムを作成しています。セクション 4.6 変換による統一については、例を使った数学理論が多すぎて、私が望んでいたほど明確ではありませんでした。

誰かが変換を利用するより簡単な例を挙げたり指摘したりできますか:

削除、分解、方向付け、消去。

Answer 1

削除:t = t無意味であり、方程式のセットから削除できます。

1 =? 1 -> nil

向き: すべての方程式を の形にしたいx =? tので、 の形の方程式を反転しますt =? x。

2 =? x1 -> x1 =? 2

削除: が与えられた場合、他のすべての方程式を変更して、 のすべてのインスタンスをにx =? t置き換えます。xt

x1 + x2 = 7, x2 = 5 -> x1 + 5 = 7, x2 = 5

分解: の形式の方程式を得るには、任意の関数を取り、それらを削除する必要がありx =? tます。このプロセスでは、技術的に一度に 1 つの機能のみが削除されることに注意してください。

x1 + 5 = 7 -> x1 = 2
2 * (x1 + x2) = 14 -> x1 + x2 = 7

うまくいけば、これが役に立ちます。