Nordstrom1988.agda

{-

Nordström, B. (1988) “Terminating general recursion”
http://dx.doi.org/10.1007/BF01941137

Mu, S-C. (2008) “Well-founded recursion and accessibility”
http://www.iis.sinica.edu.tw/~scm/2008/well-founded-recursion-and-accessibility/

-}

module Nordstrom1988 where

open import Agda.Builtin.Nat using (zero ; suc ; _-_) renaming (Nat to ℕ)


data _≤_ : ℕ → ℕ → Set where
  refl≤ : ∀ {n} → n ≤ n
  step≤ : ∀ {n m} → n ≤ m → n ≤ suc m

_<_ : ℕ → ℕ → Set
n < m = suc n ≤ m


-- 5. Primitive recursion and mathematical induction

-- Natural induction

natrec : ∀ {C : ℕ → Set} →
         (p : ℕ) → C zero → (∀ x → C x → C (suc x)) →
         C p
natrec zero    d e = d
natrec (suc p) d e = e p (natrec p d e)


-- 6. Course-of-values recursion and complete induction

-- Course-of-values induction (1)

{-# TERMINATING #-}
covrec₁ : ∀ {C : ℕ → Set} →
          (p : ℕ) → C zero → (∀ x → (∀ z → z ≤ x → C z) → C (suc x)) →
          C p
covrec₁ zero          d e = d
covrec₁ (suc zero)    d e = e zero    (λ z z≤0   → covrec₁ z d e)
covrec₁ (suc (suc p)) d e = e (suc p) (λ z z≤1+p → covrec₁ z d e)


-- Course-of-values induction (2)

{-# TERMINATING #-}
covrec₂ : ∀ {C : ℕ → Set} →
          (p : ℕ) → (∀ x → (∀ z → z < x → C z) → C x) →
          C p
covrec₂ p e = e p (λ z z<p → covrec₂ z e)


-- Complete induction

{-# TERMINATING #-}
comrec : ∀ {C : ℕ → Set} →
         (p : ℕ) → (∀ x → (∀ z → z < x → C z) → C x) →
         C p
comrec p e = e p (λ z z<p → comrec z e)


-- 9. The set of accessible elements

data Acc {A : Set} (_≺_ : A → A → Set) : A → Set where
  acc : ∀ x → (∀ y → y ≺ x → Acc _≺_ y) → Acc _≺_ x

Well-founded : ∀ {A : Set} → (A → A → Set) → Set
Well-founded _≺_ = ∀ x → Acc _≺_ x


-- Example

wf< : Well-founded _<_
wf< n = acc n (access n)
  where
    access : ∀ n m → m < n → Acc _<_ m
    access zero    m  ()
    access (suc n) .n refl≤       = acc n (access n)
    access (suc n) m  (step≤ m<n) = access n m m<n


-- 7. General recursion and well-founded induction

unacc : ∀ {A : Set} {_≺_ : A → A → Set} {C : A → Set} →
        (p : A) → Acc _≺_ p → (∀ x → (∀ z → z ≺ x → C z) → C x) →
        C p
unacc p (acc .p h) e = e p (λ z z≺p → unacc z (h z z≺p) e)

wfrec : ∀ {A : Set} {_≺_ : A → A → Set} {C : A → Set} →
        (p : A) → Well-founded _≺_ → (∀ x → (∀ z → z ≺ x → C z) → C x) →
        C p
wfrec p wf e = unacc p (wf p) e


-- Example

{-# TERMINATING #-}
div? : ℕ → ℕ → ℕ
div? zero    m       = zero
div? (suc n) zero    = suc n
div? (suc n) (suc m) = suc (div? (suc n - suc m) (suc m))

sn-sm<sn : ∀ n m → (n - m) < suc n
sn-sm<sn n       zero    = refl≤
sn-sm<sn zero    (suc m) = refl≤
sn-sm<sn (suc n) (suc m) = step≤ (sn-sm<sn n m)

div₁ : ℕ → ℕ → ℕ
div₁ n m = wfrec n wf< (body m)
  where
    body : ∀ m n → (∀ k → k < n → ℕ) → ℕ
    body m       zero    rec = zero
    body zero    (suc n) rec = suc n
    body (suc m) (suc n) rec = suc (rec (suc n - suc m)
                                        (sn-sm<sn n m))

div₂ : ℕ → ℕ → ℕ
div₂ n m = rec n m (wf< n)
  where
    rec : ∀ n → ℕ → Acc _<_ n → ℕ
    rec zero    m       (acc .0 h)       = zero
    rec (suc n) zero    (acc .(suc n) h) = suc n
    rec (suc n) (suc m) (acc .(suc n) h) = suc (rec (suc n - suc m) (suc m)
                                                    (h (suc n - suc m) (sn-sm<sn n m)))