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

Question

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?

Possible duplicate of [Assisting Agda's termination checker](https://stackoverflow.com/q/19642921/3237465). — effectfully, Oct 24 '19 at 23:37
Are `Linear` and `Term` meant to be the same type here? If so, I think your current hypotheses are impossible. If `reduce-once` is always applicable and always makes size smaller you get an infinite descending chain of `Nat`s. Which is impossible since `Nat` with the usual ordering is well-founded. — Potato44, Oct 25 '19 at 18:24
@Potato44 yes, that was a typo. Also sorry, I forgot to add a `Not(HasRedex t)` argument; the actual code is [here](https://github.com/moonad/Formality-Agda/blob/master/Formality.agda) just in case I have any further typo (`reduce-once-halts` is called `reduce<`). — MaiaVictor, Nov 02 '19 at 14:57

score 2 · Accepted Answer · answered Nov 01 '19 at 10:34

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

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

1 Answers1