我正在写一个unification F# 中与 AST 一起使用的算法使用 "Term Rewriting and All That" 进行转换( WoldCat ) 作者:Franz Baader 和 Tobias Nipkow。对于 4.6 节通过变换进行统一，它包含了太多的数学理论和示例，并且没有我希望的那么清晰。
有人可以给出或指出使用转换的更简单的示例吗:
删除、分解、定向、消除。
最佳答案
删除:t = t没有意义，可以从方程组中删除。
1 =? 1 -> nil
Orient:我们希望所有方程的形式为 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
希望这有帮助。
关于f# - 通过变革实现统一，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/9674317/