michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

setup for bisimulation

Browse source
This commit is contained in:
wadler 2018-07-03 12:51:44 -03:00
parent d7348182b2
commit 84f79d3ab7
2 changed files with 204 additions and 165 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/plta/DeBruijn.lagda
View file

@ -330,13 +330,13 @@ judgements:
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "s" ⦂ `ℕ ⇒ `ℕ `` * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "s" ⦂ `ℕ ⇒ `ℕ ``
They correspond to the following inherently-typed variables. They correspond to the following inherently-typed variables.
-- \begin{code} \begin{code}
_ : ∅ , `ℕ ⇒ `ℕ , `ℕ ∋ `ℕ _ : ∅ , `ℕ ⇒ `ℕ , `ℕ ∋ `ℕ
_ = Z _ = Z
_ : ∅ , `ℕ ⇒ `ℕ , `ℕ ∋ `ℕ ⇒ `ℕ _ : ∅ , `ℕ ⇒ `ℕ , `ℕ ∋ `ℕ ⇒ `ℕ
_ = S Z _ = S Z
-- \end{code} \end{code}
In the given context, `"z"` is represented by `Z`, and `"s"` by `S Z`. In the given context, `"z"` is represented by `Z`, and `"s"` by `S Z`.
### Terms and the typing judgement ### Terms and the typing judgement

365
src/plta/More.lagda
View file

