agda - 抽象调用站点后终止检查器失败

Question

问题

我有一个简单的 coductive 记录，其中包含一个总和类型的字段。 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 yield Agda version 2.6.0-7ae3882 .我只使用默认选项进行编译。
-v term:100的输出在这里:https://gist.github.com/emilyhorsman/f6562489b82624a5644ed78b21366239

尝试的解决方案

使用 Agda version 2.5.4.2 .不修复。

使用 --termination-depth=10 .不修复。

Answer 1

您可以使用 sized types这里。

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

哪里j有类型 Size< i ，所以递归调用 invalid₀位于“较小”Size .

请注意 valid ，不需要任何“帮助”来通过终止检查，不需要推理 Size的。