主页 / user-22286023

MogicFrog's questions

Martin Hope
MogicFrog
Asked: 2023-09-14 19:47:30 +0800 CST
  • 6

假设我们有一个名为 的数据类型Tree，以及一个size计算其大小的函数

datatype Tree = Empty | Node(key: int, left: Tree, right: Tree)
function size(t: Tree): (s: nat)
{
  match t
  case Empty => 0
  case Node(_, l, r) => size(l) + size(r) + 1
}

现在由于某些原因，我想让这棵树以某种方式“平衡”。具体来说，就是

predicate alpha_weight_balanced(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
{
  if t == Empty then true
  else
    size(t.left) as real <= alpha*(size(t) as real)
    && size(t.right) as real <= alpha*(size(t) as real)
    && alpha_weight_balanced(t.left,alpha)
    && alpha_weight_balanced(t.right,alpha)
}

当成alpha_weight_balanced立时，树的每个子节点的大小t都小于alpha*size(t)。自然地，这个引理应该成立

lemma test(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
  requires alpha_weight_balanced(t, alpha)
  requires t != Empty
  ensures size(t.left) as real <= alpha*(size(t) as real)
{}

然而，达夫尼无法证明这个“明显”的引理。我什至尝试过size像这样包裹

function f(a: int): int
// there is no implemetion for `f`

predicate alpha_weight_balanced(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
{
  if t == Empty then true
  else
    f(size(t.left)) as real <= alpha*f(size(t)) as real
    && f(size(t.right)) as real <= alpha*f(size(t)) as real
    && alpha_weight_balanced(t.left,alpha)
    && alpha_weight_balanced(t.right,alpha)
}

lemma test(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
  requires alpha_weight_balanced(t, alpha)
  requires t != Empty
  ensures     f(size(t.left)) as real <= alpha*f(size(t)) as real
              && f(size(t.right)) as real <= alpha*f(size(t)) as real
{
}

达夫尼成功地证明了这一点。但是如果我修改这个函数f

function f(a: int): int
ensures f(a) == a

证明又失败了。

我对此很困惑，有人知道为什么吗？

verification