希尔伯特 epsilon 算子

Question

为什么可以在方法和函数中使用 Hilbert epsilon 运算符，但不能在 "function method" 中使用？

method choose<T>(s:set<T>) returns (x:T)
 requires s != {}
{
var z :| z in s;
return z;
}

function choose'<T>(s:set<T>):T
// function method choose'<T>(s:set<T>):T // Activate this line and comment the previous line to see the error
 requires s != {}
{
var z :| z in s;
z
}

Answer 1

为了 Hilbert epsilon 运算符，在 Dafny 中也称为 let-such-that 表达式，

var z :| P; E

要可编译，约束 P 必须唯一地确定 z。在您的情况下，约束 P 是 z in s，它不能唯一地确定 z，单例集除外。

如果 s 是 set<int> 类型，您可以（低效地）通过将 choose' 函数更改为：

来满足此要求

function method choose'<T>(s:set<int>):int
  requires s != {}
{
  var z :| z in s && forall y :: y in s ==> z <= y;
  z
}

差不多。你需要说服 Dafny 有这样一个 z。你可以在引理中做到这一点。这是一个可能比必要的时间更长但我首先得到的工作引理可以做到这一点。请注意，引理也使用 Hilbert 运算符，但在语句上下文中，因此唯一性要求不适用。

function method choose'<T>(s:set<int>):int
  requires s != {}
{
  HasMinimum(s);
  var z :| z in s && forall y :: y in s ==> z <= y;
  z
}

lemma HasMinimum(s: set<int>)
  requires s != {}
  ensures exists z :: z in s && forall y :: y in s ==> z <= y
{
  var z :| z in s;
  if s == {z} {
    // the mimimum of a singleton set is its only element
  } else if forall y :: y in s ==> z <= y {
    // we happened to pick the minimum of s
  } else {
    // s-{z} is a smaller, nonempty set and it has a minimum
    var s' := s - {z};
    HasMinimum(s');
    var z' :| z' in s' && forall y :: y in s' ==> z' <= y;
    // the minimum of s' is the same as the miminum of s
    forall y | y in s
      ensures z' <= y
    {
      if
      case y in s' =>
        assert z' <= y;  // because z' in minimum in s'
      case y == z =>
        var k :| k in s && k < z;  // because z is not minimum in s
        assert k in s';  // because k != z
    }
  }
}

很遗憾，您的 s 类型不是 set<int>。我不知道如何从通用集合中获取唯一值。 :(

有关为什么唯一性要求在编译表达式中很重要的信息，请参阅 this paper。

鲁斯坦

Answer 2

好的，谢谢，非唯一确定值的编译问题我明白了。但是，根据您的回答，我的第一个方法 choose 应该会引发与函数方法 choose' 相同的错误，不是吗？

method choose<T>(s:set<T>) returns (x:T)
 requires s != {}
{
var z :| z in s;
return z;
}

function choose'<T>(s:set<T>):T
// function method choose'<T>(s:set<T>):T // Activate this line and comment the previous line to see the error
 requires s != {}
{
var z :| z in s;
z
}

希尔伯特 epsilon 算子

The Hilbert epsilon operator

epsilon

operator-keyword

dafny