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

Question

假设我有:

• A Linear : Set键入线性 λ 演算项。

• A reduce-once : Term → Term执行全局还原的函数。

• A 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

您可以使用 <-rec来自 Data.Nat.Induction模块做有根据的归纳超过_<_ .在这种情况下，一种解决方案是对谓词“大小严格小于 n 的项可以减少”进行归纳:

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