General Recursive Functions in Agda

GeneralRecursive.agda

module _ where
open import Data.Nat using (ℕ; suc; _+_)
open import Data.Fin using (Fin) renaming (zero to 𝕫; suc to 𝕤_)
open import Data.Vec using (Vec; []; [_]; _∷_; tail; map; allFin) renaming (lookup to _!_)
open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_)
open import Data.Vec.Relation.Binary.Equality.Propositional using (_≋_; ≋⇒≡)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

variable
  n m n' : ℕ
  i j : Fin n

data Rec : ℕ → Set where
  Z : Rec 0
  S : Rec 1

  π_ : Fin n → Rec n
  _∘_ : Rec n → Vec (Rec m) n → Rec m

  -- 2 more arguments: (x-1) and f(x-1, xs)
  ρ : Rec n → Rec (2 + n) → Rec (1 + n)
  μ : Rec (1 + n) → Rec n

Id : Vec (Rec n) n
Id = map π_ (allFin _)

Add : Rec 2
Add = ρ (π 𝕫) (S ∘ [ π 𝕤 𝕫 ])

infix 3 [_]_≫_  -- Big step
data [_]_≫_ : Rec n → Vec ℕ n → ℕ → Set where
  Z : [ Z ] [] ≫ 0
  S : [ S ] [ n ] ≫ 1 + n

  π_ : ∀ i {v : Vec ℕ n} → [ π i ] v ≫ v ! i
  _∘_ : {f : Rec n} {gs : Vec (Rec m) n}
    → {ms : Vec ℕ m} {ns : Vec ℕ n} {r : ℕ}
    → [ f ] ns ≫ r
    → Pointwise ([_] ms ≫_) gs ns
    → [ f ∘ gs ] ms ≫ r

  ρZ : {base : Rec n} {rec : Rec (2 + n)}
    → {ns : Vec ℕ n} {m : ℕ}
    → [ base ] ns ≫ m
    → [ ρ base rec ] 0 ∷ ns ≫ m
  ρS : {base : Rec n} {rec : Rec (2 + n)}
    → {ns : Vec ℕ n} {n m r : ℕ}  -- note that n is shadowed
    → [ ρ base rec ] n ∷ ns ≫ m
    → [ rec ] n ∷ m ∷ ns ≫ r
    → [ ρ base rec ] 1 + n ∷ ns ≫ r

  μZ : {f : Rec (1 + n)} {ns : Vec ℕ n}
    → [ f ] 0 ∷ ns ≫ 0
    → [ μ f ] ns ≫ 0
  μS : {f : Rec (1 + n)} {ns : Vec ℕ n} {m r : ℕ}
    → [ f ] 0 ∷ ns ≫ 1 + m
    → [ μ (f ∘ (S ∘ [ π 𝕫 ] ∷ tail Id)) ] ns ≫ r
    → [ μ f ] ns ≫ 1 + r

module General where
  {-# TERMINATING #-}
  minimize : (ℕ → ℕ) → ℕ
  minimize f with f 0
  ... | 0 = 0
  ... | suc n = suc (minimize λ n → f (suc n))

  {-# TERMINATING #-}
  exec : Rec n → Vec ℕ n → ℕ
  exec Z ns = 0
  exec S (n ∷ []) = 1 + n
  exec (π i) ns = ns ! i
  exec (f ∘ gs) ns = exec f (map (λ g → exec g ns) gs)
  exec (ρ f g) (0 ∷ ns) = exec f ns
  exec (ρ f g) (suc n ∷ ns) = exec g (n ∷ exec (ρ f g) (n ∷ ns) ∷ ns)
  exec (μ f) ns = minimize λ n → exec f (n ∷ ns)

  test : ℕ  -- 11
  test = exec Add (5 ∷ 6 ∷ [])

-- uniqueness of the results
unique : {f : Rec n} {ns : Vec ℕ n} {m n : ℕ}
  → [ f ] ns ≫ m
  → [ f ] ns ≫ n
  → m ≡ n
PointwiseUnique : {fs : Vec (Rec n) m} {rs : Vec ℕ n} {ms ns : Vec ℕ m}
  → Pointwise ([_] rs ≫_) fs ms
  → Pointwise ([_] rs ≫_) fs ns
  → ms ≡ ns
unique Z Z = refl
unique S S = refl
unique (π i) (π .i) = refl
unique (p ∘ ps) (q ∘ qs) rewrite PointwiseUnique ps qs = unique p q
unique (ρZ p) (ρZ q) = unique p q
unique (ρS p r) (ρS q s) rewrite unique p q = unique r s
unique (μZ p) (μZ q) = refl
unique (μZ p) (μS q _) with unique p q
... | ()
unique (μS p _) (μZ q) with unique p q
... | ()
unique (μS p r) (μS q s) = cong suc (unique r s)

PointwiseUnique [] [] = refl
PointwiseUnique (p ∷ ps) (q ∷ qs)
  rewrite unique p q | PointwiseUnique ps qs = refl