a reducer for the affine lambda calculus, written in Agda

affine.agda

open import Data.Unit
open import Data.Empty
open import Data.Product
open import Data.Bool using (Bool; true; false; not; _∧_; _∨_)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Induction
open import Data.Fin using (Fin)
open import Relation.Binary.PropositionalEquality
open import Induction.WellFounded

≡-suc : {n m : ℕ} -> (suc n) ≡ (suc m) -> n ≡ m
≡-suc refl = refl

a+b+c=a+c+b : (a b c : ℕ) -> a + b + c ≡ a + c + b
a+b+c=a+c+b a b c = (trans (+-assoc a b c) (trans (cong (_+_ a) (+-comm b c)) (sym (+-assoc a c b))))

-- A partition of `Fin (l + r)` into two sets, one of size `l` and one of size `r`
data Split : (l r : ℕ) -> Set where
  N : Split 0 0
  L : {l r : ℕ} -> Split l r -> Split (suc l) r
  R : {l r : ℕ} -> Split l r -> Split l (suc r)

L* : {n : ℕ} -> Split n 0
L* {0} = N
L* {(suc n)} = L L*

R* : {n : ℕ} -> Split 0 n
R* {0} = N
R* {(suc n)} = R R*

data Indexed : (l r : ℕ) -> Set where
  IL : {l r : ℕ} -> Fin (suc l) -> Split l r -> Indexed (suc l) r
  IR : {l r : ℕ} -> Fin (suc r) -> Split l r -> Indexed l (suc r)

index : {l r : ℕ} -> Split l r -> Fin (l + r) -> Indexed l r
index (L s) Fin.zero = IL Fin.zero s
index (L s) (Fin.suc n) with (index s n)
...                        | (IL i s) = IL (Fin.suc i) (L s)
...                        | (IR i s) = IR i (L s)
index {l} {suc r} (R s) f rewrite (+-suc l r) with f
...                                              | Fin.zero = IR Fin.zero s
...                                              | (Fin.suc n) with (index s n)
...                                                               | (IL i s) = IL i (R s)
...                                                               | (IR i s) = IR (Fin.suc i) (R s)


data Split² (a b c d : ℕ) : Set where
  split² : Split (a + b) (c + d) -> Split a b -> Split c d -> Split² a b c d

transpose-split² : {a b c d : ℕ} -> Split² a b c d -> Split² a c b d
transpose-split² {a} {b} {c} {d} (split² x y z) with (a + b) in eq_ab | (c + d) in eq_cd
transpose-split² {(suc a)} {b} {c} {d} (split² (L x) (L y) z) | (suc ab) | cd
  with (split² u v w) <- (transpose-split² (split² (subst₂ Split (sym (≡-suc eq_ab)) (sym eq_cd) x) y z))
  = (split² (L u) (L v) w)
transpose-split² {a} {(suc b)} {c} {d} (split² (L x) (R y) z) | (suc ab) | cd
  with (split² u v w) <- (transpose-split² (split² (subst₂ Split (sym (≡-suc (trans (sym (+-suc _ _)) eq_ab))) (sym eq_cd) x) y z))
  = (split² (R u) v (L w))
transpose-split² {a} {b} {(suc c)} {d} (split² (R x) y (L z)) | ab       | (suc cd)
  with (split² u v w) <- (transpose-split² (split² (subst₂ Split (sym eq_ab) (sym (≡-suc eq_cd)) x) y z))
  = (split² (subst₂ Split (sym (+-suc _ _)) refl (L u)) (R v) w)
transpose-split² {a} {b} {c} {(suc d)} (split² (R x) y (R z)) | ab       | (suc cd)
  with (split² u v w) <- (transpose-split² (split² (subst₂ Split (sym eq_ab) (sym (≡-suc (trans (sym (+-suc _ _)) eq_cd))) x) y z))
  = (split² (subst₂ Split refl (sym (+-suc _ _)) (R u)) v (R w))
transpose-split² {a} {b} {c} {d} (split² N _ _) | _ | _
  with refl <- (sym (m+n≡0⇒m≡0 a eq_ab)) | refl <- (sym (m+n≡0⇒m≡0 c eq_cd))
  rewrite eq_ab | eq_cd
  = (split² N N N)

transpose-split-ll : {a b c : ℕ} -> Split (a + b) c -> Split a b -> Split (a + c) b × Split a c
transpose-split-ll x y
  with (split² p q _) <- (transpose-split² (split² (subst₂ Split refl (+-comm 0 _) x) y L*))
  = (subst₂ Split refl (+-comm _ 0) p) , q

transpose-split-lr : {a b c : ℕ} -> Split (a + b) c -> Split a b -> Split a (b + c) × Split b c
transpose-split-lr {a} {b} {c} x y
  with (split² p _ q) <- (transpose-split² (split² (subst₂ Split refl (+-comm 0 _) x) y R*))
  = (subst₂ Split (+-comm _ 0) (cong (_+_ b) (+-comm c 0)) p) , (subst₂ Split refl (+-comm _ 0) q)

