Lambda calculus in Agda.

Lambda.agda

{-# OPTIONS --safe --without-K #-}

module Lambda where

open import Data.Fin
open import Data.Nat
open import Data.Sum

Context : Set
Context = ℕ

Variable : Context → Set
Variable = Fin

pattern ext x = suc x

data Term (Γ : Context) : Set where
  ` : Variable Γ → Term Γ
  ƛ : Term (ext Γ) → Term Γ
  _·_ : Term Γ → Term Γ → Term Γ

_⊆_ : Context → Context → Set
Γ ⊆ Δ = Variable Γ -> Variable Δ

infix 4 _⊆_

ext-ρ : ∀ {Γ Δ} → Γ ⊆ Δ → ext Γ ⊆ ext Δ
ext-ρ = lift 1

rename : ∀ {Γ Δ} → Γ ⊆ Δ → Term Γ → Term Δ
rename ρ (` x)   = ` (ρ x)
rename ρ (ƛ M)   = ƛ (rename (ext-ρ ρ) M)
rename ρ (M · N) = rename ρ M · rename ρ N

_⊑_ : Context → Context → Set
Γ ⊑ Δ = Variable Γ → Term Δ

infix 4 _⊑_

ext-σ : ∀ {Γ Δ} → Γ ⊑ Δ → ext Γ ⊑ ext Δ
ext-σ σ zero    = ` zero
ext-σ σ (ext x) = rename ext (σ x)

subst : ∀ {Γ Δ} → Γ ⊑ Δ → Term Γ → Term Δ
subst σ (` x)   = σ x
subst σ (ƛ M)   = ƛ (subst (ext-σ σ) M)
subst σ (M · N) = subst σ M · subst σ N

_[_] : ∀ {Γ} → Term (ext Γ) → Term Γ → Term Γ
M [ N ] = subst (λ { zero → N ; (ext x) → ` x}) M

data _—→_ {Γ} : Term Γ → Term Γ → Set where
  ξ₁ : ∀ {M M' N} → M —→ M' → M · N —→ M' · N
  ξ₂ : ∀ {M N N'} → N —→ N' → M · N —→ M · N'
  β : ∀ {M N} → (ƛ M) · N —→ M [ N ]
  ζ : ∀ {M M'} → M —→ M' → ƛ M —→ ƛ M'

infix 3 _—→_
  
data _—→*_ {Γ} : Term Γ → Term Γ → Set where
  _∎ : ∀ {M} → M —→* M
  _—→⟨_⟩_ : ∀ L {M N} → L —→ M → M —→* N → L —→* N

mutual
  data Neutral {Γ} : Term Γ → Set where
    ` : ∀ x → Neutral (` x)
    _·_ : ∀ {M N} → Neutral M → Normal N → Neutral (M · N)

  data Normal {Γ} : Term Γ → Set where
    ` : ∀ {M} → Neutral M → Normal M
    ƛ : ∀ {M} → Normal M → Normal (ƛ M)

data Progress {Γ} (M : Term Γ) : Set where
  step : ∀ {N} → M —→ N → Progress M
  done : Normal M → Progress M

progress : ∀ {Γ} (M : Term Γ) → Progress M
progress (` x) = done (` (` x))
progress (ƛ M) with progress M
... | step x = step (ζ x)
... | done x = done (ƛ x)
progress (M · N) with progress M
... | step x     = step (ξ₁ x)
... | done (ƛ _) = step β
... | done (` x) with progress N
...   | step y = step (ξ₂ y)
...   | done y = done (` (x · y))