f# - 转型统一

Question

我正在使用Franz Baader 和 Tobias Nipkow 的“Term Rewriting and All That”（WoldCat ）在 F# 中编写一个统一算法，用于AST转换。对于第 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。请注意，从技术上讲，此过程一次仅删除一个功能。

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

希望这会有所帮助。