Normalization by evaluation for System T with the normalization proof and the confluence proof

T.agda

{- Coquand, T., & Dybjer, P. (1997). Intuitionistic model constructions and normalization proofs.
  Mathematical Structures in Computer Science, 7(1). https://doi.org/10.1017/S0960129596002150 -}

open import Data.Empty                            using (⊥)
open import Data.Unit                             using (⊤; tt)
open import Data.Nat                              using (ℕ; zero; suc)
open import Data.Product                          using (_×_; _,_; Σ; proj₁; proj₂; ∃-syntax)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)

infix 3 _-→_ _-↛_
infixr 5 _`→_
infixl 7 _·_ _·ₘ_
------------------------------------------------------------------------------
-- System T in the form of combinatory logic

data Ty : Set where
  `⊥    : Ty 
  `ℕ   : Ty
  _`→_ : (A B : Ty) → Ty

variable
  A B C : Ty

data Term : Ty → Set where
  K    : Term (A `→ B `→ A)
  S    : Term ((A `→ B `→ C) `→ (A `→ B) `→ A `→ C)
  _·_  : (c : Term (A `→ B)) → (a : Term A) → Term B
  `0   : Term `ℕ
  `S   : Term `ℕ → Term `ℕ
  `rec  : Term C → Term (`ℕ `→ C `→ C) → Term (`ℕ `→ C)

variable
  a b c d a′ b′ c′ d′ : Term A
  f g  : Term (A `→ B)
  e e′ : Term (`ℕ `→ C `→ C)

data _-→_ : (M N : Term A) → Set where
  β-K    : K · a · b       -→ a
  β-S    : S · g · f · a   -→ (g · a) · (f · a)
  β-rec0 : `rec d e · `0   -→ d
  β-recS : `rec d e · `S a -→ e · a · (`rec d e · a)

  ξ-·ₗ   : a        -→ a′
         → a · b    -→ a′ · b
  ξ-·ᵣ   : b        -→ b′
         → a · b    -→ a · b′
  ξ-`S   : a        -→ a′
         → `S a     -→ `S a′
  ξ-rec₁ : d        -→ d′
         → `rec d e -→ `rec d′ e
  ξ-rec₂ : e        -→ e′
         → `rec d e -→ `rec d e′

_-↛_ : (a b : Term A) → Set
a -↛ b = (a -→ b) → ⊥
-----------------------------------------------------------------------------
-- Multi-step reduction

infix  1 begin_
infix  2 _-↠_ 
infixr 2 _-→⟨_⟩_ _-↠⟨_⟩_ _≡⟨_⟩_ _≡⟨⟩_
infix 3 _∎

data _-↠_ {A} : (a b : Term A) → Set where
  _∎ : (a : Term A)
    → a -↠ a

  _-→⟨_⟩_
    : (a : Term A) → a -→ b → b -↠ c
      ------------------------------
    → a -↠ c

begin_ : a -↠ b → a -↠ b
begin r = r

_-↠⟨_⟩_ : ∀ a
  → a -↠ b → b -↠ c
  -----------------
  → a -↠ c
a -↠⟨ .a ∎               ⟩ b-↠c = b-↠c
a -↠⟨ .a -→⟨ a→b ⟩ b-↠b′ ⟩ b-↠c = a -→⟨ a→b   ⟩ _ -↠⟨ b-↠b′ ⟩ b-↠c

_≡⟨_⟩_ : ∀ a
  → a ≡ b → b -↠ c
  ----------------
  → a -↠ c
a ≡⟨ refl ⟩ b-↠c = b-↠c

_≡⟨⟩_ : ∀ a
  → a -↠ c
  --------
  → a -↠ c
a ≡⟨⟩ b-↠c = b-↠c


-↠-refl : a -↠ a
-↠-refl {a = a} = a ∎

-↠-·ₗ : a -↠ a′ → a · b -↠ a′ · b
-↠-·ₗ (a ∎)                  = a · _ ∎
-↠-·ₗ (a -→⟨ a→a′ ⟩ a′-↠a′′) = a · _ -→⟨ ξ-·ₗ a→a′ ⟩ -↠-·ₗ a′-↠a′′

-↠-·ᵣ : b -↠ b′ → a · b -↠ a · b′
-↠-·ᵣ (b ∎)                  = _ · b ∎
-↠-·ᵣ (b -→⟨ b→b′ ⟩ b′-↠b′′) = _ · b -→⟨ ξ-·ᵣ b→b′ ⟩ -↠-·ᵣ b′-↠b′′

-↠-`S : a -↠ a′ → `S a -↠ `S a′
-↠-`S (_ ∎)                  = _ ∎
-↠-`S (a -→⟨ a→a′ ⟩ a′-↠a′′) = `S a -→⟨ ξ-`S a→a′ ⟩ -↠-`S a′-↠a′′

-↠-rec₁ : d -↠ d′ → `rec d e -↠ `rec d′ e
-↠-rec₁ (_ ∎)                  = _ ∎
-↠-rec₁ (d -→⟨ d→d′ ⟩ d′-↠d′′) = `rec d _ -→⟨ ξ-rec₁ d→d′ ⟩ -↠-rec₁ d′-↠d′′

-↠-rec₂ : e -↠ e′ → `rec d e -↠ `rec d e′
-↠-rec₂ (_ ∎)                  = _ ∎
-↠-rec₂ (e -→⟨ e→e′ ⟩ e′-↠e′′) = `rec _ e -→⟨ ξ-rec₂ e→e′ ⟩ -↠-rec₂ e′-↠e′′
------------------------------------------------------------------------------
-- Denotational semantics I

⟦_⟧ᴺTy : Ty → Set
⟦ `⊥     ⟧ᴺTy = ⊥
⟦ `ℕ     ⟧ᴺTy = ℕ
⟦ A `→ B ⟧ᴺTy = ⟦ A ⟧ᴺTy → ⟦ B ⟧ᴺTy

rec : {X : Set}
  → X → (ℕ → X → X) → ℕ → X
rec d e zero    = d
rec d e (suc n) = e n (rec d e n)

⟦_⟧ᴺ : Term A → ⟦ A ⟧ᴺTy
⟦ K        ⟧ᴺ = λ x y → x
⟦ S        ⟧ᴺ = λ g f x → g x (f x)
⟦ a · b    ⟧ᴺ = ⟦ a ⟧ᴺ ⟦ b ⟧ᴺ
⟦ `0       ⟧ᴺ = 0
⟦ `S a     ⟧ᴺ = suc ⟦ a ⟧ᴺ
⟦ `rec d e ⟧ᴺ = rec ⟦ d ⟧ᴺ ⟦ e ⟧ᴺ
------------------------------------------------------------------------------
-- Logical consistency by evaluation

consistency : Term `⊥ → ⊥
consistency = ⟦_⟧ᴺ
------------------------------------------------------------------------------
-- Denotational semantics II 

Nf : Term A → Set
Nf a = ∀ {b} → a -↛ b

NF : Ty → Set
NF A = Σ (Term A) Nf

⟦_⟧Ty : Ty → Set
⟦ `⊥     ⟧Ty = ⊥
⟦ `ℕ     ⟧Ty = ℕ
⟦ A `→ B ⟧Ty = NF (A `→ B) × (⟦ A ⟧Ty → ⟦ B ⟧Ty)

`0ⁿᶠ : NF `ℕ
`0ⁿᶠ = `0 , λ ()

`Sⁿᶠ : NF `ℕ → NF `ℕ
`Sⁿᶠ (`n , `n↓) = `S `n , λ { (ξ-`S r) → `n↓ r}

Kⁿᶠ : NF (A `→ B `→ A)
Kⁿᶠ = K , λ ()

K·ⁿᶠ : NF A → NF (B `→ A)
K·ⁿᶠ (a , a↓) = K · a , λ { (ξ-·ᵣ r) → a↓ r}

Sⁿᶠ : NF ((A `→ B `→ C) `→  (A `→ B) `→ A `→ C)
Sⁿᶠ = S , λ ()

