通过变革实现统一

Question

我正在写一个 统一 F# 中的算法可用于 谷草转氨酶 转换使用 “术语重写和所有这些” (野猫）弗朗茨·巴德尔和托拜厄斯·尼普科。对于 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

希望这有帮助。