如何说服Agda编译器表达式终止？

Question

我正在使用Philip Wadler's Programming Language Foundations In 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

不确定这是否是最惯用的解决方案，但我使用TERMINATING编译指示使它正常工作：

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

Answer 2

使用编译指示并不是说服编译器终止的方式。

编译器指出了有问题的调用：在您认为的情况下，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递增1，但是更复杂的算法（例如，被2除）需要证据证明除法的结果小于输入。