Agda中非柯里化递归函数通过终止检查的方法

问题背景 #

如下定义的自然数域上二元递归函数显然具备终止性：

open import Data.Nat

curried : ℕ → ℕ → ℕ
curried zero    k = k
curried (suc n) k = curried n (suc k)

Agda可正常通过该柯里化函数的终止检查。

该函数的非柯里化版本同样显然终止：递归调用时数对的第一个分量每次都会剥离一层suc构造子，第二个分量的变化不会影响终止性：

open import Data.Product

uncurried : ℕ × ℕ → ℕ
uncurried (zero  , k) = k
uncurried (suc n , k) = uncurried (n , suc k)

但Agda 2.6.2.2版本的终止检查器会拒绝该定义，抛出如下报错：

Termination checking failed for the following functions:
  uncurried
Problematic calls:
  uncurried (n , suc k)

除改写为柯里化形式外，有三类可行方案让上述uncurried函数通过Agda终止检查：

• 显式良基递归（最稳妥，全版本兼容）
  Agda终止检查默认仅能识别直接作为函数参数的结构递归下降，不会自动拆分元组参数识别分量的递减关系。可直接调用自然数小于关系对应的良基递归器，明确指定递归过程始终按元组第一个分量的自然数大小严格下降：

  open import Data.Nat
  open import Data.Product
  open import Induction.Nat
  open import Induction.WellFounded
  
  uncurried : ℕ × ℕ → ℕ
  uncurried (a , b) = <-rec (λ _ → ℕ) helper a b
    where
    helper : (n : ℕ) → (∀ m → m < n → ℕ) → ℕ → ℕ
    helper zero    _ k = k
    helper (suc n) rec k = rec n (s≤s ≤-refl) (suc k)
  

  该写法通过构造性的良基证明保证递归合法性，不依赖终止检查器的自动推导，所有Agda正式版本均可正常通过检查，不会引入逻辑风险。

• 开启大小类型扩展（改动最小）
  开启Agda的大小类型扩展后，可通过类型标记明确告知终止检查器递归调用时元组第一个分量的大小严格递减：

  {-# OPTIONS --sized-types #-}
  open import Data.Nat
  open import Data.Product
  open import Size
  
  uncurried : {i : Size} → ℕ × ℕ i → ℕ
  uncurried (zero  , k) = k
  uncurried (suc n , k) = uncurried (n , suc k)
  

  该方案几乎不需要改动原函数的递归结构，仅需添加编译选项和大小类型标注即可通过检查。

• 添加TERMINATING标注（临时方案，不推荐）
  可直接给函数添加TERMINATING编译指示，跳过终止检查：

  open import Data.Nat
  open import Data.Product
  
  {-# TERMINATING #-}
  uncurried : ℕ × ℕ → ℕ
  uncurried (zero  , k) = k
  uncurried (suc n , k) = uncurried (n , suc k)
  

  注意：该方案会完全关闭对应函数的终止检查，如果函数存在非终止分支会直接导致类型系统逻辑不一致，仅适合已手动完全确认终止性、临时快速验证代码的场景使用。

内容的提问来源于stack exchange，提问作者Cactus