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

user_1031791 0
Viewed 83

Suppose I have:

  • A Linear : Set type for linear λ-calculus terms.

  • A reduce-once : Term → Term function that performs a global reduction of redexes.

  • A size : Linear → Nat relation that counts the number of constructors.

  • A proof reduce-once-halts : (t : Linear) → size (reduce-once t) < size t.

That is, I have a proof that applying reduce-once always decreases the size of a term. From that, one should logically be able to implement a terminating function, reduce : (t : Linear) → Sigma t IsNormalized, that reduces the term to normal form. Since I believe this is a common situation, my question is: how is that usually formalized in Agda? How can I convince it that a function that decreases the size of its argument can be applied recursively and will eventually halt?

agda
1 Answers

You can use <-rec from the Data.Nat.Induction module to do well-founded induction over _<_. In this case, one solution is to do induction on the predicate "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
user_28825160
Related