Skip to content

Instantly share code, notes, and snippets.

@FrozenWinters

FrozenWinters/modalNbE.agda

Last active November 1, 2022 14:50
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save FrozenWinters/7c333e0c7f5d6762199eebdc0736175f to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save FrozenWinters/7c333e0c7f5d6762199eebdc0736175f to your computer and use it in GitHub Desktop.
Download ZIP
NbE for K modal logic
Raw
modalNbE.agda
{-# OPTIONS --cubical #-}
module modalNbE where
open import Agda.Primitive using (Level; lzero; lsuc; _βŠ”_)
open import Cubical.Foundations.Everything renaming (cong to ap)
open import Cubical.Data.Sigma
-- Data Structures
private
variable
β„“ ℓ₁ β„“β‚‚ ℓ₃ β„“β‚„ β„“β‚… ℓ₆ : Level
infixl 20 _⊹_
data 𝐢𝑑π‘₯ (ty : Type β„“) : Type β„“ where
βˆ… : 𝐢𝑑π‘₯ ty
_⊹_ : 𝐢𝑑π‘₯ ty β†’ ty β†’ 𝐢𝑑π‘₯ ty
data π‘‰π‘Žπ‘Ÿ (ty : Type β„“) : (Ξ“ : 𝐢𝑑π‘₯ ty) (A : ty) β†’ Type β„“ where
𝑧𝑣 : {Ξ“ : 𝐢𝑑π‘₯ ty} {A : ty} β†’ π‘‰π‘Žπ‘Ÿ ty (Ξ“ ⊹ A) A
𝑠𝑣 : {Ξ“ : 𝐢𝑑π‘₯ ty} {A B : ty} β†’ π‘‰π‘Žπ‘Ÿ ty Ξ“ A β†’ π‘‰π‘Žπ‘Ÿ ty (Ξ“ ⊹ B) A
infixl 20 _βŠ•_
data 𝐸𝑙𝑠 {ty : Type ℓ₁} (el : ty β†’ Type β„“β‚‚) : (Ξ“ : 𝐢𝑑π‘₯ ty) β†’ Type (ℓ₁ βŠ” β„“β‚‚) where
! : 𝐸𝑙𝑠 el βˆ…
_βŠ•_ : {Ξ“ : 𝐢𝑑π‘₯ ty} {A : ty} β†’ 𝐸𝑙𝑠 el Ξ“ β†’ el A β†’ 𝐸𝑙𝑠 el (Ξ“ ⊹ A)
π‘‡π‘šπ‘  : {ty : Type ℓ₁} (tm : 𝐢𝑑π‘₯ ty β†’ ty β†’ Type β„“β‚‚) (Ξ“ Ξ” : 𝐢𝑑π‘₯ ty) β†’ Type (ℓ₁ βŠ” β„“β‚‚)
π‘‡π‘šπ‘  tm Ξ“ Ξ” = 𝐸𝑙𝑠 (tm Ξ“) Ξ”
𝑅𝑒𝑛 : (ty : Type β„“) β†’ 𝐢𝑑π‘₯ ty β†’ 𝐢𝑑π‘₯ ty β†’ Type β„“
𝑅𝑒𝑛 ty = π‘‡π‘šπ‘  (π‘‰π‘Žπ‘Ÿ ty)
map𝐢𝑑π‘₯ : {ty₁ : Type ℓ₁} {tyβ‚‚ : Type β„“β‚‚} (f : ty₁ β†’ tyβ‚‚) (Ξ“ : 𝐢𝑑π‘₯ ty₁) β†’ 𝐢𝑑π‘₯ tyβ‚‚
map𝐢𝑑π‘₯ f βˆ… = βˆ…
map𝐢𝑑π‘₯ f (Ξ“ ⊹ A) = map𝐢𝑑π‘₯ f Ξ“ ⊹ f A
map𝐸𝑙𝑠 : {ty : Type ℓ₁} {Ξ” : 𝐢𝑑π‘₯ ty} {el₁ : ty β†’ Type β„“β‚‚} {elβ‚‚ : ty β†’ Type ℓ₃}
(f : {A : ty} β†’ el₁ A β†’ elβ‚‚ A) β†’ 𝐸𝑙𝑠 el₁ Ξ” β†’ 𝐸𝑙𝑠 elβ‚‚ Ξ”
map𝐸𝑙𝑠 f ! = !
map𝐸𝑙𝑠 f (Οƒ βŠ• t) = map𝐸𝑙𝑠 f Οƒ βŠ• f t
π𝐸𝑙𝑠 : {ty : Type ℓ₁} {el : ty β†’ Type β„“β‚‚} {Ξ“ : 𝐢𝑑π‘₯ ty} {A : ty} β†’
𝐸𝑙𝑠 el (Ξ“ ⊹ A) β†’ 𝐸𝑙𝑠 el Ξ“
π𝐸𝑙𝑠 (Οƒ βŠ• t) = Οƒ
𝑧𝐸𝑙𝑠 : {ty : Type ℓ₁} {el : ty β†’ Type β„“β‚‚} {Ξ“ : 𝐢𝑑π‘₯ ty} {A : ty} β†’
𝐸𝑙𝑠 el (Ξ“ ⊹ A) β†’ el A
𝑧𝐸𝑙𝑠 (Οƒ βŠ• t) = t
derive : {ty : Type ℓ₁} {el : ty β†’ Type β„“β‚‚} {Ξ“ : 𝐢𝑑π‘₯ ty} {A : ty} β†’
𝐸𝑙𝑠 el Ξ“ β†’ π‘‰π‘Žπ‘Ÿ ty Ξ“ A β†’ el A
derive Οƒ 𝑧𝑣 = 𝑧𝐸𝑙𝑠 Οƒ
derive Οƒ (𝑠𝑣 v) = derive (π𝐸𝑙𝑠 Οƒ) v
_⊹⊹_ : {ty : Type β„“} β†’ 𝐢𝑑π‘₯ ty β†’ 𝐢𝑑π‘₯ ty β†’ 𝐢𝑑π‘₯ ty
Ξ“ ⊹⊹ βˆ… = Ξ“
Ξ“ ⊹⊹ (Ξ” ⊹ A) = (Ξ“ ⊹⊹ Ξ”) ⊹ A
_βŠ•βŠ•-f_ : {ty : Type ℓ₁} {el : ty β†’ Type β„“β‚‚} {Ξ“ Ξ” : 𝐢𝑑π‘₯ ty} {f : ty β†’ ty} β†’
𝐸𝑙𝑠 el (map𝐢𝑑π‘₯ f Ξ“) β†’ 𝐸𝑙𝑠 el (map𝐢𝑑π‘₯ f Ξ”) β†’ 𝐸𝑙𝑠 el (map𝐢𝑑π‘₯ f (Ξ“ ⊹⊹ Ξ”))
_βŠ•βŠ•-f_ {Ξ” = βˆ…} Οƒ ! = Οƒ
_βŠ•βŠ•-f_ {Ξ” = Ξ” ⊹ A} Οƒ (Ο„ βŠ• t) = (Οƒ βŠ•βŠ•-f Ο„) βŠ• t
module _ {ty : Type β„“} where
private
ctx = 𝐢𝑑π‘₯ ty
ren = 𝑅𝑒𝑛 ty
var = π‘‰π‘Žπ‘Ÿ ty
W₁𝑅𝑒𝑛 : {Ξ“ Ξ” : ctx} (A : ty) β†’ ren Ξ“ Ξ” β†’ ren (Ξ“ ⊹ A) Ξ”
W₁𝑅𝑒𝑛 A = map𝐸𝑙𝑠 𝑠𝑣
W₂𝑅𝑒𝑛 : {Ξ“ Ξ” : ctx} (A : ty) β†’ ren Ξ“ Ξ” β†’ ren (Ξ“ ⊹ A) (Ξ” ⊹ A)
W₂𝑅𝑒𝑛 A Οƒ = W₁𝑅𝑒𝑛 A Οƒ βŠ• 𝑧𝑣
id𝑅𝑒𝑛 : (Ξ“ : ctx) β†’ ren Ξ“ Ξ“
id𝑅𝑒𝑛 βˆ… = !
id𝑅𝑒𝑛 (Ξ“ ⊹ A) = W₂𝑅𝑒𝑛 A (id𝑅𝑒𝑛 Ξ“)
π𝑅𝑒𝑛 : {Ξ“ : ctx} {A : ty} β†’ ren (Ξ“ ⊹ A) Ξ“
π𝑅𝑒𝑛 {Ξ“} {A} = π𝐸𝑙𝑠 (id𝑅𝑒𝑛 (Ξ“ ⊹ A))
π₁𝑅𝑒𝑛 : (Ξ“ Ξ” : ctx) β†’ ren (Ξ“ ⊹⊹ Ξ”) Ξ“
π₁𝑅𝑒𝑛 Ξ“ βˆ… = id𝑅𝑒𝑛 Ξ“
π₁𝑅𝑒𝑛 Ξ“ (Ξ” ⊹ A) = W₁𝑅𝑒𝑛 A (π₁𝑅𝑒𝑛 Ξ“ Ξ”)
π₂𝑅𝑒𝑛 : (Ξ“ Ξ” : ctx) β†’ ren (Ξ“ ⊹⊹ Ξ”) Ξ”
π₂𝑅𝑒𝑛 Ξ“ βˆ… = !
π₂𝑅𝑒𝑛 Ξ“ (Ξ” ⊹ A) = W₂𝑅𝑒𝑛 A (π₂𝑅𝑒𝑛 Ξ“ Ξ”)
infix 30 _[_]𝑅
_[_]𝑅 : {Ξ“ Ξ” : ctx} {A : ty} β†’ var Ξ” A β†’ ren Ξ“ Ξ” β†’ var Ξ“ A
v [ Οƒ ]𝑅 = derive Οƒ v
infixl 30 _βˆ˜π‘…π‘’π‘›_
_βˆ˜π‘…π‘’π‘›_ : {Ξ“ Ξ” Ξ£ : ctx} β†’ ren Ξ” Ξ£ β†’ ren Ξ“ Ξ” β†’ ren Ξ“ Ξ£
Οƒ βˆ˜π‘…π‘’π‘› Ο„ = map𝐸𝑙𝑠 _[ Ο„ ]𝑅 Οƒ
-- Syntax
infixr 20 _β‡’_
data Ty : Type where
Base : Ty
_β‡’_ : Ty β†’ Ty β†’ Ty
β–‘ : Ty β†’ Ty
Ctx = 𝐢𝑑π‘₯ Ty
Var = π‘‰π‘Žπ‘Ÿ Ty
Ren = 𝑅𝑒𝑛 Ty
infixl 30 Box_With_
data Tm : Ctx β†’ Ty β†’ Type
Tms = π‘‡π‘šπ‘  Tm
data Tm where
V : {Ξ“ : Ctx} {A : Ty} β†’ Var Ξ“ A β†’ Tm Ξ“ A
Lam : {Ξ“ : Ctx} {A B : Ty} β†’ Tm (Ξ“ ⊹ A) B β†’ Tm Ξ“ (A β‡’ B)
App : {Ξ“ : Ctx} {A B : Ty} β†’ Tm Ξ“ (A β‡’ B) β†’ Tm Ξ“ A β†’ Tm Ξ“ B
Box_With_ : {Ξ“ Ξ” : Ctx} {A : Ty} β†’
Tm Ξ” A β†’ Tms Ξ“ (map𝐢𝑑π‘₯ β–‘ Ξ”) β†’ Tm Ξ“ (β–‘ A)
-- NbE
data Ne : Ctx β†’ Ty β†’ Type
data Nf : Ctx β†’ Ty β†’ Type
Nes = π‘‡π‘šπ‘  Ne
infixl 30 BOX_WITH_
data Ne where
VN : {Ξ“ : Ctx} {A : Ty} β†’ Var Ξ“ A β†’ Ne Ξ“ A
APP : {Ξ“ : Ctx} {A B : Ty} β†’ Ne Ξ“ (A β‡’ B) β†’ Nf Ξ“ A β†’ Ne Ξ“ B
data Nf where
NEU : {Ξ“ : Ctx} β†’ Ne Ξ“ Base β†’ Nf Ξ“ Base
LAM : {Ξ“ : Ctx} {A B : Ty} β†’ Nf (Ξ“ ⊹ A) B β†’ Nf Ξ“ (A β‡’ B)
BOX_WITH_ : {Ξ“ Ξ” : Ctx} {A : Ty} β†’
Nf Ξ” A β†’ Nes Ξ“ (map𝐢𝑑π‘₯ β–‘ Ξ”) β†’ Nf Ξ“ (β–‘ A)
infixl 20 _[_]Ne _[_]Nf
{-# TERMINATING #-}
_[_]Ne : {Ξ” Ξ“ : Ctx} {A : Ty} β†’ Ne Ξ“ A β†’ Ren Ξ” Ξ“ β†’ Ne Ξ” A
_[_]Nf : {Ξ” Ξ“ : Ctx} {A : Ty} β†’ Nf Ξ“ A β†’ Ren Ξ” Ξ“ β†’ Nf Ξ” A
VN v [ Οƒ ]Ne = VN (derive Οƒ v)
APP M N [ Οƒ ]Ne = APP (M [ Οƒ ]Ne) (N [ Οƒ ]Nf)
NEU M [ Οƒ ]Nf = NEU (M [ Οƒ ]Ne)
LAM {A = A} N [ Οƒ ]Nf = LAM (N [ W₂𝑅𝑒𝑛 A Οƒ ]Nf)
BOX N WITH Ο„ [ Οƒ ]Nf = BOX N WITH (map𝐸𝑙𝑠 _[ Οƒ ]Ne Ο„)
_∘NeR_ : {Ξ“ Ξ” Ξ£ : Ctx} β†’ Nes Ξ” Ξ£ β†’ Ren Ξ“ Ξ” β†’ Nes Ξ“ Ξ£
Οƒ ∘NeR Ο„ = map𝐸𝑙𝑠 _[ Ο„ ]Ne Οƒ
El : Ctx β†’ Ty β†’ Type
El Ξ“ Base = Nf Ξ“ Base
El Ξ“ (A β‡’ B) = {Ξ” : Ctx} β†’ Ren Ξ” Ξ“ β†’ El Ξ” A β†’ El Ξ” B
El Ξ“ (β–‘ A) = Ξ£ Ctx (Ξ» Ξ” β†’ Nes Ξ“ (map𝐢𝑑π‘₯ β–‘ Ξ”) Γ— El Ξ” A)
Els : Ctx β†’ Ctx β†’ Type
Els Ξ” Ξ“ = π‘‡π‘šπ‘  El Ξ” Ξ“
q : {Ξ“ : Ctx} {A : Ty} β†’ El Ξ“ A β†’ Nf Ξ“ A
u : {Ξ“ : Ctx} {A : Ty} β†’ Ne Ξ“ A β†’ El Ξ“ A
q {A = Base} N = N
q {A = A β‡’ B} 𝒻 = LAM (q (𝒻 π𝑅𝑒𝑛 (u (VN 𝑧𝑣))))
q {A = β–‘ A} (Ξ” , Οƒ , π“ˆ) = BOX q π“ˆ WITH Οƒ
u {A = Base} M = NEU M
u {A = A β‡’ B} M Οƒ π“ˆ = u (APP (M [ Οƒ ]Ne) (q π“ˆ))
u {A = β–‘ A} M = (βˆ… ⊹ A) , (! βŠ• M), u (VN 𝑧𝑣)
_[_]El : {Ξ” Ξ“ : Ctx} {A : Ty} β†’ El Ξ“ A β†’ Ren Ξ” Ξ“ β†’ El Ξ” A
_[_]El {A = Base} N Οƒ = N [ Οƒ ]Nf
_[_]El {A = A β‡’ B} 𝒻 Οƒ Ο„ π“ˆ = 𝒻 (Οƒ βˆ˜π‘…π‘’π‘› Ο„) π“ˆ
_[_]El {A = β–‘ A} (Ξ” , Ο„ , π“ˆ) Οƒ = Ξ” , Ο„ ∘NeR Οƒ , π“ˆ
unify : {Ξ“ Ξ” : Ctx} β†’ Els Ξ“ (map𝐢𝑑π‘₯ β–‘ Ξ”) β†’
Ξ£ Ctx (Ξ» Ξ£ β†’ Nes Ξ“ (map𝐢𝑑π‘₯ β–‘ Ξ£) Γ— Els Ξ£ Ξ”)
unify {Ξ” = βˆ…} ! = βˆ… , ! , !
unify {Ξ” = _ ⊹ _} (π“ˆs βŠ• π“ˆ) with unify π“ˆs | π“ˆ
... | (Ξ“ , Οƒ , π“ˆs) | (Ξ” , Ο„ , π“ˆ) =
(Ξ“ ⊹⊹ Ξ”) , (Οƒ βŠ•βŠ•-f Ο„) , (map𝐸𝑙𝑠 _[ π₁𝑅𝑒𝑛 Ξ“ Ξ” ]El π“ˆs) βŠ• (π“ˆ [ π₂𝑅𝑒𝑛 Ξ“ Ξ” ]El)
{-# TERMINATING #-}
eval : {Ξ“ Ξ” : Ctx} {A : Ty} β†’ Tm Ξ” A β†’ Els Ξ“ Ξ” β†’ El Ξ“ A
eval (V v) π“ˆs = derive π“ˆs v
eval (Lam t) π“ˆs Οƒ π“ˆ = eval t (map𝐸𝑙𝑠 _[ Οƒ ]El π“ˆs βŠ• π“ˆ)
eval {Ξ“} (App t s) π“ˆs = eval t π“ˆs (id𝑅𝑒𝑛 Ξ“) (eval s π“ˆs)
eval (Box t With Οƒ) π“ˆs with unify (map𝐸𝑙𝑠 (Ξ» s β†’ eval s π“ˆs) Οƒ)
... | (Ξ” , Ο„ , 𝓉s) = Ξ” , Ο„ , eval t 𝓉s
norm : {Ξ“ : Ctx} {A : Ty} β†’ Tm Ξ“ A β†’ Nf Ξ“ A
norm {Ξ“} t = q (eval t (map𝐸𝑙𝑠 (u ∘ VN) (id𝑅𝑒𝑛 Ξ“)))
-- Some tests
{-# TERMINATING #-}
ΞΉNe : {Ξ“ : Ctx} {A : Ty} β†’ Ne Ξ“ A β†’ Tm Ξ“ A
ΞΉNf : {Ξ“ : Ctx} {A : Ty} β†’ Nf Ξ“ A β†’ Tm Ξ“ A
ΞΉNe (VN v) = V v
ΞΉNe (APP M N) = App (ΞΉNe M) (ΞΉNf N)
ΞΉNf (NEU M) = ΞΉNe M
ΞΉNf (LAM N) = Lam (ΞΉNf N)
ΞΉNf (BOX N WITH Οƒ) = Box (ΞΉNf N) With map𝐸𝑙𝑠 ΞΉNe Οƒ
K : {Ξ“ : Ctx} {A B : Ty} β†’ Tm Ξ“ (β–‘ (A β‡’ B) β‡’ β–‘ A β‡’ β–‘ B)
K = Lam (Lam (Box (App (V (𝑠𝑣 𝑧𝑣)) (V 𝑧𝑣)) With (! βŠ• V (𝑠𝑣 𝑧𝑣) βŠ• V 𝑧𝑣)))
eg0 = K {βˆ…} {Base} {Base}
val0 = ΞΉNf (norm eg0)
eg1 : Tm (βˆ… ⊹ β–‘ (Base β‡’ Base) ⊹ β–‘ Base) (β–‘ Base)
eg1 = Box (App (V (𝑠𝑣 𝑧𝑣)) (V 𝑧𝑣)) With
(! βŠ• V (𝑠𝑣 𝑧𝑣) βŠ• Box App (V (𝑠𝑣 𝑧𝑣)) (V 𝑧𝑣) With (! βŠ• V (𝑠𝑣 𝑧𝑣) βŠ• V 𝑧𝑣))
val1 = ΞΉNf (norm eg1)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment