Primitive recursive functions in Agda

Primrec.agda

open import Data.Nat
open import Data.Fin as Fin

module Primrec where

  -- The datatype of primitive recursive function
  data PR : ∀ (k : ℕ) → Set where
    pr-zero : PR 0 -- zero
    pr-succ : PR 1 -- successor
    pr-proj : ∀ {k} (i : Fin k) → PR k -- projection
    pr-comp : ∀ {k m} (fs : Fin k → PR m) (g : PR k) → PR m -- composition
    pr-rec  : ∀ {k} (f : PR k) (g : PR (suc (suc k))) → PR (suc k) -- primitive recursion

  -- Evaluate a primitive recursive function
  eval : ∀ {k} (f : PR k) → (∀ (i : Fin k) → ℕ) → ℕ
  eval pr-zero xs = 0
  eval pr-succ xs = suc (xs zero)
  eval (pr-proj i) xs = xs i
  eval (pr-comp fs f) xs = eval f λ i → eval (fs i) xs
  eval (pr-rec f g) xs = primrec (xs zero)
     where primrec : ℕ → ℕ
           primrec zero = eval f (λ i → xs (suc i))
           primrec (suc n) = eval g (λ { Fin.zero → n
                                       ; (Fin.suc Fin.zero) → primrec n
                                       ; (Fin.suc (Fin.suc i)) → xs (suc i)})

  -- unary and binary evaluation
  eval-1 : PR 1 → ℕ → ℕ
  eval-1 f n = eval f λ _ → n

  eval-2 : PR 2 → ℕ → ℕ → ℕ
  eval-2 f m n = eval f λ { zero → m ; (suc zero) → n}

  -- unary composition
  pr-comp-1 : ∀ {k} → PR k → PR 1 → PR k
  pr-comp-1 f g = pr-comp (λ i → f) g

  -- binary composition
  pr-comp-2 : ∀ {k} → PR k → PR k → PR 2 → PR k
  pr-comp-2 f g h = pr-comp (λ { zero → f ; (suc zero) → g}) h

  -- useful projections
  pr-fst : ∀ {k} → PR (suc k)
  pr-fst = pr-proj Fin.zero

  pr-snd : ∀ {k} → PR (suc (suc k))
  pr-snd = pr-proj (Fin.suc Fin.zero)

  pr-thd : ∀ {k} → PR (suc (suc (suc k)))
  pr-thd = pr-proj (Fin.suc (Fin.suc Fin.zero))

  -- identity
  pr-id : PR 1
  pr-id = pr-fst

  -- constant map
  pr-const : ∀ {k} → ℕ → PR k
  pr-const zero = pr-comp (λ {()}) pr-zero
  pr-const (suc n) = pr-comp-1 (pr-const n) pr-succ

  -- predecessor
  pr-pred : PR 1
  pr-pred = pr-rec (pr-const 0) pr-fst

  -- addition
  pr-add : PR 2
  pr-add = pr-rec pr-id (pr-comp-1 pr-snd pr-succ)

  -- multiplication
  pr-mul : PR 2
  pr-mul = pr-rec (pr-const 0) (pr-comp-2 pr-snd pr-thd pr-add)

  -- examples

  three : ℕ
  three = eval-1 pr-pred 4

  seven : ℕ
  seven = eval-2 pr-add 3 4

  forty-two : ℕ
  forty-two = eval-2 pr-mul 6 7