-- An affine lambda term with *exactly* `n` free vars
data Term : (n : ℕ) -> Set where
  var : Term 1
  app : {n m : ℕ} -> Split n m -> Term n -> Term m -> Term (n + m)
  lam : {n : ℕ} -> Term (suc n) -> Term n
  era : {n : ℕ} -> Term n -> Term n

-- An affine lambda term with *at most* `n` free vars
data Subterm : (n : ℕ) -> Set where
  subterm : {n m : ℕ} -> Split n m -> Term n -> Subterm (n + m)

-- The index of a term; used for termination checking
#-Term : {n : ℕ} -> Term n -> ℕ
#-Term var = 0
#-Term (app _ x y) = (#-Term x) + (#-Term y)
#-Term (lam t) = (suc (#-Term t))
#-Term (era t) = (suc (#-Term t))

-- A chain of arguments, passed in succession to `Term n`, resulting in a `Term m`
data Args : (n m : ℕ) -> Set where
  nil : {n : ℕ} -> Args n n
  arg : {a b c : ℕ} -> Split a b -> Term b -> Args (a + b) c -> Args a c

-- Converts a chain of arguments back into a chain of apps
make-apps : {n m : ℕ} -> Subterm n -> Args n m -> Subterm m
make-apps t nil = t
make-apps (subterm {n} {m} ss t) (arg {_} {b} sa a r)
  with SS , SA <- (transpose-split-ll sa ss)
  = (make-apps (subst Subterm (a+b+c=a+c+b n b m) (subterm SS (app SA t a))) r)

-- The index of a chain of arguments; used for termination checking
#-Args : {n m : ℕ} -> Args n m -> ℕ
#-Args nil = 0
#-Args (arg _ t a) = (#-Term t) + (#-Args a)

-- The index of the inputs to a `Normalizer`; used for termination checking
# : {a b c : ℕ} -> Term a -> Args (a + b) c -> ℕ
# t a = (#-Term t) + (#-Args a)

≡-#-Term : {p q : ℕ} -> (t : Term p) -> (e : p ≡ q) -> (#-Term t) ≡ (#-Term (subst Term e t))
≡-#-Term var refl = refl
≡-#-Term (lam t) refl = (cong suc (≡-#-Term t refl))
≡-#-Term (era t) refl = (cong suc (≡-#-Term t refl))
≡-#-Term (app s x y) refl = (subst₂ (\ p q -> (#-Term (app s x y)) ≡ (p + q)) (≡-#-Term x refl) (≡-#-Term y refl) refl)

≡-#-Args : {p q r : ℕ} -> (a : Args p r) -> (e : p ≡ q) -> (#-Args a) ≡ (#-Args (subst₂ Args e refl a))
≡-#-Args nil refl = refl
≡-#-Args (arg s t a) refl = (cong (\ x -> (#-Term t) + x) (≡-#-Args a refl))

