求一组递归结果的最小值
求一组递归结果的最小值
提问于 2020-01-14 00:20:45
我正在用Dafny编码编辑距离递推方程。
我想我已经验证了它，但是我很好奇是否有一种更简洁的方法来表示在三个编辑选项中重复使用的选择：
E(i,j) := min { 1 + E(i-1,j), 1 + E(i, j-1), diff(i, j) + E(i-1,j-1) }在达夫尼：
if 1 + recEdDist'(a, b, ai+1, bi) < 1 + recEdDist'(a, b, ai, bi+1)
&& 1 + recEdDist'(a, b, ai+1, bi) < diff(a[ai], b[bi]) + recEdDist'(a, b, ai+1, bi+1)
then 1 + recEdDist'(a, b, ai+1, bi) else
if 1 + recEdDist'(a, b, ai, bi+1) < 1 + recEdDist'(a, b, ai+1, bi)
&& 1 + recEdDist'(a, b, ai, bi+1) < diff(a[ai], b[bi]) + recEdDist'(a, b, ai+1, bi+1)
then 1 + recEdDist'(a, b, ai, bi+1) else
diff(a[ai], b[bi]) + recEdDist'(a, b, ai+1, bi+1)全来源在这里.
回答 1
Stack Overflow用户
发布于 2020-01-15 16:55:00
如果你定义
function min(a: int, b: int) : int
{ if a < b then a else b }下面的表达式给出了三个参数中的最小值：
min(1 + E(i-1,j), (min(1 + E(i, j-1), diff(i, j) + E(i-1,j-1))达芙妮为你证明了这样的事情，以防你担心：
assert min(a, min(b, c)) <= a;
assert min(a, min(b, c)) <= b;
assert min(a, min(b, c)) <= c;
assert min(a, min(b, c)) == a || min(a, min(b, c)) == b || min(a, min(b, c)) ==c;你说你认为你已经核实过了。但是我看到的是一个只有函数定义和一些测试的Dafny文件。验证的只是归纳函数的明确性和这几个测试用例。您的意思是通过验证，还是您也有一个根据此函数进行验证的实现？
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/59725981
复制相关文章
相似问题
腾讯云开发者
