如何从大小减少的显式证明到停止减少算法？

Question

假设我有：

线性 λ 微积分项的 Linear : Set 类型。
一个 reduce-once : Term → Term 函数，它执行全局减少 redexes。
一个计算构造函数数量的size : Linear → Nat关系。
证明reduce-once-halts : (t : Linear) → size (reduce-once t) < size t.

也就是说，我有一个证据表明应用 reduce-once 总是会减小术语的大小。由此，逻辑上应该能够实现一个终止函数，reduce : (t : Linear) → Sigma t IsNormalized，将术语减少到正常形式。因为我相信这是一种常见的情况，所以我的问题是：这在 Agda 中通常是如何形式化的？我如何才能说服它减小其参数大小的函数可以递归应用并最终停止？

Answer 1

您可以使用 Data.Nat.Induction 模块中的 <-rec 对 _<_ 进行有根据的归纳。在这种情况下，一种解决方案是对谓词 "terms of size strictly less than n can be reduced":

进行归纳

open import Data.Nat
open import Data.Nat.Induction
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

postulate
  Term : Set
  reduce-once : Term → Term
  size : Term → ℕ
  reduce-once-halts : (t : Term) → size (reduce-once t) < size t

reduce-aux : (n : ℕ) (t : Term) → size t < n → Term
reduce-aux = <-rec
  (λ n → (t : Term) → size t < n → Term)
  λ n h t size-t<n → h (size t) size-t<n (reduce-once t) (reduce-once-halts t)

reduce : Term → Term
reduce t = reduce-aux (1 + size t) t ≤-refl

如何从大小减少的显式证明到停止减少算法？

How to go from an explicit proof of size decrease to a halting reduction algorithm?

agda