replace' : {n m t : ℕ} -> (t ≡ (suc n)) -> Fin t -> Split n m -> (x : Term t) -> (y : Term m) -> Σ (Term (n + m)) \ t -> (#-Term t) ≡ (#-Term x) + (#-Term y)
replace' e _ _ var t with refl <- e = t , refl
replace' e f s (era t) u with T , p <- (replace' e f s t u) = (era T) , (cong suc p)
replace' e f s (lam t) u with T , p <- (replace' (cong suc e) (Fin.suc f) (L s) t u) = (lam T) , (cong suc p)
replace' {n} {m} {t} e f sr (app sa x y) u with (index sa f)
... | (IL {xn} {yn} i sa)
      with p , q <- (transpose-split-ll (subst₂ Split (≡-suc (sym e)) refl sr) sa)
      with T , k <- (replace' refl i q x u)
      with eq <- (trans (a+b+c=a+c+b xn m yn) (cong (\ x -> (x + m)) (≡-suc e)))
      = (subst Term eq (app {_} {yn} p T y)) ,
      (trans (sym (≡-#-Term (app {_} {yn} p T y) eq))
        (trans (cong (\ n -> n + #-Term y) k) (a+b+c=a+c+b (#-Term x) (#-Term u) (#-Term y)))
      )
... | (IR {xn} {yn} i sa)
      with p , r <- (transpose-split-lr (subst₂ Split (≡-suc (trans (sym e) (+-suc _ _))) refl sr) sa)
      with T , k <- (replace' refl i r y u)
      with eq <- (trans (sym (+-assoc xn yn m)) (cong (\x -> x + m) (≡-suc (trans (sym (+-suc _ _)) e))  ))
      = (subst Term eq (app {xn} {_} p x T)) ,
      (trans (sym (≡-#-Term (app {xn} {_} p x T) eq))
        (trans (cong (\ n -> (#-Term x) + n) k) (sym (+-assoc (#-Term x) (#-Term y) (#-Term u))))
        -- (trans (cong (\ n -> n + #-Term y) k) (a+b+c=a+c+b (#-Term x) (#-Term u) (#-Term y)))
      )

-- Replaces a free variable in a term
replace : {n m : ℕ} -> Fin (suc n) -> Split n m -> (x : Term (suc n)) -> (y : Term m) -> Σ (Term (n + m)) \ t -> (#-Term t) ≡ (#-Term x) + (#-Term y)
replace = replace' refl

Normalizer : (n : ℕ) -> Set
Normalizer n = {a b c : ℕ} -> (t : Term a) -> Split a b -> (a : Args (a + b) c) -> (# t a) < n -> Subterm c

normalizer-base : Normalizer 0
normalizer-base _ _ _ a = ⊥-elim (m<n⇒n≢0 a refl)

normalizer-suc : {n : ℕ} -> Normalizer n -> Normalizer (suc n)
normalizer-suc rec var s a g = (make-apps (subterm s var) a)
normalizer-suc {n} rec {_} {p} (app {r} {s} sa x y) ss a g
  with SA , SS <- (transpose-split-ll ss sa)
  = normalizer-suc rec x SS (arg SA y (subst₂ Args (a+b+c=a+c+b r s p) refl a))
  (subst (\ x -> x < (suc n)) (trans (+-assoc (#-Term x) (#-Term y) (#-Args a))
    (cong (\ t -> #-Term x + (#-Term y + t)) (≡-#-Args a (a+b+c=a+c+b r s p)))
  ) g)
normalizer-suc rec {n} {m} (era t) si nil g
  with x <- (n + m) | (subterm so b) <- (normalizer-suc rec t si nil (<-trans ≤-refl g))
  = (subterm so (era b))
normalizer-suc rec {n} {m} (era t) ss (arg {_} {b} sa a aa) g
  with SS , _ <- (transpose-split-lr sa ss)
  = normalizer-suc rec t SS (subst₂ Args (+-assoc n m b) refl aa)
  (≤-trans (subst (\ x -> (#-Term t + x) < 2+ (#-Term t + (#-Term a + #-Args aa))) (≡-#-Args aa (+-assoc n m b))
    (+-mono-≤ (s≤s (z≤n {1})) (+-monoʳ-≤ (#-Term t) (+-monoˡ-≤ (#-Args aa) z≤n)))
  ) g)
normalizer-suc rec {a} {b} (lam t) S nil g
  with x <- (suc (a + b)) | [ eq ] <- inspect suc (a + b) | (subterm {a} {b} s u) <- (normalizer-suc rec t (L S) nil (<-trans ≤-refl g))
  with s
... | (N) = ⊥-elim (1+n≢0 eq)
... | (L s) = (subst Subterm (sym (≡-suc eq)) (subterm s (lam u)))
... | (R s) = (subst Subterm (sym (≡-suc (trans eq (+-suc _ _)))) (subterm s (era u)))
normalizer-suc {o} rec {n} {m} (lam t) ss (arg {_} {b} sa a aa) (s≤s g)
  with SS , SA <- (transpose-split-ll sa ss)
  with tr , k <- (replace Fin.zero SA t a)
  = rec tr SS (subst₂ Args (a+b+c=a+c+b n m b) refl aa)
  (subst (\ x -> suc (#-Term tr + x) ≤ _) (≡-#-Args aa (a+b+c=a+c+b n m b))
  (subst (\ x -> suc (x + #-Args aa) ≤ _) (sym k)
  (subst (\ x -> suc x ≤ o) (sym (+-assoc (#-Term t) (#-Term a) (#-Args aa)))
  g)))

normalizer' : (n : ℕ) -> ({m : ℕ} -> m < n -> Normalizer m) -> Normalizer n
normalizer' 0 _ = normalizer-base
normalizer' (suc n) m = normalizer-suc {n} (m ≤-refl)

normalizer = All.wfRec <-wellFounded _ Normalizer normalizer'

normal : Term 0 -> Term 0
normal t
  with z <- 0 in eq
     | (subterm _ u) <- normalizer (suc (#-Term t)) t N nil (subst₂ _<_ (+-comm 0 _) refl ≤-refl)
  = (subst Term (trans (m+n≡0⇒m≡0 _ (sym eq)) eq) u)

K = lam (era var)
I = lam var

T = K
F = (normal (app N K I))

Not = (lam (app L* (app L* var F) T))
And = (lam (lam (app L* (app (R L*) var var) F)))
Or = (lam (lam (app R* Not (app (R L*) (app R* And (app R* Not var)) (app R* Not var)))))

test : ⊤
  × F ≡ era (lam var)
  × (normal (app N Not F)) ≡ T
  × (normal (app N Not T)) ≡ F
  × (normal (app N (app N And T) T)) ≡ T
  × (normal (app N (app N And T) F)) ≡ F
  × (normal (app N (app N And F) T)) ≡ F
  × (normal (app N (app N And F) F)) ≡ F
  × (normal (app N (app N Or T) T)) ≡ T
  × (normal (app N (app N Or T) F)) ≡ T
  × (normal (app N (app N Or F) T)) ≡ T
  × (normal (app N (app N Or F) F)) ≡ F
test = tt , refl , refl , refl , refl , refl , refl , refl , refl , refl , refl , refl