@ -18,7 +18,6 @@ description will be informal. We show how to formalise a few
of the constructs, but leave the rest as an exercise for the of the constructs, but leave the rest as an exercise for the
reader. reader.
## Imports ## Imports
\begin{code} \begin{code}
@ -37,17 +36,20 @@ open import Relation.Nullary using (¬_; Dec; yes; no)
## Syntax ## Syntax
\begin{code} \begin{code}
infixl 6 _,_
infix 4 _⊢_ infix 4 _⊢_
infix 4 _∋_ infix 4 _∋_
infixr 5 _⇒_ infixl 5 _,_
infixr 6 _`⊎_
infixr 7 _`×_
infix 4 ƛ_ infixr 7 _⇒_
infix 4 μ_ infixr 8 _`⊎_
infixl 5 _·_ infixr 9 _`×_
infix 6 S_
infix 5 ƛ_
infix 5 μ_
infixl 7 _·_
infix 8 `suc_
infix 9 `_
infix 9 S_
data Type : Set where data Type : Set where
`ℕ : Type `ℕ : Type
@ -59,7 +61,7 @@ data Type : Set where
`List : Type → Type `List : Type → Type
data Env : Set where data Env : Set where
ε : Env ∅ : Env
_,_ : Env → Type → Env _,_ : Env → Type → Env
data _∋_ : Env → Type → Set where data _∋_ : Env → Type → Set where
@ -75,7 +77,7 @@ data _∋_ : Env → Type → Set where
data _⊢_ : Env → Type → Set where data _⊢_ : Env → Type → Set where
⌊_⌋ : ∀ {Γ} {A} `_ : ∀ {Γ} {A}
→ Γ ∋ A → Γ ∋ A
------ ------
→ Γ ⊢ A → Γ ⊢ A
@ -95,7 +97,7 @@ data _⊢_ : Env → Type → Set where
---------- ----------
→ Γ ⊢ `ℕ → Γ ⊢ `ℕ
`suc : ∀ {Γ} `suc_ : ∀ {Γ}
→ Γ ⊢ `ℕ → Γ ⊢ `ℕ
------- -------
→ Γ ⊢ `ℕ → Γ ⊢ `ℕ
@ -190,69 +192,69 @@ Simultaneous substitution, a la McBride
\begin{code} \begin{code}
ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ∋ B) ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ∋ B)
ext σ Z = Z ext ρ Z = Z
ext σ (S x) = S (σ x) ext ρ (S x) = S (ρ x)
rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A} → Γ ⊢ A → Δ ⊢ A) rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
rename σ (⌊ n ⌋) = ⌊ σ n ⌋ rename ρ (` x) = ` (ρ x)
rename σ (ƛ N) = ƛ (rename (ext σ) N) rename ρ (ƛ N) = ƛ (rename (ext ρ) N)
rename σ (L · M) = (rename σ L) · (rename σ M) rename ρ (L · M) = (rename ρ L) · (rename ρ M)
rename σ (`zero) = `zero rename ρ (`zero) = `zero
rename σ (`suc M) = `suc (rename σ M) rename ρ (`suc M) = `suc (rename ρ M)
rename σ (`caseℕ L M N) = `caseℕ (rename σ L) (rename σ M) (rename (ext σ) N) rename ρ (`caseℕ L M N) = `caseℕ (rename ρ L) (rename ρ M) (rename (ext ρ) N)
rename σ (μ N) = μ (rename (ext σ) N) rename ρ (μ N) = μ (rename (ext ρ) N)
rename σ `⟨ M , N ⟩ = `⟨ rename σ M , rename σ N ⟩ rename ρ `⟨ M , N ⟩ = `⟨ rename ρ M , rename ρ N ⟩
rename σ (`proj₁ L) = `proj₁ (rename σ L) rename ρ (`proj₁ L) = `proj₁ (rename ρ L)
rename σ (`proj₂ L) = `proj₂ (rename σ L) rename ρ (`proj₂ L) = `proj₂ (rename ρ L)
rename σ (`inj₁ M) = `inj₁ (rename σ M) rename ρ (`inj₁ M) = `inj₁ (rename ρ M)
rename σ (`inj₂ N) = `inj₂ (rename σ N) rename ρ (`inj₂ N) = `inj₂ (rename ρ N)
rename σ (`case⊎ L M N) = `case⊎ (rename σ L) (rename (ext σ) M) (rename (ext σ) N) rename ρ (`case⊎ L M N) = `case⊎ (rename ρ L) (rename (ext ρ) M) (rename (ext ρ) N)
rename σ `tt = `tt rename ρ `tt = `tt
rename σ (`case⊥ L) = `case⊥ (rename σ L) rename ρ (`case⊥ L) = `case⊥ (rename ρ L)
rename σ `[] = `[] rename ρ `[] = `[]
rename σ (M `∷ N) = (rename σ M) `∷ (rename σ N) rename ρ (M `∷ N) = (rename ρ M) `∷ (rename ρ N)
rename σ (`caseL L M N) = `caseL (rename σ L) (rename σ M) (rename (ext (ext σ)) N) rename ρ (`caseL L M N) = `caseL (rename ρ L) (rename ρ M) (rename (ext (ext ρ)) N)
rename σ (`let M N) = `let (rename σ M) (rename (ext σ) N) rename ρ (`let M N) = `let (rename ρ M) (rename (ext ρ) N)
\end{code} \end{code}
## Substitution ## Substitution
\begin{code} \begin{code}
exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ⊢ B) exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ⊢ B)
exts ρ Z = ⌊ Z ⌋ exts σ Z = ` Z
exts ρ (S x) = rename S_ (ρ x) exts σ (S x) = rename S_ (σ x)
subst : ∀ {Γ Δ} → (∀ {C} → Γ ∋ C → Δ ⊢ C) → (∀ {C} → Γ ⊢ C → Δ ⊢ C) subst : ∀ {Γ Δ} → (∀ {C} → Γ ∋ C → Δ ⊢ C) → (∀ {C} → Γ ⊢ C → Δ ⊢ C)
subst ρ (⌊ k ⌋) = ρ k subst σ (` k) = σ k
subst ρ (ƛ N) = ƛ (subst (exts ρ) N) subst σ (ƛ N) = ƛ (subst (exts σ) N)
subst ρ (L · M) = (subst ρ L) · (subst ρ M) subst σ (L · M) = (subst σ L) · (subst σ M)
subst ρ (`zero) = `zero subst σ (`zero) = `zero
subst ρ (`suc M) = `suc (subst ρ M) subst σ (`suc M) = `suc (subst σ M)
subst ρ (`caseℕ L M N) = `caseℕ (subst ρ L) (subst ρ M) (subst (exts ρ) N) subst σ (`caseℕ L M N) = `caseℕ (subst σ L) (subst σ M) (subst (exts σ) N)
subst ρ (μ N) = μ (subst (exts ρ) N) subst σ (μ N) = μ (subst (exts σ) N)
subst ρ `⟨ M , N ⟩ = `⟨ subst ρ M , subst ρ N ⟩ subst σ `⟨ M , N ⟩ = `⟨ subst σ M , subst σ N ⟩
subst ρ (`proj₁ L) = `proj₁ (subst ρ L) subst σ (`proj₁ L) = `proj₁ (subst σ L)
subst ρ (`proj₂ L) = `proj₂ (subst ρ L) subst σ (`proj₂ L) = `proj₂ (subst σ L)
subst ρ (`inj₁ M) = `inj₁ (subst ρ M) subst σ (`inj₁ M) = `inj₁ (subst σ M)
subst ρ (`inj₂ N) = `inj₂ (subst ρ N) subst σ (`inj₂ N) = `inj₂ (subst σ N)
subst ρ (`case⊎ L M N) = `case⊎ (subst ρ L) (subst (exts ρ) M) (subst (exts ρ) N) subst σ (`case⊎ L M N) = `case⊎ (subst σ L) (subst (exts σ) M) (subst (exts σ) N)
subst ρ `tt = `tt subst σ `tt = `tt
subst ρ (`case⊥ L) = `case⊥ (subst ρ L) subst σ (`case⊥ L) = `case⊥ (subst σ L)
subst ρ `[] = `[] subst σ `[] = `[]
subst ρ (M `∷ N) = (subst ρ M) `∷ (subst ρ N) subst σ (M `∷ N) = (subst σ M) `∷ (subst σ N)
subst ρ (`caseL L M N) = `caseL (subst ρ L) (subst ρ M) (subst (exts (exts ρ)) N) subst σ (`caseL L M N) = `caseL (subst σ L) (subst σ M) (subst (exts (exts σ)) N)
subst ρ (`let M N) = `let (subst ρ M) (subst (exts ρ) N) subst σ (`let M N) = `let (subst σ M) (subst (exts σ) N)
_[_] : ∀ {Γ A B} _[_] : ∀ {Γ A B}
→ Γ , A ⊢ B → Γ , A ⊢ B
→ Γ ⊢ A → Γ ⊢ A
------------ ------------
→ Γ ⊢ B → Γ ⊢ B
_[_] {Γ} {A} N V = subst {Γ , A} {Γ} ρ N _[_] {Γ} {A} N V = subst {Γ , A} {Γ} σ N
where where
ρ : ∀ {B} → Γ , A ∋ B → Γ ⊢ B σ : ∀ {B} → Γ , A ∋ B → Γ ⊢ B
ρ Z = V σ Z = V
ρ (S x) = ⌊ x ⌋ σ (S x) = ` x
_[_][_] : ∀ {Γ A B C} _[_][_] : ∀ {Γ A B C}
→ Γ , A , B ⊢ C → Γ , A , B ⊢ C
@ -260,12 +262,12 @@ _[_][_] : ∀ {Γ A B C}
→ Γ ⊢ B → Γ ⊢ B
--------------- ---------------
→ Γ ⊢ C → Γ ⊢ C
_[_][_] {Γ} {A} {B} N V W = subst {Γ , A , B} {Γ} ρ N _[_][_] {Γ} {A} {B} N V W = subst {Γ , A , B} {Γ} σ N
where where
ρ : ∀ {C} → Γ , A , B ∋ C → Γ ⊢ C σ : ∀ {C} → Γ , A , B ∋ C → Γ ⊢ C
ρ Z = W σ Z = W
ρ (S Z) = V σ (S Z) = V
ρ (S (S x)) = ⌊ x ⌋ σ (S (S x)) = ` x
\end{code} \end{code}
## Value ## Value
@ -323,172 +325,172 @@ not fixed by the given arguments.
## Reduction step ## Reduction step
\begin{code} \begin{code}
infix 2 _⟶_ infix 2 _—→_
data _⟶_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A} ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
→ L ⟶ L′ → L —→ L′
----------------- -----------------
→ L · M ⟶ L′ · M → L · M —→ L′ · M
ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A} ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
→ Value V → Value V
→ M ⟶ M′ → M —→ M′
----------------- -----------------
→ V · M ⟶ V · M′ → V · M —→ V · M′
β-⇒ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A} β-⇒ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
→ Value W → Value W
--------------------- ---------------------
→ (ƛ N) · W ⟶ N [ W ] → (ƛ N) · W —→ N [ W ]
ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ} ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
→ M ⟶ M′ → M —→ M′
------------------- -------------------
→ `suc M ⟶ `suc M′ → `suc M —→ `suc M′
ξ-caseℕ : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A} ξ-caseℕ : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
→ L ⟶ L′ → L —→ L′
------------------------------- -------------------------------
→ `caseℕ L M N ⟶ `caseℕ L′ M N → `caseℕ L M N —→ `caseℕ L′ M N
β-ℕ₁ : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A} β-ℕ₁ : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
----------------------- -----------------------
→ `caseℕ `zero M N ⟶ M → `caseℕ `zero M N —→ M
β-ℕ₂ : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A} β-ℕ₂ : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
→ Value V → Value V
-------------------------------- --------------------------------
→ `caseℕ (`suc V) M N ⟶ N [ V ] → `caseℕ (`suc V) M N —→ N [ V ]
β-μ : ∀ {Γ A} {N : Γ , A ⊢ A} β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
------------------ ------------------
→ μ N ⟶ N [ μ N ] → μ N —→ N [ μ N ]
ξ-⟨,⟩₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ ⊢ B} ξ-⟨,⟩₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ ⊢ B}
→ M ⟶ M′ → M —→ M′
-------------------------- --------------------------
→ `⟨ M , N ⟩ ⟶ `⟨ M′ , N ⟩ → `⟨ M , N ⟩ —→ `⟨ M′ , N ⟩
ξ-⟨,⟩₂ : ∀ {Γ A B} {V : Γ ⊢ A} {N N′ : Γ ⊢ B} ξ-⟨,⟩₂ : ∀ {Γ A B} {V : Γ ⊢ A} {N N′ : Γ ⊢ B}
→ Value V → Value V
→ N ⟶ N′ → N —→ N′
-------------------------- --------------------------
→ `⟨ V , N ⟩ ⟶ `⟨ V , N′ ⟩ → `⟨ V , N ⟩ —→ `⟨ V , N′ ⟩
ξ-proj₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B} ξ-proj₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B}
→ L ⟶ L′ → L —→ L′
----------------------- -----------------------
→ `proj₁ L ⟶ `proj₁ L′ → `proj₁ L —→ `proj₁ L′
ξ-proj₂ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B} ξ-proj₂ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B}
→ L ⟶ L′ → L —→ L′
----------------------- -----------------------
→ `proj₂ L ⟶ `proj₂ L′ → `proj₂ L —→ `proj₂ L′
β-×₁ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B} β-×₁ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
→ Value V → Value V
→ Value W → Value W
------------------------ ------------------------
→ `proj₁ `⟨ V , W ⟩ ⟶ V → `proj₁ `⟨ V , W ⟩ —→ V
β-×₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B} β-×₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
→ Value V → Value V
→ Value W → Value W
------------------------ ------------------------
→ `proj₂ `⟨ V , W ⟩ ⟶ W → `proj₂ `⟨ V , W ⟩ —→ W
ξ-inj₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A} ξ-inj₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A}
→ M ⟶ M′ → M —→ M′
----------------------------- -----------------------------
→ `inj₁ {B = B} M ⟶ `inj₁ M′ → `inj₁ {B = B} M —→ `inj₁ M′
ξ-inj₂ : ∀ {Γ A B} {N N′ : Γ ⊢ B} ξ-inj₂ : ∀ {Γ A B} {N N′ : Γ ⊢ B}
→ N ⟶ N′ → N —→ N′
----------------------------- -----------------------------
→ `inj₂ {A = A} N ⟶ `inj₂ N′ → `inj₂ {A = A} N —→ `inj₂ N′
ξ-case⊎ : ∀ {Γ A B C} {L L′ : Γ ⊢ A `⊎ B} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C} ξ-case⊎ : ∀ {Γ A B C} {L L′ : Γ ⊢ A `⊎ B} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C}
→ L ⟶ L′ → L —→ L′
------------------------------- -------------------------------
→ `case⊎ L M N ⟶ `case⊎ L′ M N → `case⊎ L M N —→ `case⊎ L′ M N
β-⊎₁ : ∀ {Γ A B C} {V : Γ ⊢ A} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C} β-⊎₁ : ∀ {Γ A B C} {V : Γ ⊢ A} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C}
→ Value V → Value V
--------------------------------- ---------------------------------
→ `case⊎ (`inj₁ V) M N ⟶ M [ V ] → `case⊎ (`inj₁ V) M N —→ M [ V ]
β-⊎₂ : ∀ {Γ A B C} {W : Γ ⊢ B} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C} β-⊎₂ : ∀ {Γ A B C} {W : Γ ⊢ B} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C}
→ Value W → Value W
--------------------------------- ---------------------------------
→ `case⊎ (`inj₂ W) M N ⟶ N [ W ] → `case⊎ (`inj₂ W) M N —→ N [ W ]
ξ-case⊥ : ∀ {Γ A} {L L′ : Γ ⊢ `⊥} ξ-case⊥ : ∀ {Γ A} {L L′ : Γ ⊢ `⊥}
→ L ⟶ L′ → L —→ L′
------------------------------- -------------------------------
→ `case⊥ {A = A} L ⟶ `case⊥ L′ → `case⊥ {A = A} L —→ `case⊥ L′
ξ-∷₁ : ∀ {Γ A} {M M′ : Γ ⊢ A} {N : Γ ⊢ `List A} ξ-∷₁ : ∀ {Γ A} {M M′ : Γ ⊢ A} {N : Γ ⊢ `List A}
→ M ⟶ M′ → M —→ M′
------------------- -------------------
→ M `∷ N ⟶ M′ `∷ N → M `∷ N —→ M′ `∷ N
ξ-∷₂ : ∀ {Γ A} {V : Γ ⊢ A} {N N′ : Γ ⊢ `List A} ξ-∷₂ : ∀ {Γ A} {V : Γ ⊢ A} {N N′ : Γ ⊢ `List A}
→ Value V → Value V
→ N ⟶ N′ → N —→ N′
------------------- -------------------
→ V `∷ N ⟶ V `∷ N′ → V `∷ N —→ V `∷ N′
ξ-caseL : ∀ {Γ A B} {L L′ : Γ ⊢ `List A} {M : Γ ⊢ B} {N : Γ , A , `List A ⊢ B} ξ-caseL : ∀ {Γ A B} {L L′ : Γ ⊢ `List A} {M : Γ ⊢ B} {N : Γ , A , `List A ⊢ B}
→ L ⟶ L′ → L —→ L′
------------------------------- -------------------------------
→ `caseL L M N ⟶ `caseL L′ M N → `caseL L M N —→ `caseL L′ M N
β-List₁ : ∀ {Γ A B} {M : Γ ⊢ B} {N : Γ , A , `List A ⊢ B} β-List₁ : ∀ {Γ A B} {M : Γ ⊢ B} {N : Γ , A , `List A ⊢ B}
--------------------- ---------------------
→ `caseL `[] M N ⟶ M → `caseL `[] M N —→ M
β-List₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ `List A} β-List₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ `List A}
{M : Γ ⊢ B} {N : Γ , A , `List A ⊢ B} {M : Γ ⊢ B} {N : Γ , A , `List A ⊢ B}
→ Value V → Value V
→ Value W → Value W
------------------------------------- -------------------------------------
→ `caseL (V `∷ W) M N ⟶ N [ V ][ W ] → `caseL (V `∷ W) M N —→ N [ V ][ W ]
ξ-let : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ , A ⊢ B} ξ-let : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ , A ⊢ B}
→ M ⟶ M′ → M —→ M′
----------------------- -----------------------
→ `let M N ⟶ `let M′ N → `let M N —→ `let M′ N
β-let : ∀ {Γ A B} {V : Γ ⊢ A} {N : Γ , A ⊢ B} β-let : ∀ {Γ A B} {V : Γ ⊢ A} {N : Γ , A ⊢ B}
→ Value V → Value V
--------------------- ---------------------
→ `let V N ⟶ N [ V ] → `let V N —→ N [ V ]
\end{code} \end{code}
## Reflexive and transitive closure ## Reflexive and transitive closure
\begin{code} \begin{code}
infix 2 _⟶*_ infix 2 _—↠_
infix 1 begin_ infix 1 begin_
infixr 2 _⟶⟨_⟩_ infixr 2 _—→⟨_⟩_
infix 3 _∎ infix 3 _∎
data _⟶*_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
_∎ : ∀ {Γ A} (M : Γ ⊢ A) _∎ : ∀ {Γ A} (M : Γ ⊢ A)
-------- --------
→ M ⟶* M → M —↠ M
_⟶⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A} _—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
→ L ⟶ M → L —→ M
→ M ⟶* N → M —↠ N
--------- ---------
→ L ⟶* N → L —↠ N
begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A} → (M ⟶* N) → (M ⟶* N) begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A} → (M —↠ N) → (M —↠ N)
begin M⟶*N = M⟶*N begin M—↠N = M—↠N
\end{code} \end{code}
@ -496,33 +498,33 @@ begin M⟶*N = M⟶*N
Values do not reduce. Values do not reduce.
\begin{code} \begin{code}
Value-lemma : ∀ {Γ A} {M N : Γ ⊢ A} → Value M → ¬ (M ⟶ N) Value-lemma : ∀ {Γ A} {M N : Γ ⊢ A} → Value M → ¬ (M —→ N)
Value-lemma Fun () Value-lemma Fun ()
Value-lemma Zero () Value-lemma Zero ()
Value-lemma (Suc VM) (ξ-suc M⟶M′) = Value-lemma VM M⟶M′ Value-lemma (Suc VM) (ξ-suc M—→M′) = Value-lemma VM M—→M′
Value-lemma (Pair VM _) (ξ-⟨,⟩₁ M⟶M′) = Value-lemma VM M⟶M′ Value-lemma (Pair VM _) (ξ-⟨,⟩₁ M—→M′) = Value-lemma VM M—→M′
Value-lemma (Pair _ VN) (ξ-⟨,⟩₂ _ N⟶N′) = Value-lemma VN N⟶N′ Value-lemma (Pair _ VN) (ξ-⟨,⟩₂ _ N—→N′) = Value-lemma VN N—→N′
Value-lemma (Inj₁ VM) (ξ-inj₁ M⟶M′) = Value-lemma VM M⟶M′ Value-lemma (Inj₁ VM) (ξ-inj₁ M—→M′) = Value-lemma VM M—→M′
Value-lemma (Inj₂ VN) (ξ-inj₂ N⟶N′) = Value-lemma VN N⟶N′ Value-lemma (Inj₂ VN) (ξ-inj₂ N—→N′) = Value-lemma VN N—→N′
Value-lemma TT () Value-lemma TT ()
Value-lemma Nil () Value-lemma Nil ()
Value-lemma (Cons VM _) (ξ-∷₁ M⟶M′) = Value-lemma VM M⟶M′ Value-lemma (Cons VM _) (ξ-∷₁ M—→M′) = Value-lemma VM M—→M′
Value-lemma (Cons _ VN) (ξ-∷₂ _ N⟶N′) = Value-lemma VN N⟶N′ Value-lemma (Cons _ VN) (ξ-∷₂ _ N—→N′) = Value-lemma VN N—→N′
\end{code} \end{code}
As a corollary, terms that reduce are not values. As a corollary, terms that reduce are not values.
\begin{code} \begin{code}
⟶-corollary : ∀ {Γ A} {M N : Γ ⊢ A} → (M ⟶ N) → ¬ Value M —→-corollary : ∀ {Γ A} {M N : Γ ⊢ A} → (M —→ N) → ¬ Value M
⟶-corollary M⟶N VM = Value-lemma VM M⟶N —→-corollary M—→N VM = Value-lemma VM M—→N
\end{code} \end{code}
## Progress ## Progress
\begin{code} \begin{code}
data Progress {A} (M : ε ⊢ A) : Set where data Progress {A} (M : ∅ ⊢ A) : Set where
step : ∀ {N : ε ⊢ A} step : ∀ {N : ∅ ⊢ A}
→ M ⟶ N → M —→ N
------------- -------------
→ Progress M → Progress M
done : done :
@ -530,60 +532,60 @@ data Progress {A} (M : ε ⊢ A) : Set where
---------- ----------
→ Progress M → Progress M
progress : ∀ {A} → (M : ε ⊢ A) → Progress M progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M
progress ⌊ () ⌋ progress (` ())
progress (ƛ N) = done Fun progress (ƛ N) = done Fun
progress (L · M) with progress L progress (L · M) with progress L
... | step L⟶L′ = step (ξ-·₁ L⟶L′) ... | step L—→L′ = step (ξ-·₁ L—→L′)
... | done Fun with progress M ... | done Fun with progress M
... | step M⟶M′ = step (ξ-·₂ Fun M⟶M′) ... | step M—→M′ = step (ξ-·₂ Fun M—→M′)
... | done VM = step (β-⇒ VM) ... | done VM = step (β-⇒ VM)
progress (`zero) = done Zero progress (`zero) = done Zero
progress (`suc M) with progress M progress (`suc M) with progress M
... | step M⟶M′ = step (ξ-suc M⟶M′) ... | step M—→M′ = step (ξ-suc M—→M′)
... | done VM = done (Suc VM) ... | done VM = done (Suc VM)
progress (`caseℕ L M N) with progress L progress (`caseℕ L M N) with progress L
... | step L⟶L′ = step (ξ-caseℕ L⟶L′) ... | step L—→L′ = step (ξ-caseℕ L—→L′)
... | done Zero = step β-ℕ₁ ... | done Zero = step β-ℕ₁
... | done (Suc VL) = step (β-ℕ₂ VL) ... | done (Suc VL) = step (β-ℕ₂ VL)
progress (μ N) = step β-μ progress (μ N) = step β-μ
progress `⟨ M , N ⟩ with progress M progress `⟨ M , N ⟩ with progress M
... | step M⟶M′ = step (ξ-⟨,⟩₁ M⟶M′) ... | step M—→M′ = step (ξ-⟨,⟩₁ M—→M′)
... | done VM with progress N ... | done VM with progress N
... | step N⟶N′ = step (ξ-⟨,⟩₂ VM N⟶N′) ... | step N—→N′ = step (ξ-⟨,⟩₂ VM N—→N′)
... | done VN = done (Pair VM VN) ... | done VN = done (Pair VM VN)
progress (`proj₁ L) with progress L progress (`proj₁ L) with progress L
... | step L⟶L′ = step (ξ-proj₁ L⟶L′) ... | step L—→L′ = step (ξ-proj₁ L—→L′)
... | done (Pair VM VN) = step (β-×₁ VM VN) ... | done (Pair VM VN) = step (β-×₁ VM VN)
progress (`proj₂ L) with progress L progress (`proj₂ L) with progress L
... | step L⟶L′ = step (ξ-proj₂ L⟶L′) ... | step L—→L′ = step (ξ-proj₂ L—→L′)
... | done (Pair VM VN) = step (β-×₂ VM VN) ... | done (Pair VM VN) = step (β-×₂ VM VN)
progress (`inj₁ M) with progress M progress (`inj₁ M) with progress M
... | step M⟶M′ = step (ξ-inj₁ M⟶M′) ... | step M—→M′ = step (ξ-inj₁ M—→M′)
... | done VM = done (Inj₁ VM) ... | done VM = done (Inj₁ VM)
progress (`inj₂ N) with progress N progress (`inj₂ N) with progress N
... | step N⟶N′ = step (ξ-inj₂ N⟶N′) ... | step N—→N′ = step (ξ-inj₂ N—→N′)
... | done VN = done (Inj₂ VN) ... | done VN = done (Inj₂ VN)
progress (`case⊎ L M N) with progress L progress (`case⊎ L M N) with progress L
... | step L⟶L′ = step (ξ-case⊎ L⟶L′) ... | step L—→L′ = step (ξ-case⊎ L—→L′)
... | done (Inj₁ VV) = step (β-⊎₁ VV) ... | done (Inj₁ VV) = step (β-⊎₁ VV)
... | done (Inj₂ VW) = step (β-⊎₂ VW) ... | done (Inj₂ VW) = step (β-⊎₂ VW)
progress (`tt) = done TT progress (`tt) = done TT
progress (`case⊥ {A = A} L) with progress L progress (`case⊥ {A = A} L) with progress L
... | step L⟶L′ = step (ξ-case⊥ {A = A} L⟶L′) ... | step L—→L′ = step (ξ-case⊥ {A = A} L—→L′)
... | done () ... | done ()
progress (`[]) = done Nil progress (`[]) = done Nil
progress (M `∷ N) with progress M progress (M `∷ N) with progress M
... | step M⟶M′ = step (ξ-∷₁ M⟶M′) ... | step M—→M′ = step (ξ-∷₁ M—→M′)
... | done VM with progress N ... | done VM with progress N
... | step N⟶N′ = step (ξ-∷₂ VM N⟶N′) ... | step N—→N′ = step (ξ-∷₂ VM N—→N′)
... | done VN = done (Cons VM VN) ... | done VN = done (Cons VM VN)
progress (`caseL L M N) with progress L progress (`caseL L M N) with progress L
... | step L⟶L′ = step (ξ-caseL L⟶L′) ... | step L—→L′ = step (ξ-caseL L—→L′)
... | done Nil = step β-List₁ ... | done Nil = step β-List₁
... | done (Cons VV VW) = step (β-List₂ VV VW) ... | done (Cons VV VW) = step (β-List₂ VV VW)
progress (`let M N) with progress M progress (`let M N) with progress M
... | step M⟶M′ = step (ξ-let M⟶M′) ... | step M—→M′ = step (ξ-let M—→M′)
... | done VM = step (β-let VM) ... | done VM = step (β-let VM)
\end{code} \end{code}
@ -591,27 +593,64 @@ progress (`let M N) with progress M
## Normalise ## Normalise
\begin{code} \begin{code}
Gas : Set data Gas : Set where
Gas = ℕ gas : ℕ → Gas
data Normalise {A} (M : ε ⊢ A) : Set where data Finished {Γ A} (N : Γ ⊢ A) : Set where
normal : ∀ {N : ε ⊢ A}
→ Gas
→ M ⟶* N
-----------
→ Normalise M
normalise : ∀ {A} → ℕ → (L : ε ⊢ A) → Normalise L done :
normalise zero L = normal zero (L ∎) Value N
normalise (suc g) L with progress L ----------
... | done VL = normal (suc zero) (L ∎) → Finished N
... | step {M} L⟶M with normalise g M
... | normal h M⟶*N = normal (suc h) (L ⟶⟨ L⟶M ⟩ M⟶*N) out-of-gas :
----------
Finished N
data Steps : ∀ {A} → ∅ ⊢ A → Set where
steps : ∀ {A} {L N : ∅ ⊢ A}
→ L —↠ N
→ Finished N
----------
→ Steps L
eval : ∀ {A}
→ Gas
→ (L : ∅ ⊢ A)
-----------
→ Steps L
eval (gas zero) L = steps (L ∎) out-of-gas
eval (gas (suc m)) L with progress L
... | done VL = steps (L ∎) (done VL)
... | step {M} L—→M with eval (gas m) M
... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin
\end{code} \end{code}
## Bisimulation ## Bisimulation
\begin{code}
data _~_ : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A → Set where
~` : ∀ {Γ A} {x : Γ ∋ A}
-------------
→ (` x) ~ (` x)
~ƛ : ∀ {Γ A B} {N N′ : Γ , A ⊢ B}
→ N ~ N′
--------------
→ (ƛ N) ~ (ƛ N′)
~· : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
→ L ~ L′
→ M ~ M′
-------------------
→ (L · M) ~ (L′ · M′)
~let : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N N′ : Γ , A ⊢ B}
→ M ~ M′
→ N ~ N′
--------------------------
→ (`let M N) ~ ((ƛ N′) · M′)
\end{code} \end{code}