Free variables in untyped lambda calculus.

Free.agda

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

module Free where

-- This particular way of implementing Untyped Lambda Calculus (i.e. using the
-- standard library for contexts and variables) is inspired by a Gist by G.
-- Allais. The original Gist can be found here:
--
--      https://gist.github.com/gallais/303cfcfe053fbc63eb61

open import Agda.Builtin.Equality
open import Data.Fin hiding (_+_)
open import Data.Nat
open import Relation.Nullary

-- Some effort is put into making the notation as "mathy" as possible.

Context : Set
Context = ℕ

Variable : Context → Set
Variable = Fin

-- The `ext` synonym is only used for contexts.
pattern ext x = suc x

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

infixl 7 _·_

data Free {Γ} : Variable Γ → Term Γ → Set where
    ` : ∀ x → Free x (` x)
    ƛ : ∀ {x M} → Free (suc x) M → Free x (ƛ M)
    ·₁ : ∀ {x M N} → Free x M → Free x (M · N)
    ·₂ : ∀ {x M N} → Free x N → Free x (M · N)

pattern `0 = ` zero
pattern `1 = ` (suc zero)
pattern `2 = ` (suc (suc zero))

s : ∀ {Γ} → Term Γ
s = ƛ (ƛ (ƛ (`2 · `0 · (`1 · `0))))

k : ∀ {Γ} → Term Γ
k = ƛ (ƛ `1)

i : ∀ {Γ} → Term Γ
i = ƛ `0

Closed : ∀ {Γ} → Term Γ → Set
Closed M = ∀ {x} → ¬ Free x M

s-closed : ∀ {Γ} → Closed {Γ} s
s-closed (ƛ (ƛ (ƛ fv))) with fv
... | ·₁ (·₁ ())
... | ·₂ (·₁ ())

k-closed : ∀ {Γ} → Closed {Γ} k
k-closed (ƛ (ƛ ()))

i-closed : ∀ {Γ} → Closed {Γ} i
i-closed (ƛ ())

omega : ∀ {Γ} → Term Γ
omega = ƛ (`0 · `0)

omega-closed : ∀ {Γ} → Closed {Γ} omega
omega-closed (ƛ (·₁ ()))

_⊆_ : 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

rename-FV : ∀ {Γ Δ x} (ρ : Γ ⊆ Δ) (M : Term Γ) → Free x M → Free (ρ x) (rename ρ M)
rename-FV ρ (` x) (` x) = ` (ρ x)
rename-FV ρ (ƛ M) (ƛ fv) = ƛ (rename-FV (ext-ρ ρ) M fv)
rename-FV ρ (M · N) fv with fv
... | ·₁ fv' = ·₁ (rename-FV ρ M fv')
... | ·₂ fv' = ·₂ (rename-FV ρ N fv')

weaken : ∀ {Γ} → Term Γ → Term (ext Γ)
weaken = rename suc

weaken-FV : ∀ {Γ x} (M : Term Γ) → Free x M → Free (suc x) (weaken M)
weaken-FV = rename-FV suc

weaken-zero : ∀ {Γ} (M : Term Γ) → ¬ Free zero (weaken M)
weaken-zero (ƛ M) (ƛ fv) = go M fv
    where
    go : ∀ {Γ} (M : Term (ext Γ)) → ¬ Free (suc zero) (rename (ext-ρ suc) M)
    go `1 ()
    go (ƛ M) (ƛ fv) = ?
    go (M · N) fv with fv
    ... | ·₁ fv' = go M fv'
    ... | ·₂ fv' = go N fv'
weaken-zero (M · N) fv with fv
... | ·₁ fv' = weaken-zero M fv'
... | ·₂ fv' = weaken-zero N fv'

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

infix 4 _⊑_

ext-σ : ∀ {Γ Δ} → Γ ⊑ Δ → ext Γ ⊑ ext Δ
ext-σ σ zero = ` zero
ext-σ σ (suc x) = rename suc (σ 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 ; (suc x) → ` x }) M