recursion - 协助Agda的终止检查器制作递归函数

Question

假设我们希望为某些类型 A₀ ⋯ Aₙ 和 B 定义一个函数

f : A₀ ⋯ Aₙ → B
f x₀ ⋯ xₙ = ... recursive call to f ...

假设这个定义在结构上不是递归的。

还假设我有以下定义:

1. 一个函数 g : A₀ ⋯ Aₙ → ℕ ，它采用以下子集 f 的参数为自然数；

2. 对于 f 的每种情况: 证明参数的 g 传递给递归 call 严格小于传入参数的 g (使用自然数上的内置 _<_ 或 _<′_ 关系)。

我如何将这些部分放在一起来创建一个递归函数， 使用 Agda“标准”库中的 Induction 模块？

---

此问题是 this question 的后续问题关于同一主题，已经给出了非常完整的答案。然而，我觉得示例函数的类型不幸地被选择为 ℕ → ℕ，这让我很难看出它是如何扩展到一般情况的。

另外，请注意，我并不期望得到一个详细的答案，并解释有理有据的归纳背后的工作原理及其在 Agda 中的实现，如 @Vitus 善意提供的 quite an elaborate answer for this .

Answer 1

如果您有一个函数 A → B 并且您知道 B 具有良好基础的关系，则可以在 A 上构造一个良好基础的关系:

_<_ : B → B → Set
f   : A → B

_≺_ : A → A → Set
x ≺ y = f x < f y
-- or more concisely
_≺_ = _<_ on f -- 'on' come from Function module

证明 _≺_ 也是有根据的并不难，但它已经在标准库中，所以我们只需使用它:

open Inverse-image
  {A = A}     -- new type
  {_<_ = _≺_} -- new relation
  f
  renaming (well-founded to <⇒≺-well-founded)

Inverse-image 导出 well-founded 值作为证明。然后我们可以使用这个值来获取为我们执行递归的实际函数:

≺-well-founded = <⇒≺-well-founded <-well-founded

open All (≺-well-founded)
  renaming (wfRec to ≺-rec)

就是这样，≺-rec 现在可用于实现以 A 作为参数类型的递归函数。

---

≺-rec 的使用大致如下:

g : A → C
g = ≺-rec
  _  {- level paremeter -}
  _  {- A → Set; return type in case Agda cannot figure out the dependency -}
  go {- helper function -}
  where
  go : ∀ x → (∀ y → y ≺ x → C) → C
  go x rec = ... (rec arg proof) ...

arg 是递归发生的参数，proof 是参数实际上更小的证明。

当返回类型取决于参数时，辅助函数大致如下所示:

go : ∀ x → (∀ y → y ≺ x → C y) → C x

---

当处理具有多个参数的函数时，您需要将它们集中到一个类型中，以便关系可以讨论所有这些参数。这通常意味着对，或者，如果参数之间存在依赖关系，则意味着依赖对。