module Type.Reduction where

Right now this file is not used in other things. In the rest of the formalisation we compute types via NBE. Instead, it acts as a warmup to understanding reduction of types, progress, etc.

This version of reduction does not compute under binders. The NBE version does full normalisation.

Imports

open import Type
open import Type.RenamingSubstitution
open import Builtin.Constant.Type
open import Relation.Nullary
open import Data.Product
open import Data.Empty

open import Agda.Builtin.Nat
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

Values

Values, types in the empty context that cannot reduce any furter, presented as a predicate. We don’t reduce under either lambda or pi binders here.

data Value⋆ : ∅ ⊢⋆ J → Set where

  V-Π : (N : ∅ ,⋆ K ⊢⋆ *)
        -----------------
      → Value⋆ (Π N)

  _V-⇒_ : Value⋆ A
        → Value⋆ B
          --------------
        → Value⋆ (A ⇒ B)

  V-ƛ : (N : ∅ ,⋆ K ⊢⋆ J)
        -----------------
      → Value⋆ (ƛ N)

  V-con : (tcn : TyCon)
          ----------------
        → Value⋆ (con tcn)

  V-μ : Value⋆ A
      → Value⋆ B
        --------------
      → Value⋆ (μ A B)

Converting a value back into a term. For this representation of values this is trivial:

discharge : {A : ∅ ⊢⋆ K} → Value⋆ A → ∅ ⊢⋆ K
discharge {A = A} V = A

Reduction

Reduction is intrinsically kind preserving. This doesn’t require proof.

infix 2 _—→⋆_
infix 2 _—↠⋆_

data _—→⋆_ : (∅ ⊢⋆ J) → (∅ ⊢⋆ J) → Set where
  ξ-⇒₁ : A —→⋆ A'
         -----------------
       → A ⇒ B —→⋆ A' ⇒ B

  ξ-⇒₂ : Value⋆ A
    → B —→⋆ B'
      -----------------
    → A ⇒ B —→⋆ A ⇒ B'

  ξ-·₁ : A —→⋆ A'
         ----------------
       → A · B —→⋆ A' · B

  ξ-·₂ : Value⋆ A
       → B —→⋆ B'
         ----------------
       → A · B —→⋆ A · B'

  β-ƛ : Value⋆ B
        -------------------
      → ƛ A · B —→⋆ A [ B ]

  ξ-μ₁ : A —→⋆ A'
         ----------------
       → μ A B —→⋆ μ A' B

  ξ-μ₂ : Value⋆ A
       → B —→⋆ B'
         ----------------
       → μ A B —→⋆ μ A B'

Reflexive transitie closure of reduction

data _—↠⋆_ : (∅ ⊢⋆ J) → (∅ ⊢⋆ J) → Set where

  refl—↠⋆ : --------
             A —↠⋆ A

  trans—↠⋆ : A —→⋆ B
           → B —↠⋆ C
             -------
           → A —↠⋆ C

Progress

An enumeration of possible outcomes of progress: a step or we hit a value.

data Progress⋆ (A : ∅ ⊢⋆ K) : Set where
  step : A —→⋆ B
         -----------
       → Progress⋆ A
  done : Value⋆ A
         -----------
       → Progress⋆ A

The progress proof. For any type in the empty context we can make progres. Note that ther is no case for variables as there are no variables in the empty context.

progress⋆ : (A : ∅ ⊢⋆ K) → Progress⋆ A
progress⋆ (` ())
progress⋆ (μ A B) with progress⋆ A
... | step p  = step (ξ-μ₁ p)
... | done VA with progress⋆ B
... | step p  = step (ξ-μ₂ VA p)
... | done VB = done (V-μ VA VB)
progress⋆ (Π A) = done (V-Π A)
progress⋆ (A ⇒ B) with progress⋆ A
... | step p = step (ξ-⇒₁ p)
... | done VA with progress⋆ B
... | step q  = step (ξ-⇒₂ VA q)
... | done VB = done (VA V-⇒ VB)
progress⋆ (ƛ A) = done (V-ƛ A)
progress⋆ (A · B) with progress⋆ A
... | step p = step (ξ-·₁ p)
... | done VA with progress⋆ B
... | step p = step (ξ-·₂ VA p)
progress⋆ (.(ƛ _) · B) | done (V-ƛ A) | done VB = step (β-ƛ VB)
progress⋆ (con tcn) = done (V-con tcn)

Determinism of Reduction:

A type is a value or it can make a step, but not both:

notboth : (A : ∅ ⊢⋆ K) → ¬ (Value⋆ A × (Σ (∅ ⊢⋆ K) (A —→⋆_)))
notboth .(_ ⇒ _) ((V V-⇒ W) , .(_ ⇒ _) , ξ-⇒₁ p)   = notboth _ (V , _ , p)
notboth .(_ ⇒ _) ((V V-⇒ W) , .(_ ⇒ _) , ξ-⇒₂ _ p) = notboth _ (W , _ , p)
notboth .(μ _ _) (V-μ V W   , .(μ _ _)  , ξ-μ₁ p)   = notboth _ (V , _ , p)
notboth .(μ _ _) (V-μ V W   , .(μ _ _)  , ξ-μ₂ _ p) = notboth _ (W , _ , p)

Reduction is deterministic. There is only one possible reduction step a type can make.

det : (p : A —→⋆ B)(q : A —→⋆ B') → B ≡ B'
det (ξ-⇒₁ p) (ξ-⇒₁ q) = cong (_⇒ _) (det p q)
det (ξ-⇒₁ p) (ξ-⇒₂ w q) = ⊥-elim (notboth _ (w , _ , p))
det (ξ-⇒₂ v p) (ξ-⇒₁ q) = ⊥-elim (notboth _ (v , _ , q))
det (ξ-⇒₂ v p) (ξ-⇒₂ w q) = cong (_ ⇒_) (det p q)
det (ξ-·₁ p) (ξ-·₁ q) = cong (_· _) (det p q)
det (ξ-·₁ p) (ξ-·₂ w q) = ⊥-elim (notboth _ (w , _ , p))
det (ξ-·₂ v p) (ξ-·₁ q) = ⊥-elim (notboth _ (v , _ , q))
det (ξ-·₂ v p) (ξ-·₂ w q) = cong (_ ·_) (det p q)
det (ξ-·₂ v p) (β-ƛ w) = ⊥-elim (notboth _ (w , _ , p))
det (β-ƛ v) (ξ-·₂ w q) = ⊥-elim (notboth _ (v , _ , q))
det (β-ƛ v) (β-ƛ w) = refl
det (ξ-μ₁ p) (ξ-μ₁ q) = cong (λ X → μ X _) (det p q)
det (ξ-μ₁ p) (ξ-μ₂ w q) = ⊥-elim (notboth _ (w , _ , p))
det (ξ-μ₂ v p) (ξ-μ₁ q) = ⊥-elim (notboth _ (v , _ , q))
det (ξ-μ₂ v p) (ξ-μ₂ w q) = cong (μ _) (det p q)