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

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

尝试过的解决方案

使用Agda version 2.5.4.2。不修复。
使用--termination-depth=10。不修复。

Answer 1

问题是 Agda 看不到 invalid₀ 是高效的。这是因为它既是递归的又不受构造函数保护。 Agda 在决定是否终止时不会查看 maybe 的定义。

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

okay₀ : Maybe Unit → Stream
step (okay₀ x@(just _)) = inj₂ (invalid₀ x)
step (okay₀ nothing) = inj₁ unit

重要的部分是递归 just 案例将构造函数 inj₂ 作为表达式的顶层。

Answer 2

您可以在这里使用 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

在 invalid₀ 的定义中更明确地说明 Size 参数：

step (invalid₀ {i} x) {j} = maybe (λ _ → inj₂ (invalid₀ {j} x)) (inj₁ unit) x

其中 j 的类型为 Size< i，因此对 invalid₀ 的递归调用是在“较小的”Size.

上

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

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

Termination checker fails after abstracting the call site

agda

coinduction

问题

有效

休息

背景

尝试过的解决方案