moved again

index.md

@@ -19,40 +19,40 @@ are encouraged.
 
 ## Front matter
 
-  - [Preface]({{ site.baseurl }}{% link out/plta/Preface.md %})
+  - [Preface]({{ site.baseurl }}{% link out/plfa/Preface.md %})
 
 ## Part 1: Logical Foundations
 
 (This part is ready for review. Please comment!)
 
-  - [Naturals: Natural numbers]({{ site.baseurl }}{% link out/plta/Naturals.md %})
+  - [Naturals: Natural numbers]({{ site.baseurl }}{% link out/plfa/Naturals.md %})
-  - [Induction: Proof by induction]({{ site.baseurl }}{% link out/plta/Induction.md %})
+  - [Induction: Proof by induction]({{ site.baseurl }}{% link out/plfa/Induction.md %})
-  - [Relations: Inductive definition of relations]({{ site.baseurl }}{% link out/plta/Relations.md %})
+  - [Relations: Inductive definition of relations]({{ site.baseurl }}{% link out/plfa/Relations.md %})
-  - [Equality: Equality and equational reasoning]({{ site.baseurl }}{% link out/plta/Equality.md %})
+  - [Equality: Equality and equational reasoning]({{ site.baseurl }}{% link out/plfa/Equality.md %})
-  - [Isomorphism: Isomorphism and embedding]({{ site.baseurl }}{% link out/plta/Isomorphism.md %})
+  - [Isomorphism: Isomorphism and embedding]({{ site.baseurl }}{% link out/plfa/Isomorphism.md %})
-  - [Connectives: Conjunction, disjunction, and implication]({{ site.baseurl }}{% link out/plta/Connectives.md %})
+  - [Connectives: Conjunction, disjunction, and implication]({{ site.baseurl }}{% link out/plfa/Connectives.md %})
-  - [Negation: Negation, with intuitionistic and classical Logic]({{ site.baseurl }}{% link out/plta/Negation.md %})
+  - [Negation: Negation, with intuitionistic and classical Logic]({{ site.baseurl }}{% link out/plfa/Negation.md %})
-  - [Quantifiers: Universals and existentials]({{ site.baseurl }}{% link out/plta/Quantifiers.md %})
+  - [Quantifiers: Universals and existentials]({{ site.baseurl }}{% link out/plfa/Quantifiers.md %})
-  - [Lists: Lists and higher-order functions]({{ site.baseurl }}{% link out/plta/Lists.md %})
+  - [Lists: Lists and higher-order functions]({{ site.baseurl }}{% link out/plfa/Lists.md %})
-  - [Decidable: Booleans and decision procedures]({{ site.baseurl }}{% link out/plta/Decidable.md %})
+  - [Decidable: Booleans and decision procedures]({{ site.baseurl }}{% link out/plfa/Decidable.md %})
 
 ## Part 2: Programming Language Foundations
 
 (This part is not yet ready for review.)
 
-  - [Lambda: Lambda: Introduction to Lambda Calculus]({{ site.baseurl }}{% link out/plta/Lambda.md %})
+  - [Lambda: Lambda: Introduction to Lambda Calculus]({{ site.baseurl }}{% link out/plfa/Lambda.md %})
-  - [Properties: Progress and Preservation]({{ site.baseurl }}{% link out/plta/Properties.md %})
+  - [Properties: Progress and Preservation]({{ site.baseurl }}{% link out/plfa/Properties.md %})
-  - [DeBruijn: Inherently typed De Bruijn representation]({{ site.baseurl }}{% link out/plta/DeBruijn.md %})
+  - [DeBruijn: Inherently typed De Bruijn representation]({{ site.baseurl }}{% link out/plfa/DeBruijn.md %})
-  - [More: More constructs of simply-typed lambda calculus]({{ site.baseurl }}{% link out/plta/More.md %}) 
+  - [More: More constructs of simply-typed lambda calculus]({{ site.baseurl }}{% link out/plfa/More.md %}) 
-  - [Bisimulation: Relating reductions systems]({{ site.baseurl }}{% link out/plta/Bisimulation.md %}) 
+  - [Bisimulation: Relating reductions systems]({{ site.baseurl }}{% link out/plfa/Bisimulation.md %}) 
-  - [Inference: Bidirectional type inference]({{ site.baseurl }}{% link out/plta/Inference.md %})
+  - [Inference: Bidirectional type inference]({{ site.baseurl }}{% link out/plfa/Inference.md %})
-  - [Untyped: Untyped lambda calculus with full normalisation]({{ site.baseurl }}{% link out/plta/Untyped.md %})
+  - [Untyped: Untyped lambda calculus with full normalisation]({{ site.baseurl }}{% link out/plfa/Untyped.md %})
 
 ## Backmatter
 
-  - [Acknowledgements]({{ site.baseurl }}{% link out/plta/Acknowledgements.md %})
+  - [Acknowledgements]({{ site.baseurl }}{% link out/plfa/Acknowledgements.md %})
-  - [Fonts: Test page for fonts]({{ site.baseurl }}{% link out/plta/Fonts.md %})
+  - [Fonts: Test page for fonts]({{ site.baseurl }}{% link out/plfa/Fonts.md %})
-  - [Statistics: Line counts for each chapter]({{ site.baseurl }}{% link out/plta/Statistics.md %})
+  - [Statistics: Line counts for each chapter]({{ site.baseurl }}{% link out/plfa/Statistics.md %})
 
 [wen]: https://github.com/wenkokke
 [phil]: http://homepages.inf.ed.ac.uk/wadler/

