模块 Diffing

参数化 diffing

此模块实现了对任意内容列表的 diffing。它通过以下参数进行参数化：

• 两个列表的内容
• 当元素保留时的相等性证明
• 当元素发生变化时的 diffing 证明

Diffing 被扩展以维护状态，该状态取决于在遍历两个列表时计算出的变化。

底层算法是修改后的 Wagner-Fischer 算法（参见 <https://en.wikipedia.org/wiki/Wagner%E2%80%93Fischer_algorithm>）。

我们提供以下保证：给定两个列表 l 和 r，如果不同的补丁导致不同的状态，我们说该状态发生分歧。

• 我们始终返回 l 和 r 前缀上的最佳补丁，在该前缀上状态不会发生分歧。
• 否则，我们将返回一个正确但非最佳的补丁，其中没有分歧状态的子补丁对于给定的初始状态是最佳的。

更准确地说，Wagner-Fischer 的最优性取决于以下属性：左输入的 k 前缀和右输入的 l 前缀之间的编辑距离 d(k,l) 满足

d(k,l) = min ( del_cost + d(k-1,l), insert_cost + d(k,l-1), change_cost + d(k-1,l-1) )

在这个假设下，贪婪地选择将左 k 前缀转换为右 l 前缀的最小补丁的状态作为所有可能的补丁（将左 k 前缀转换为右 l 前缀）的状态的代表是最佳的。

如果该属性不满足，我们仍然可以贪婪地选择一个代表状态。但是，计算出的补丁不再保证是全局最优的。尽管如此，它仍然是一个正确的补丁，它甚至在所有探索过的补丁中是最优的。