S·ⁿᶠ : NF (A `→ B `→ C) → NF ((A `→ B) `→ A `→ C)
S·ⁿᶠ (a , a↓) = S · a , λ { (ξ-·ᵣ r) → a↓ r}

S··ⁿᶠ : NF (A `→ B `→ C) → NF (A `→ B) → NF (A `→ C)
S··ⁿᶠ (a , a↓) (b , b↓) = S · a · b ,
  λ { (ξ-·ₗ (ξ-·ᵣ r)) → a↓ r ; (ξ-·ᵣ r) → b↓ r}

recⁿᶠ : NF C → NF (`ℕ `→ C `→ C) → NF (`ℕ `→ C)
recⁿᶠ (d , d↓) (e , e↓) =
  (`rec d e) , λ { (ξ-rec₁ r) → d↓ r ; (ξ-rec₂ r) → e↓ r}
  
↓_ : ⟦ A ⟧Ty → NF A
↓_ {`ℕ}     zero    = `0ⁿᶠ
↓_ {`ℕ}     (suc a) = `Sⁿᶠ (↓ a)
↓_ {A `→ B} (c , f) = c

_·ₘ_ : ⟦ A `→ B ⟧Ty → ⟦ A ⟧Ty → ⟦ B ⟧Ty
(c , f) ·ₘ q = f q
  
⟦_⟧ : Term A → ⟦ A ⟧Ty
⟦ K        ⟧ = Kⁿᶠ , λ p → K·ⁿᶠ (↓ p) , λ q → p 
⟦ S        ⟧ = Sⁿᶠ , λ p → let a = ↓ p in
  S·ⁿᶠ a    , λ q → let b = ↓ q in
  S··ⁿᶠ a b , λ r → (p ·ₘ r) ·ₘ (q ·ₘ r)
⟦ a · b    ⟧ = ⟦ a ⟧ ·ₘ ⟦ b ⟧
⟦ `0       ⟧ = zero
⟦ `S a     ⟧ = suc ⟦ a ⟧
⟦ `rec d e ⟧ = let 𝑑 = ⟦ d ⟧; 𝑒 = ⟦ e ⟧ in
  recⁿᶠ (↓ 𝑑) (↓ 𝑒) , rec 𝑑 λ x y → 𝑒 ·ₘ x ·ₘ y