src/plfa/SmallInherent.lagda

@@ -0,0 +1,217 @@
+---
+title     : "SmallInherent"
+layout    : page
+permalink : /SmallInherent/
+---
+
+
+\begin{code}
+module plfa.SmallInherent where
+
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Nat using (ℕ; zero; suc)
+
+infix  4 _⊢_
+infix  4 _∋_
+infixl 5 _,_
+
+infixr 7 _⇒_
+
+infix  5 ƛ_
+infixl 7 _·_
+infix  9 `_
+infix  9 S_
+infix  9 #_
+
+infix  1 begin_
+infix  2 _—→_
+infix  2 _—↠_
+infixr 2 _—→⟨_⟩_
+infix  3 _∎
+
+data Type : Set where
+  _⇒_ : Type → Type → Type
+  `ℕ  : Type
+
+data Context : Set where
+  ∅   : Context
+  _,_ : Context → Type → Context
+
+data _∋_ : Context → Type → Set where
+
+  Z : ∀ {Γ A}
+      ----------
+    → Γ , A ∋ A
+
+  S_ : ∀ {Γ A B}
+    → Γ ∋ A
+      ---------
+    → Γ , B ∋ A
+
+data _⊢_ : Context → Type → Set where
+
+  `_ : ∀ {Γ} {A}
+    → Γ ∋ A
+      ------
+    → Γ ⊢ A
+
+  ƛ_  :  ∀ {Γ} {A B}
+    → Γ , A ⊢ B
+      ----------
+    → Γ ⊢ A ⇒ B
+
+  _·_ : ∀ {Γ} {A B}
+    → Γ ⊢ A ⇒ B
+    → Γ ⊢ A
+      ----------
+    → Γ ⊢ B
+
+lookup : Context → ℕ → Type
+lookup (Γ , A) zero     =  A
+lookup (Γ , _) (suc n)  =  lookup Γ n
+lookup ∅       _        =  ⊥-elim impossible
+  where postulate impossible : ⊥
+
+count : ∀ {Γ} → (n : ℕ) → Γ ∋ lookup Γ n
+count {Γ , _} zero     =  Z
+count {Γ , _} (suc n)  =  S (count n)
+count {∅}     _        =  ⊥-elim impossible
+  where postulate impossible : ⊥
+
+#_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n
+# n  =  ` count n
+
+ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
+    ----------------------------------
+  → (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
+ext ρ Z      =  Z
+ext ρ (S x)  =  S (ρ x)
+
+rename : ∀ {Γ Δ}
+  → (∀ {A} → Γ ∋ A → Δ ∋ A)
+    ------------------------
+  → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
+rename ρ (` x)          =  ` (ρ x)
+rename ρ (ƛ N)          =  ƛ (rename (ext ρ) N)
+rename ρ (L · M)        =  (rename ρ L) · (rename ρ M)
+
+exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A)
+    ----------------------------------
+  → (∀ {A B} → Γ , B ∋ A → Δ , B ⊢ A)
+exts σ Z      =  ` Z
+exts σ (S x)  =  rename S_ (σ x)
+
+subst : ∀ {Γ Δ}
+  → (∀ {A} → Γ ∋ A → Δ ⊢ A)
+    ------------------------
+  → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
+subst σ (` k)          =  σ k
+subst σ (ƛ N)          =  ƛ (subst (exts σ) N)
+subst σ (L · M)        =  (subst σ L) · (subst σ M)
+
+_[_] : ∀ {Γ A B}
+        → Γ , B ⊢ A
+        → Γ ⊢ B 
+          ---------
+        → Γ ⊢ A
+_[_] {Γ} {A} {B} N M =  subst {Γ , B} {Γ} σ {A} N
+  where
+  σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A
+  σ Z      =  M
+  σ (S x)  =  ` x
+
+data Value : ∀ {Γ A} → Γ ⊢ A → Set where
+
+  V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
+      ---------------------------
+    → Value (ƛ N)
+
+data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+
+  ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
+    → L —→ L′
+      -----------------
+    → L · M —→ L′ · M
+
+  ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
+    → Value V
+    → M —→ M′
+      --------------
+    → V · M —→ V · M′
+
+  β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
+    → Value W
+      -------------------
+    → (ƛ N) · W —→ N [ W ]
+
+data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+
+  _∎ : ∀ {Γ A} (M : Γ ⊢ A)
+      --------
+    → M —↠ M
+
+  _—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
+    → L —→ M
+    → M —↠ N
+      ---------
+    → L —↠ N
+
+begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A}
+  → M —↠ N
+    ------
+  → M —↠ N
+begin M—↠N = M—↠N
+
+data Progress {A} (M : ∅ ⊢ A) : Set where
+  step : ∀ {N : ∅ ⊢ A}
+    → M —→ N
+      -------------
+    → Progress M
+  done :
+      Value M
+      ----------
+    → Progress M
+
+progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M
+progress (` ())
+progress (ƛ N)                          =  done V-ƛ
+progress (L · M) with progress L
+...    | step L—→L′                     =  step (ξ-·₁ L—→L′)
+...    | done V-ƛ with progress M
+...        | step M—→M′                 =  step (ξ-·₂ V-ƛ M—→M′)
+...        | done VM                    =  step (β-ƛ VM)
+
+data Gas : Set where
+  gas : ℕ → Gas
+
+data Finished {Γ A} (N : Γ ⊢ A) : Set where
+
+   done :
+       Value N
+       ----------
+     → Finished 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}
+