f# - 转型统一

Question

我正在写一个 unification F# 中的算法用于 AST使用 "Term Rewriting and All That" 的转换( WoldCat ) 作者:Franz Baader 和 Tobias Nipkow。对于第 4.6 节通过变换统一，它的数学理论太多了，而且没有我想要的那么清楚。

有人可以给出或指出使用转换的更简单的例子:

删除、分解、定位、消除。

Answer 1

删除:t = t是没有意义的，可以从方程组中删除。

1 =? 1 -> nil

东方:我们希望所有方程都以 x =? t 的形式存在，所以以 t =? x 的形式翻转任何方程.

2 =? x1 -> x1 =? 2

消除:给定 x =? t ，更改所有其他方程以替换 x 的所有实例与 t .

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

分解:我们需要取任何函数并消去它们以获得 x =? t形式的方程。 .请注意，此过程在技术上一次仅删除一个功能。

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

希望这会有所帮助。