Проверка завершения завершается неудачно после абстрагирования сайта вызова

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

Здесь вы можете использовать типы размера .

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.

Answer 2

Проблема в том, что Агда не видит, что invalid₀ продуктивно.Это потому, что он является рекурсивным и не защищен конструктором.Агда не смотрит внутрь определения maybe, когда решает, заканчивается ли это или нет.

Вот реализация, которая удовлетворяет проверке завершения, потому что обе ветви защищены конструкторами и / или нерекурсивны:

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

Важной частью является рекурсивный just case имеетконструктор inj₂ в качестве верхнего уровня выражения.