提取呼叫站点后，终止检查器失败

Question

问题

我有一个简单的归纳记录，其中有一个求和类型的单个字段。Unit给我们提供了一个简单的类型。

open import Data.Maybe
open import Data.Sum

data Unit : Set where
  unit : Unit

record Stream : Set where
  coinductive
  field
    step : Unit ? Stream

open Stream

作品

valid 通过终止检查器：

valid : Maybe Unit ? Stream
step (valid x) = inj? (valid x)

休息时间

但是说我想消除Maybe Unit成员，只有在有资格时递归just。

invalid? : Maybe Unit ? Stream
step (invalid? x) = maybe (? _ ? inj? (invalid? x)) (inj? unit) x

现在终止检查器不满意！

Termination checking failed for the following functions:
  invalid?
Problematic calls:
  invalid? x

为什么这不满足终止检查器？有没有解决的办法，或者我的概念理解不正确？

背景

agda --version产量Agda version 2.6.0-7ae3882。我仅使用默认选项进行编译。

的输出在-v term:100这里：https : //gist.github.com/emilyhorsman/f6562489b82624a5644ed78b21366239

尝试的解决方案

1. 使用Agda version 2.5.4.2。无法修复。
2. 使用--termination-depth=10。无法修复。

Answer 1

问题是 Agda 不认为这invalid\xe2\x82\x80是富有成效的。这是因为它是递归的并且不受构造函数保护。Agda 不查看定义的内部maybeAgda在决定是否终止时

\n\n

这是一个满足终止检查器的实现，因为两个分支都由构造函数和/或非递归保护：

\n\n

okay\xe2\x82\x80 : Maybe Unit \xe2\x86\x92 Stream\nstep (okay\xe2\x82\x80 x@(just _)) = inj\xe2\x82\x82 (invalid\xe2\x82\x80 x)\nstep (okay\xe2\x82\x80 nothing) = inj\xe2\x82\x81 unit\n

\n\n

重要的部分是递归just情况有构造函数inj\xe2\x82\x82作为表达式的顶层。

\n

Answer 2

您可以在此处使用大小类型。

open import Data.Maybe
open import Data.Sum
open import Size

data Unit : Set where
  unit : Unit

record Stream {i : Size} : Set where
  coinductive
  field
    step : {j : Size< i} ? Unit ? Stream {j}

open Stream

valid : Maybe Unit ? Stream
step (valid x) = inj? (valid x)

invalid? : {i : Size} ? Maybe Unit ? Stream {i}
step (invalid? x) = maybe (? _ ? inj? (invalid? x)) (inj? unit) x

_ : step (invalid? (nothing)) ? inj? unit
_ = refl

_ : step (invalid? (just unit)) ? inj? (invalid? (just unit))
_ = refl

更明确地Size定义以下内容中的参数invalid?：

step (invalid? {i} x) {j} = maybe (? _ ? inj? (invalid? {j} x)) (inj? unit) x

where j具有类型Size< i，因此对的递归调用invalid?位于“ smaller”上Size。

请注意，valid无需通过任何“帮助”即可通过终止检查，根本不需要推理Size。