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

fixes to formal code in More

Browse source
This commit is contained in:
wadler 2018-07-09 12:23:41 -03:00
parent c0b9c4ba01
commit 202f0f54ba
4 changed files with 1638 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1556
extra/extra/PropertiesDec.lagda Normal file
View file

File diff suppressed because it is too large Load diff

6
index.md
View file

@ -31,7 +31,7 @@ are encouraged.
- [Equality: Equality and equational reasoning]({{ site.baseurl }}{% link out/plfa/Equality.md %})
- [Isomorphism: Isomorphism and embedding]({{ site.baseurl }}{% link out/plfa/Isomorphism.md %})
- [Connectives: Conjunction, disjunction, and implication]({{ site.baseurl }}{% link out/plfa/Connectives.md %})
- [Negation: Negation, with intuitionistic and classical Logic]({{ site.baseurl }}{% link out/plfa/Negation.md %})
- [Negation: Negation, with intuitionistic and classical logic]({{ site.baseurl }}{% link out/plfa/Negation.md %})
- [Quantifiers: Universals and existentials]({{ site.baseurl }}{% link out/plfa/Quantifiers.md %})
- [Lists: Lists and higher-order functions]({{ site.baseurl }}{% link out/plfa/Lists.md %})
- [Decidable: Booleans and decision procedures]({{ site.baseurl }}{% link out/plfa/Decidable.md %})
@ -40,13 +40,13 @@ are encouraged.
(The following is ready for review. Please comment!)
- [Lambda: Lambda: Introduction to Lambda Calculus]({{ site.baseurl }}{% link out/plfa/Lambda.md %})
- [Lambda: Introduction to Lambda Calculus]({{ site.baseurl }}{% link out/plfa/Lambda.md %})
- [Properties: Progress and Preservation]({{ site.baseurl }}{% link out/plfa/Properties.md %})
- [DeBruijn: Inherently typed De Bruijn representation]({{ site.baseurl }}{% link out/plfa/DeBruijn.md %})
(The following is not yet ready for review.)
- [More: More constructs of simply-typed lambda calculus]({{ site.baseurl }}{% link out/plfa/More.md %})
- [More: Additional constructs of simply-typed lambda calculus]({{ site.baseurl }}{% link out/plfa/More.md %})
- [Bisimulation: Relating reductions systems]({{ site.baseurl }}{% link out/plfa/Bisimulation.md %})
- [Inference: Bidirectional type inference]({{ site.baseurl }}{% link out/plfa/Inference.md %})
- [Untyped: Untyped lambda calculus with full normalisation]({{ site.baseurl }}{% link out/plfa/Untyped.md %})

80
src/plfa/More.lagda
View file

