为什么Dafny归纳谓词使用序数?

第11.1.2节 提供以下极端谓词示例:

inductive predicate g(x: int) { x == 0 || g(x-2) }
copredicate G(x: int) { x == 0 || G(x-2) }

然后,第11.1.3节给出了一些关于它们的示例证明:

lemma EvenNat(x: int)
  requires g(x)
  ensures 0 <= x && x % 2 == 0
{
  var k: nat :| g#[k](x); EvenNatAux(k, x);
}

lemma EvenNatAux(k: nat, x: int)
  requires g#[k](x)
  ensures 0 <= x && x % 2 == 0
{
  if x == 0 {
  } else {
    EvenNatAux(k-1, x-2);
  }
}

lemma Always(x: int)
  ensures G(x)
{ forall k: nat { AlwaysAux(k, x); } }
lemma AlwaysAux(k: nat, x: int)
  ensures G#[k](x)
{ }

这些引理 don't type-check . 前缀调用表示法 g#[k](x)

参数0的类型不匹配(需要函数 ORDINAL ,得到 nat )

inductive lemma 和 colemma 第11.1.4节中的示例可以正常工作。我的问题是11.1.3。

这一定改变了。为什么普通人比自然人是更好的选择?这两种类型是否有可能产生不同的固定点,如果有,为序数产生的固定点是否真的是最小的固定点?

我有点担心我可能会定义一个归纳谓词

inductive predicate isProvable(x) {
    isAxiom(x) || exists w :: isProvable(w) && implies(w, x)
}

它的意思是荒谬的,允许无限的 implies 因为索引是序数。我担心是不是错了?