Как убедить компилятор Agda в том, что выражение заканчивается?

Question

Я изучаю Agda, используя Основы языка программирования Филиппа Уодлера В Agda , и я не могу понять, как убедить компилятор в том, что вычисление завершается.

У меня естьтипы для унарных и двоичных натуральных чисел:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

И я написал функцию для преобразования между двумя представлениями (используя несколько помощников):

-- try to count to a given power of two
--
-- to-count m t f n =
--    t (n - 2^m)     if n >= 2^m
--    (f * 2^m) + n   otherwise
to-count : ℕ → (ℕ → Bin) → Bin → ℕ → Bin
to-count zero    t f zero    = f
to-count zero    t f (suc n) = t n
to-count (suc m) t f n       = to-count m (to-count m t (f I)) (f O) n

-- keep trying to count bigger and bigger powers of two
to-next : ℕ → ℕ → Bin
to-next m = to-count m (to-next (suc m)) (⟨⟩ I)

to : ℕ → Bin
to = to-count zero (to-next zero) ⟨⟩

Позже, когда я пытался доказать, что мойпреобразование верное:

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)

_ : to zero ≡ ⟨⟩
_ = refl

_ : to (suc zero) ≡ ⟨⟩ I
_ = refl

Компилятор жалуется, что проверка завершения не удалась:

Checking Naturals (Naturals.agda).
Naturals.agda:23,1-24,48
Termination checking failed for the following functions:
  to-next
Problematic calls:
  to-next (suc m)
    (at Naturals.agda:24,25-32)
Naturals.agda:37,5-9
to-next zero zero != ⟨⟩ I of type Bin
when checking that the expression refl has type
to (suc zero) ≡ (⟨⟩ I)

Какие стратегии я могу использовать, чтобы убедить компилятор в том, что он завершает работу?

Answer 1

Использование прагмы - это не то, как вам нужно убедить компилятор в том, что функция завершается.

Компилятор указал на проблемный вызов: to-next (suc m) не может рассматриваться как неиспользуемый в тех случаях, которые вы считаете, и, очевидно, он создаетструктурно большее значение, чем на входе.

Способ решения этой проблемы состоит в том, чтобы выразить конструкцию Bin из ℕ по-другому.

inc-bin : Bin -> Bin
inc-bin ⟨⟩ = ⟨⟩ I
inc-bin (bb O) = bb I
inc-bin (bb I) = (inc-bin bb) O

to-bin-daft : ℕ -> Bin
to-bin-daft zero = b O
to-bin-daft (suc m) = inc-bin (to-bin-daft m)

Это «глупый», так какбуквально увеличивает Bin на единицу за каждый suc, но более сложные алгоритмы, включающие, скажем, деление на 2, требуют доказательства того, что результат деления меньше, чем ввод.

Answer 2

Не уверен, что это самое идиоматическое решение, но я запустил его, используя TERMINATING pragma:

{-# TERMINATING #-}
to-next : ℕ → ℕ → Bin
to-next m = to-count m (to-next (suc m)) (⟨⟩ I)