Skip to content

Instantly share code, notes, and snippets.

@Lysxia
Created February 17, 2025 20:00
Show Gist options
  • Save Lysxia/7acb28e556bc8c38677a14f843e1a360 to your computer and use it in GitHub Desktop.
Save Lysxia/7acb28e556bc8c38677a14f843e1a360 to your computer and use it in GitHub Desktop.
CoDebruijn scoped syntax of untyped lambda calculus
module CoDebruijn where
open import Data.Product using (_×_; _,_; ∃-syntax)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
data Context : Set where
O : Context
1+_ : Context → Context
data Singleton : Context → Set where
one : Singleton (1+ O)
-- Relevant cover
data Cover : Context → Context → Context → Set where
O : Cover O O O
1+_ : {Γ Γ₁ Γ₂ : Context} → Cover Γ Γ₁ Γ₂ → Cover (1+ Γ) (1+ Γ₁) (1+ Γ₂)
1+ˡ_ : {Γ Γ₁ Γ₂ : Context} → Cover Γ Γ₁ Γ₂ → Cover (1+ Γ) (1+ Γ₁) Γ₂
1+ʳ_ : {Γ Γ₁ Γ₂ : Context} → Cover Γ Γ₁ Γ₂ → Cover (1+ Γ) Γ₁ (1+ Γ₂)
-- Context update for a single binder
data Extend₁ (Γ : Context) : Context → Set where
extend : Extend₁ Γ (1+ Γ) -- the bound variable is used
refl : Extend₁ Γ Γ -- the bound variable is not used
data RTerm (Γ : Context) : Set where
Var : Singleton Γ → RTerm Γ
App : {Γ₁ Γ₂ : Context} → Cover Γ Γ₁ Γ₂ → RTerm Γ₁ → RTerm Γ₂ → RTerm Γ
Lam : {Γ₁ : Context} → Extend₁ Γ Γ₁ → RTerm Γ₁ → RTerm Γ
data Thinning : Context → Context → Set where
O : Thinning O O
1+_ : {Γ Γ₁ : Context} → Thinning Γ Γ₁ → Thinning (1+ Γ) (1+ Γ₁)
1/_ : {Γ Γ₁ : Context} → Thinning Γ Γ₁ → Thinning (1+ Γ) Γ₁
data Term (Γ : Context) : Set where
Weaken : {Γ₁ : Context} → Thinning Γ Γ₁ → RTerm Γ₁ → Term Γ
data RSubst : Context → Context → Set where
[] : RSubst O O
⦅_⦆_∷_ : {Γ Γ₀ Γ₁ Γ₂ : Context} → Cover Γ₀ Γ₁ Γ₂ → RTerm Γ₁ → RSubst Γ Γ₂ → RSubst (1+ Γ) Γ₀
data Subst (Γ₁ Γ₂ : Context) : Set where
Weaken : {Γ₃ : Context} → Thinning Γ₂ Γ₃ → RSubst Γ₁ Γ₃ → Subst Γ₁ Γ₂
Thinnings→Cover : {Γ Γ₁ Γ₂ : Context} → Thinning Γ Γ₁ → Thinning Γ Γ₂ → ∃[ Δ ] Thinning Γ Δ × Cover Δ Γ₁ Γ₂
Thinnings→Cover O O = O , O , O
Thinnings→Cover (1+ θ₁) (1+ θ₂) = let Δ , θ , c = Thinnings→Cover θ₁ θ₂ in 1+ Δ , 1+ θ , 1+ c
Thinnings→Cover (1+ θ₁) (1/ θ₂) = let Δ , θ , c = Thinnings→Cover θ₁ θ₂ in 1+ Δ , 1+ θ , 1+ˡ c
Thinnings→Cover (1/ θ₁) (1+ θ₂) = let Δ , θ , c = Thinnings→Cover θ₁ θ₂ in 1+ Δ , 1+ θ , 1+ʳ c
Thinnings→Cover (1/ θ₁) (1/ θ₂) = let Δ , θ , c = Thinnings→Cover θ₁ θ₂ in Δ , 1/ θ , c
_∷ˢ_ : {Γ₁ Γ₂ : Context} → Term Γ₂ → Subst Γ₁ Γ₂ → Subst (1+ Γ₁) Γ₂
Weaken θ t ∷ˢ Weaken θ₁ s = let Δ , θ′ , c′ = Thinnings→Cover θ θ₁ in Weaken θ′ (⦅ c′ ⦆ t ∷ s)
Thinning-trans : {Γ₁ Γ₂ Γ₃ : Context} → Thinning Γ₁ Γ₂ → Thinning Γ₂ Γ₃ → Thinning Γ₁ Γ₃
Thinning-trans O O = O
Thinning-trans (1+ θ₁) (1+ θ₂) = 1+ Thinning-trans θ₁ θ₂
Thinning-trans (1+ θ₁) (1/ θ₂) = 1/ Thinning-trans θ₁ θ₂
Thinning-trans (1/ θ₁) θ₂ = 1/ Thinning-trans θ₁ θ₂
Cover→Thinning : {Γ Γ₁ Γ₂ : Context} → Cover Γ Γ₁ Γ₂ → Thinning Γ Γ₁ × Thinning Γ Γ₂
Cover→Thinning O = O , O
Cover→Thinning (1+ c) = let θ₁ , θ₂ = Cover→Thinning c in 1+ θ₁ , 1+ θ₂
Cover→Thinning (1+ˡ c) = let θ₁ , θ₂ = Cover→Thinning c in 1+ θ₁ , 1/ θ₂
Cover→Thinning (1+ʳ c) = let θ₁ , θ₂ = Cover→Thinning c in 1/ θ₁ , 1+ θ₂
inv-∷ˢ : {Γ₁ Γ₂ : Context} → Subst (1+ Γ₁) Γ₂ → Term Γ₂ × Subst Γ₁ Γ₂
inv-∷ˢ (Weaken θ (⦅ c ⦆ t ∷ s)) = let θ₁ , θ₂ = Cover→Thinning c in Weaken (Thinning-trans θ θ₁) t , Weaken (Thinning-trans θ θ₂) s
≥O : {Γ : Context} → Thinning Γ O
≥O {O} = O
≥O {1+ Γ} = 1/ ≥O
weaken-subst : {Γ₁ Γ₂ Γ₃ : Context} → Subst Γ₁ Γ₂ → Thinning Γ₁ Γ₃ → Subst Γ₃ Γ₂
weaken-subst s O = Weaken ≥O []
weaken-subst s (1+ θ) = let t₂ , s₂ = inv-∷ˢ s in t₂ ∷ˢ weaken-subst s₂ θ
weaken-subst s (1/ θ) = let _ , s₂ = inv-∷ˢ s in weaken-subst s₂ θ
Cover-Oʳ : {Γ Γ₁ : Context} → Cover Γ Γ₁ O → Γ ≡ Γ₁
Cover-Oʳ O = refl
Cover-Oʳ (1+ˡ c) with Cover-Oʳ c
... | refl = refl
inv-one : {Γ : Context} → RSubst (1+ O) Γ → RTerm Γ
inv-one (⦅ c ⦆ t ∷ []) with Cover-Oʳ c
... | refl = t
min-Cover : {Γ₁ Γ₂ Γ₃ Δ₁ Δ₂ : Context} → Cover Γ₁ Γ₂ Γ₃ → Cover Γ₃ Δ₁ Δ₂ → ∃[ E₁ ] ∃[ E₂ ] Cover E₁ Γ₂ Δ₁ × Cover E₂ Γ₂ Δ₂ × Cover Γ₁ E₁ E₂
min-Cover O O = O , O , O , O , O
min-Cover (1+ c) (1+ θ) = let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ in 1+ E₁ , 1+ E₂ , 1+ c₁ , 1+ c₂ , 1+ c′
min-Cover (1+ c) (1+ˡ θ) = let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ in 1+ E₁ , 1+ E₂ , 1+ c₁ , 1+ˡ c₂ , 1+ c′
min-Cover (1+ c) (1+ʳ θ) = let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ in 1+ E₁ , 1+ E₂ , 1+ˡ c₁ , 1+ c₂ , 1+ c′
min-Cover (1+ˡ c) θ = let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ in 1+ E₁ , 1+ E₂ , 1+ˡ c₁ , 1+ˡ c₂ , 1+ c′
min-Cover (1+ʳ c) (1+ θ) = let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ in 1+ E₁ , 1+ E₂ , 1+ʳ c₁ , 1+ʳ c₂ , 1+ c′
min-Cover (1+ʳ c) (1+ˡ θ) = let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ in 1+ E₁ , E₂ , 1+ʳ c₁ , c₂ , 1+ˡ c′
min-Cover (1+ʳ c) (1+ʳ θ) = let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ in E₁ , 1+ E₂ , c₁ , 1+ʳ c₂ , 1+ʳ c′
min-Coverˡ : {Γ₁ Γ₂ Γ₃ Δ₁ Δ₂ : Context} → Cover Γ₁ Γ₂ Γ₃ → Cover Γ₃ Δ₁ Δ₂ → ∃[ E₁ ] Cover E₁ Γ₂ Δ₁ × Cover Γ₁ E₁ Δ₂
min-Coverˡ O O = O , O , O
min-Coverˡ (1+ c) (1+ θ) = let E₂ , c₂ , c′ = min-Coverˡ c θ in 1+ E₂ , 1+ c₂ , 1+ c′
min-Coverˡ (1+ c) (1+ˡ θ) = let E₂ , c₂ , c′ = min-Coverˡ c θ in 1+ E₂ , 1+ c₂ , 1+ˡ c′
min-Coverˡ (1+ c) (1+ʳ θ) = let E₂ , c₂ , c′ = min-Coverˡ c θ in 1+ E₂ , 1+ˡ c₂ , 1+ c′
min-Coverˡ (1+ˡ c) θ = let E₂ , c₂ , c′ = min-Coverˡ c θ in 1+ E₂ , 1+ˡ c₂ , 1+ˡ c′
min-Coverˡ (1+ʳ c) (1+ θ) = let E₂ , c₂ , c′ = min-Coverˡ c θ in 1+ E₂ , 1+ʳ c₂ , 1+ c′
min-Coverˡ (1+ʳ c) (1+ˡ θ) = let E₂ , c₂ , c′ = min-Coverˡ c θ in 1+ E₂ , 1+ʳ c₂ , 1+ˡ c′
min-Coverˡ (1+ʳ c) (1+ʳ θ) = let E₂ , c₂ , c′ = min-Coverˡ c θ in E₂ , c₂ , 1+ʳ c′
min-Coverʳ : {Γ₁ Γ₂ Γ₃ Δ₁ Δ₂ : Context} → Cover Γ₁ Γ₂ Γ₃ → Cover Γ₃ Δ₁ Δ₂ → ∃[ E₂ ] Cover E₂ Γ₂ Δ₂ × Cover Γ₁ Δ₁ E₂
min-Coverʳ O O = O , O , O
min-Coverʳ (1+ c) (1+ θ) = let E₂ , c₂ , c′ = min-Coverʳ c θ in 1+ E₂ , 1+ c₂ , 1+ c′
min-Coverʳ (1+ c) (1+ˡ θ) = let E₂ , c₂ , c′ = min-Coverʳ c θ in 1+ E₂ , 1+ˡ c₂ , 1+ c′
min-Coverʳ (1+ c) (1+ʳ θ) = let E₂ , c₂ , c′ = min-Coverʳ c θ in 1+ E₂ , 1+ c₂ , 1+ʳ c′
min-Coverʳ (1+ˡ c) θ = let E₂ , c₂ , c′ = min-Coverʳ c θ in 1+ E₂ , 1+ˡ c₂ , 1+ʳ c′
min-Coverʳ (1+ʳ c) (1+ θ) = let E₂ , c₂ , c′ = min-Coverʳ c θ in 1+ E₂ , 1+ʳ c₂ , 1+ c′
min-Coverʳ (1+ʳ c) (1+ˡ θ) = let E₂ , c₂ , c′ = min-Coverʳ c θ in E₂ , c₂ , 1+ˡ c′
min-Coverʳ (1+ʳ c) (1+ʳ θ) = let E₂ , c₂ , c′ = min-Coverʳ c θ in 1+ E₂ , 1+ʳ c₂ , 1+ʳ c′
split-subst : {Γ₀ Δ₀ Γ₁ Γ₂ : Context} → RSubst Γ₀ Δ₀ → Cover Γ₀ Γ₁ Γ₂ → ∃[ Δ₁ ] ∃[ Δ₂ ] RSubst Γ₁ Δ₁ × RSubst Γ₂ Δ₂ × Cover Δ₀ Δ₁ Δ₂
split-subst [] O = _ , _ , [] , [] , O
split-subst (⦅ c ⦆ t ∷ s) (1+ θ) =
let Δ₁ , Δ₂ , s₁ , s₂ , θ′ = split-subst s θ in
let E₁ , E₂ , c₁ , c₂ , c′ = min-Cover c θ′ in
_ , _ , ⦅ c₁ ⦆ t ∷ s₁ , ⦅ c₂ ⦆ t ∷ s₂ , c′
split-subst (⦅ c ⦆ t ∷ s) (1+ˡ θ) =
let Δ₁ , Δ₂ , s₁ , s₂ , θ′ = split-subst s θ in
let E₁ , c₁ , c′ = min-Coverˡ c θ′ in
_ , _ , ⦅ c₁ ⦆ t ∷ s₁ , s₂ , c′
split-subst (⦅ c ⦆ t ∷ s) (1+ʳ θ) =
let Δ₁ , Δ₂ , s₁ , s₂ , θ′ = split-subst s θ in
let E₂ , c₂ , c′ = min-Coverʳ c θ′ in
_ , _ , s₁ , ⦅ c₂ ⦆ t ∷ s₂ , c′
coverʳ : {Γ : Context} → Cover Γ O Γ
coverʳ {O} = O
coverʳ {1+ Γ} = 1+ʳ coverʳ {Γ}
1+-rsubst : {Γ Δ : Context} → RSubst Γ Δ → RSubst (1+ Γ) (1+ Δ)
1+-rsubst θ = ⦅ 1+ˡ coverʳ ⦆ Var one ∷ θ
extend-subst : {Γ Δ Γ₁ : Context} → RSubst Γ Δ → Extend₁ Γ Γ₁ → ∃[ Δ₁ ] RSubst Γ₁ Δ₁ × Extend₁ Δ Δ₁
extend-subst s extend = _ , 1+-rsubst s , extend
extend-subst s refl = _ , s , refl
rsubst : {Γ₁ Γ₂ : Context} → RSubst Γ₁ Γ₂ → RTerm Γ₁ → RTerm Γ₂
rsubst s (Var one) = inv-one s
rsubst s (App θ t₁ t₂) =
let _ , _ , s₁ , s₂ , θ′ = split-subst s θ in
App θ′ (rsubst s₁ t₁) (rsubst s₂ t₂)
rsubst s (Lam θ t) =
let _ , s₁ , θ₁ = extend-subst s θ in
Lam θ₁ (rsubst s₁ t)
subst : {Γ₁ Γ₂ : Context} → Subst Γ₁ Γ₂ → Term Γ₁ → Term Γ₂
subst s (Weaken θ t) with weaken-subst s θ
... | Weaken θ′ s′ = Weaken θ′ (rsubst s′ t)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment