2

我一直在用“旧”和“新”方法在 Agda 中处理共归纳法进行一些实验，但我认为我仍然遗漏了一些关于 Agda 在不使用Size时对核心递归函数的终止检查行为的重要事实。

例如，考虑 和 的以下Stream定义repeat：

data    Stream (A : Set) : Set
record ∞Stream (A : Set) : Set where
  coinductive
  field force : Stream A
open ∞Stream

data Stream A where
  cons : A -> ∞Stream A -> Stream A

repeat : ∀{A} -> A -> ∞Stream A
force (repeat x) = cons x (repeat x)

粗略地说，协约记录类型∞Stream是专门Thunk用于流的。我在很多 Agda 形式化中看到了类似的定义，尽管它们通常被改进为 aSize以获得更好的精度。无论如何，上面的定义repeat被 Agda 接受，没有任何Size注释。

问题是当我尝试将∞Stream记录分解为 aThunk时，以便我可以Thunk在其他地方重用以定义其他可能无限的数据类型：

record Thunk (A : Set) : Set where
  coinductive
  field force : A
open Thunk

data Stream (A : Set) : Set where
  cons : A -> Thunk (Stream A) -> Stream A

repeat : ∀{A} -> A -> Thunk (Stream A)
force (repeat x) = cons x (repeat x)

注意：

  • 两种情况下的代码repeat完全相同，
  • repeat在每种情况下，都会在构造函数的下方找到递归调用cons，
  • 在每种情况下都会repeat产生一个共归纳记录类型的值，

然而 Agda 接受第一个定义repeat但拒绝第二个定义（以下函数的终止检查失败：repeat）。

我知道使用Thunk标准库中的大小可以修改第二个版本，以便被 Agda 接受。尽管如此，我想了解是什么让上面的第一个版本与第二个版本如此不同，以至于它通过了​​终止检查器。在我看来，它们基本相同。

谢谢！

4

0 回答 0