时间戳

首页 > 解决方案 > 希尔伯特 epsilon 算子

operator-keyword - 希尔伯特 epsilon 算子

问题描述

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

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
}

标签： operator-keyworddafnyepsilon

解决方案

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

var z :| P; E

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

如果s是 type 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. 你可以在引理中做到这一点。这是一个可能比必要时间更长但我得到的第一件事就是这样做的引理。请注意，引理也使用希尔伯特运算符，但在语句上下文中，因此不适用唯一性要求。

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>. 我不知道如何从一般集合中获得唯一值。:(

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

鲁斯坦

推荐阅读