Created
February 17, 2025 20:00
-
-
Save Lysxia/7acb28e556bc8c38677a14f843e1a360 to your computer and use it in GitHub Desktop.
CoDebruijn scoped syntax of untyped lambda calculus
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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