@ -1,5 +1,5 @@
---
title : "More: More constructs of simply-typed lambda calculus"
title : "More: Additional constructs of simply-typed lambda calculus"
layout : page
permalink : /More/
---
@ -12,12 +12,34 @@ So far, we have focussed on a relatively minimal language,
based on Plotkin's PCF, which supports functions, naturals, and
fixpoints. In this chapter we extend our calculus to support
more datatypes, including products, sums, unit type, empty
type, and lists, all of which will be familiar from Part I of
type, and lists, all of which are familiar from Part I of
this textbook. We also describe _let_ bindings. Most of the
description will be informal. We show how to formalise a few
of the constructs, and leave the rest as an exercise for the
reader.
## Products
## An alternative formulation of products
## Sums
## Unit type
## Empty type
## Lists
## Let bindings
## Imports
\begin{code}
@ -135,6 +157,12 @@ data _⊢_ : Context → Type → Set where
-----------
→ Γ ⊢ B
case× : ∀ {Γ A B C}
→ Γ ⊢ A `× B
→ Γ , A , B ⊢ C
--------------
→ Γ ⊢ C
`inj₁ : ∀ {Γ A B}
→ Γ ⊢ A
-----------
@ -232,6 +260,7 @@ rename ρ (μ N) = μ (rename (ext ρ) N)
rename ρ `⟨ M , N ⟩ = `⟨ rename ρ M , rename ρ N ⟩
rename ρ (`proj₁ L) = `proj₁ (rename ρ L)
rename ρ (`proj₂ L) = `proj₂ (rename ρ L)
rename ρ (case× L M) = case× (rename ρ L) (rename (ext (ext ρ)) M)
rename ρ (`inj₁ M) = `inj₁ (rename ρ M)
rename ρ (`inj₂ N) = `inj₂ (rename ρ N)
rename ρ (case⊎ L M N) = case⊎ (rename ρ L) (rename (ext ρ) M) (rename (ext ρ) N)
@ -261,6 +290,7 @@ subst σ (μ N) = μ (subst (exts σ) N)
subst σ `⟨ M , N ⟩ = `⟨ subst σ M , subst σ N ⟩
subst σ (`proj₁ L) = `proj₁ (subst σ L)
subst σ (`proj₂ L) = `proj₂ (subst σ L)
subst σ (case× L M) = case× (subst σ L) (subst (exts (exts σ)) M)
subst σ (`inj₁ M) = `inj₁ (subst σ M)
subst σ (`inj₂ N) = `inj₂ (subst σ N)
subst σ (case⊎ L M N) = case⊎ (subst σ L) (subst (exts σ) M) (subst (exts σ) N)
@ -387,11 +417,11 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
-------------------------
→ case L M N —→ case L′ M N
β-ℕ₁ : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
β-zero : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
-------------------
→ case `zero M N —→ M
β-ℕ₂ : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
→ Value V
----------------------------
→ case (`suc V) M N —→ N [ V ]
@ -421,18 +451,29 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
---------------------
→ `proj₂ L —→ `proj₂ L′
β-×₁ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
β-proj₁ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
→ Value V
→ Value W
----------------------
→ `proj₁ `⟨ V , W ⟩ —→ V
β-×₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
β-proj₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
→ Value V
→ Value W
----------------------
→ `proj₂ `⟨ V , W ⟩ —→ W
ξ-case× : ∀ {Γ A B C} {L L′ : Γ ⊢ A `× B} {M : Γ , A , B ⊢ C}
→ L —→ L′
-----------------------
→ case× L M —→ case× L′ M
β-case× : ∀ {Γ A B C} {V : Γ ⊢ A} {W : Γ ⊢ B} {M : Γ , A , B ⊢ C}
→ Value V
→ Value W
----------------------------------
→ case× `⟨ V , W ⟩ M —→ M [ V ][ W ]
ξ-inj₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A}
→ M —→ M′
---------------------------
@ -448,12 +489,12 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
---------------------------
→ case⊎ L M N —→ case⊎ L′ M N
β-⊎₁ : ∀ {Γ A B C} {V : Γ ⊢ A} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C}
β-inj₁ : ∀ {Γ A B C} {V : Γ ⊢ A} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C}
→ Value V
------------------------------
→ case⊎ (`inj₁ V) M N —→ M [ V ]
β-⊎₂ : ∀ {Γ A B C} {W : Γ ⊢ B} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C}
β-inj₂ : ∀ {Γ A B C} {W : Γ ⊢ B} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C}
→ Value W
------------------------------
→ case⊎ (`inj₂ W) M N —→ N [ W ]
@ -479,11 +520,11 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
---------------------------
→ caseL L M N —→ caseL L′ M N
β-List₁ : ∀ {Γ A B} {M : Γ ⊢ B} {N : Γ , A , `List A ⊢ B}
β-[] : ∀ {Γ A B} {M : Γ ⊢ B} {N : Γ , A , `List A ⊢ B}
------------------
→ caseL `[] M N —→ M
β-List₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ `List A}
β-∷ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ `List A}
{M : Γ ⊢ B} {N : Γ , A , `List A ⊢ B}
→ Value V
→ Value W
@ -592,8 +633,8 @@ progress (`suc M) with progress M
... | done VM = done (V-suc VM)
progress (case L M N) with progress L
... | step L—→L′ = step (ξ-case L—→L′)
... | done V-zero = step β-ℕ₁
... | done (V-suc VL) = step (β-ℕ₂ VL)
... | done V-zero = step β-zero
... | done (V-suc VL) = step (β-suc VL)
progress (μ N) = step β-μ
progress `⟨ M , N ⟩ with progress M
... | step M—→M′ = step (ξ-⟨,⟩₁ M—→M′)
@ -602,10 +643,13 @@ progress `⟨ M , N ⟩ with progress M
... | done VN = done (V-⟨ VM , VN ⟩)
progress (`proj₁ L) with progress L
... | step L—→L′ = step (ξ-proj₁ L—→L′)
... | done (V-⟨ VM , VN ⟩) = step (β-×₁ VM VN)
... | done (V-⟨ VM , VN ⟩) = step (β-proj₁ VM VN)
progress (`proj₂ L) with progress L
... | step L—→L′ = step (ξ-proj₂ L—→L′)
... | done (V-⟨ VM , VN ⟩) = step (β-×₂ VM VN)
... | done (V-⟨ VM , VN ⟩) = step (β-proj₂ VM VN)
progress (case× L M) with progress L
... | step L—→L′ = step (ξ-case× L—→L′)
... | done (V-⟨ VM , VN ⟩) = step (β-case× VM VN)
progress (`inj₁ M) with progress M
... | step M—→M′ = step (ξ-inj₁ M—→M′)
... | done VM = done (V-inj₁ VM)
@ -614,8 +658,8 @@ progress (`inj₂ N) with progress N
... | done VN = done (V-inj₂ VN)
progress (case⊎ L M N) with progress L
... | step L—→L′ = step (ξ-case⊎ L—→L′)
... | done (V-inj₁ VV) = step (β-⊎₁ VV)
... | done (V-inj₂ VW) = step (β-⊎₂ VW)
... | done (V-inj₁ VV) = step (β-inj₁ VV)
... | done (V-inj₂ VW) = step (β-inj₂ VW)
progress (`tt) = done V-tt
progress (case⊥ {A = A} L) with progress L
... | step L—→L′ = step (ξ-case⊥ {A = A} L—→L′)
@ -628,8 +672,8 @@ progress (M `∷ N) with progress M
... | done VN = done (_V-∷_ VM VN)
progress (caseL L M N) with progress L
... | step L—→L′ = step (ξ-caseL L—→L′)
... | done V-[] = step β-List₁
... | done (_V-∷_ VV VW) = step (β-List₂ VV VW)
... | done V-[] = step β-[]
... | done (_V-∷_ VV VW) = step (β-∷ VV VW)
progress (`let M N) with progress M
... | step M—→M′ = step (ξ-let M—→M′)
... | done VM = step (β-let VM)

34
src/plfa/Properties.lagda
View file

@ -914,14 +914,14 @@ When our evaluator returns a term `N`, it will either give evidence that
\begin{code}
data Finished (N : Term) : Set where
done :
Value N
----------
→ Finished N
done :
Value N
----------
→ Finished N
out-of-gas :
----------
Finished N
out-of-gas :
----------
Finished N
\end{code}
Given a term `L` of type `A`, the evaluator will, for some `N`, return
a reduction sequence from `L` to `N` and an indication of whether
@ -1368,22 +1368,22 @@ det : ∀ {M M′ M″}
det (ξ-·₁ L—→L′) (ξ-·₁ L—→L″) = cong₂ _·_ (det L—→L′ L—→L″) refl
det (ξ-·₁ L—→L′) (ξ-·₂ VL M—→M″) = ⊥-elim (V¬—→ VL L—→L′)
det (ξ-·₁ L—→L′) (β-ƛ _) = ⊥-elim (V¬—→ V-ƛ L—→L′)
det (ξ-·₂ VL _) (ξ-·₁ L—→L″) = ⊥-elim (V¬—→ VL L—→L″)
det (ξ-·₂ VL _) (ξ-·₁ L—→L″) = ⊥-elim (V¬—→ VL L—→L″)
det (ξ-·₂ _ M—→M′) (ξ-·₂ _ M—→M″) = cong₂ _·_ refl (det M—→M′ M—→M″)
det (ξ-·₂ _ M—→M′) (β-ƛ VM) = ⊥-elim (V¬—→ VM M—→M′)
det (β-ƛ _) (ξ-·₁ L—→L″) = ⊥-elim (V¬—→ V-ƛ L—→L″)
det (β-ƛ VM) (ξ-·₂ _ M—→M″) = ⊥-elim (V¬—→ VM M—→M″)
det (β-ƛ _) (β-ƛ _) = refl
det (β-ƛ _) (ξ-·₁ L—→L″) = ⊥-elim (V¬—→ V-ƛ L—→L″)
det (β-ƛ VM) (ξ-·₂ _ M—→M″) = ⊥-elim (V¬—→ VM M—→M″)
det (β-ƛ _) (β-ƛ _) = refl
det (ξ-suc M—→M′) (ξ-suc M—→M″) = cong `suc_ (det M—→M′ M—→M″)
det (ξ-case L—→L′) (ξ-case L—→L″) = cong₄ case_[zero⇒_|suc_⇒_]
(det L—→L′ L—→L″) refl refl refl
det (ξ-case L—→L′) β-zero = ⊥-elim (V¬—→ V-zero L—→L′)
det (ξ-case L—→L′) (β-suc VL) = ⊥-elim (V¬—→ (V-suc VL) L—→L′)
det β-zero (ξ-case M—→M″) = ⊥-elim (V¬—→ V-zero M—→M″)
det β-zero β-zero = refl
det (β-suc VL) (ξ-case L—→L″) = ⊥-elim (V¬—→ (V-suc VL) L—→L″)
det (β-suc _) (β-suc _) = refl
det β-μ β-μ = refl
det β-zero (ξ-case M—→M″) = ⊥-elim (V¬—→ V-zero M—→M″)
det β-zero β-zero = refl
det (β-suc VL) (ξ-case L—→L″) = ⊥-elim (V¬—→ (V-suc VL) L—→L″)
det (β-suc _) (β-suc _) = refl
det β-μ β-μ = refl
\end{code}
The proof is by induction over possible reductions. We consider
three typical cases.
@ -1418,7 +1418,7 @@ three typical cases.
Since the left-hand sides are identical, the right-hand sides are
also identical. The formal proof invokes `refl`.
Almost half the lines in the above proof are redundant, e.g., the case
Five of the 18 lines in the above proof are redundant, e.g., the case
when one rule is `ξ-·₁` and the other is `ξ-·₂` is considered twice,
once with `ξ-·₁` first and `ξ-·₂` second, and the other time with the
two swapped. What we might like to do is delete the redundant lines