------------------------------------------------------------------------------
-- Normalisation by evaluation

nf : (a : Term A) → NF A
nf a = ↓ ⟦ a ⟧

↓′_ : ⟦ A ⟧Ty → Term A
↓′ a = (↓ a) .proj₁

nf′ : Term A → Term A
nf′ a = ↓′ ⟦ a ⟧
------------------------------------------------------------------------------
-- Soudness of normalisation 

⟦⟧-respects-→ : a -→ a′ → ⟦ a ⟧ ≡ ⟦ a′ ⟧
⟦⟧-respects-→ β-K        = refl
⟦⟧-respects-→ β-S        = refl
⟦⟧-respects-→ β-rec0     = refl
⟦⟧-respects-→ β-recS     = refl
⟦⟧-respects-→ (ξ-·ₗ r)   rewrite ⟦⟧-respects-→ r = refl
⟦⟧-respects-→ (ξ-·ᵣ r)   rewrite ⟦⟧-respects-→ r = refl
⟦⟧-respects-→ (ξ-`S r)   rewrite ⟦⟧-respects-→ r = refl
⟦⟧-respects-→ (ξ-rec₁ r) rewrite ⟦⟧-respects-→ r = refl
⟦⟧-respects-→ (ξ-rec₂ r) rewrite ⟦⟧-respects-→ r = refl

nf-respects-→ : a -→ a′ → nf a ≡ nf a′
nf-respects-→ r rewrite ⟦⟧-respects-→ r = refl

nf-respects-↠ : a -↠ a′ → nf a ≡ nf a′
nf-respects-↠ (_ ∎)          = refl
nf-respects-↠ (_ -→⟨ r ⟩ rs) = trans (nf-respects-→ r) (nf-respects-↠ rs)
------------------------------------------------------------------------------
-- Glued values

tmOf : ⟦ A `→ B ⟧Ty → Term (A `→ B)
tmOf ((c , _) , _) = c

Gl : (A : Ty) → ⟦ A ⟧Ty → Set
Gl `ℕ       n = ⊤
Gl (A `→ B) q = {p : ⟦ A ⟧Ty} → Gl A p →
  (↓′ q · ↓′ p -↠ ↓′ (q ·ₘ p)) × Gl B (q ·ₘ p)

gluedRec : Gl (`ℕ `→ C) ⟦ `rec d e ⟧
glued    : (a : Term A) → Gl A ⟦ a ⟧

gluedRec {C} {d} {e} {zero}  tt = (begin
  `rec (nf′ d) (nf′ e) · `0
    -→⟨ β-rec0 ⟩
  nf′ d ∎)
  , glued d
gluedRec {C} {d} {e} {suc n} tt = (begin
  nf′ (`rec d e) · ↓′ (suc n)
    ≡⟨⟩
  `rec (nf′ d) (nf′ e) · `S (↓′ n)
    -→⟨ β-recS  ⟩
  (nf′ e) · (↓′ n) · (`rec (nf′ d) (nf′ e) · ↓′ n)
    -↠⟨ -↠-·ₗ (glued e _ .proj₁) ⟩
  ↓′ (⟦ e ⟧ ·ₘ n) · (`rec (nf′ d) (nf′ e) · ↓′ n)
    -↠⟨ -↠-·ᵣ (gluedRec {C} {d} {e} {n} tt .proj₁) ⟩
  ↓′ (⟦ e ⟧ ·ₘ n) · ↓′ (⟦ `rec d e ⟧ ·ₘ n)
    -↠⟨ glued e _ .proj₂ (gluedRec{C} {d} {e} {n} tt .proj₂) .proj₁ ⟩
  ↓′ (⟦ `rec d e ⟧ ·ₘ suc n) ∎)
  , glued e _ .proj₂ (gluedRec {C} {d} {e} {n} tt .proj₂) .proj₂
glued K       {p} x =
  (K · ↓′ p ∎) , λ {q} y → (K · ↓′ p · ↓′ q -→⟨ β-K ⟩ ↓′ p ∎) , x
glued S       {p} x =
  (S · ↓′ p ∎) , λ {q} y → -↠-refl , λ {r} z → (begin
    ↓′ (⟦ S ⟧ ·ₘ p ·ₘ q) · ↓′ r
      -→⟨ β-S ⟩
    (tmOf p · ↓′ r) · (tmOf q · ↓′ r)
      -↠⟨ -↠-·ₗ (x z .proj₁)  ⟩
    ↓′ (p ·ₘ r) · (tmOf q · ↓′ r)
      -↠⟨ -↠-·ᵣ (y z .proj₁) ⟩
    ↓′ (p ·ₘ r) · ↓′ (q ·ₘ r)
      -↠⟨ x z .proj₂ (y z .proj₂) .proj₁ ⟩
    ↓′ (⟦ S ⟧ ·ₘ p ·ₘ q ·ₘ r) ∎ )
    , x z .proj₂ (y z .proj₂) .proj₂
glued (c · a)    = glued c (glued a) .proj₂
glued `0         = tt
glued (`S a)     = tt
glued (`rec d e) {n} = gluedRec {d = d} {e} {n}

-↠-complete : (a : Term A) → a -↠ nf′ a
-↠-complete K          = K ∎
-↠-complete S          = S ∎
-↠-complete (a · b)    = begin
  a · b
    -↠⟨ -↠-·ₗ (-↠-complete a) ⟩
  nf′ a · b
    -↠⟨ -↠-·ᵣ (-↠-complete b) ⟩
  nf′ a · nf′ b
    -↠⟨ glued a (glued b) .proj₁  ⟩
  nf′ (a · b) ∎
-↠-complete `0         = `0 ∎
-↠-complete (`S a)     = -↠-`S (-↠-complete a)
-↠-complete (`rec d e) = begin
  `rec d e
    -↠⟨ -↠-rec₁ (-↠-complete d) ⟩
  `rec (nf′ d) e
    -↠⟨ -↠-rec₂ (-↠-complete e) ⟩
  `rec (nf′ d) (nf′ e) ∎
------------------------------------------------------------------------------
-- Confluency by normalisation

triangle : a -↠ b
  → b -↠ nf′ a
triangle {a = a} {b} r = begin
  b
    -↠⟨ -↠-complete b ⟩
  nf′ b
    ≡⟨ sym (cong proj₁ (nf-respects-↠ r)) ⟩
  nf′ a ∎

confluence : a -↠ b → a -↠ b′
  → ∃[ c ] (b -↠ c) × (b′ -↠ c)
confluence r s = _ , triangle r , triangle s