From 6ff8e77c221b6186e2785bf27f1a0251066852a1 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Wed, 13 Sep 2017 17:34:32 +0100 Subject: [PATCH 1/6] changes to README and config --- README.md | 21 ++++++++------------- _config.yml | 4 ++-- src/Stlc.lagda | 3 +++ 3 files changed, 13 insertions(+), 15 deletions(-) diff --git a/README.md b/README.md index 8b452fef..1dd415d6 100644 --- a/README.md +++ b/README.md @@ -15,13 +15,14 @@ and [Philip Wadler]( http://homepages.inf.ed.ac.uk/wadler/ ). +Please send us comments! Contact details below. ## How to host literate code In directory `sf/` run the following: - $ make clobber + $ make clobber $ make $ make serve & @@ -29,18 +30,6 @@ The visible page appears at localhost:4000/sf/ -## Markdown - -For markdown commands see [Daring Fireball]( -https://daringfireball.net/projects/markdown/syntax -). - -## Important git commands - - git pull - git commit -am "message" - git push - ## Unicode abbreviations @@ -68,3 +57,9 @@ Also see [here]( http://agda.readthedocs.io/en/latest/tools/emacs-mode.html ). +## Markdown + +For markdown commands see [Daring Fireball]( +https://daringfireball.net/projects/markdown/syntax +). + diff --git a/_config.yml b/_config.yml index 114d4b8f..82910942 100644 --- a/_config.yml +++ b/_config.yml @@ -8,10 +8,10 @@ author: Wen Kokke contributors: - name: Wen Kokke email: wen.kokke@ed.ac.uk - github_username: wenkokke + twitter_username: wenkokke - name: Philip Wadler email: wadler@inf.ed.ac.uk - github_username: wadler + twitter_username: philipwadler description: > Software Foundations in Agda. diff --git a/src/Stlc.lagda b/src/Stlc.lagda index fae038d7..35f314b1 100644 --- a/src/Stlc.lagda +++ b/src/Stlc.lagda @@ -192,6 +192,9 @@ is sometimes called _alpha renaming_. As we descend from a term into its subterms, variables that are bound may become free. Consider the following terms. + + + * `` ฮป[ f โˆถ ๐”น โ‡’ ๐”น ] ฮป[ x โˆถ ๐”น ] ` f ยท (` f ยท ` x) `` Both variable `f` and `x` are bound. From b5b755ac495a0f98ddc380e998609ebc9f319e2a Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Sun, 1 Oct 2017 20:23:11 +0100 Subject: [PATCH 2/6] publishing Basics --- index.md | 3 - out/Stlc.md | 4835 ++++++++++++++++++++++++++------------------------- 2 files changed, 2434 insertions(+), 2404 deletions(-) diff --git a/index.md b/index.md index 750defcf..0db2ca5f 100644 --- a/index.md +++ b/index.md @@ -17,10 +17,7 @@ http://homepages.inf.ed.ac.uk/wadler/ ## Contents - - - [Maps: Total and Partial Maps]({{ "/Maps" | relative_url }}) - [Stlc: The Simply Typed Lambda-Calculus]({{ "/Stlc" | relative_url }}) - [StlcProp: Properties of STLC]({{ "/StlcProp" | relative_url }}) diff --git a/out/Stlc.md b/out/Stlc.md index 9e603fc5..d6ce9cb3 100644 --- a/out/Stlc.md +++ b/out/Stlc.md @@ -38,7 +38,8 @@ lists, records, subtyping, and mutable state. ## Imports -
{% raw %}
+
+
 open)
-{% endraw %}

+
+
## Syntax @@ -299,7 +301,8 @@ Here is the syntax of types in BNF. And here it is formalised in Agda. -
{% raw %}
+
+
 infixrType
-{% endraw %}

+
+
Terms have six constructs. Three are for the core lambda calculus: @@ -405,7 +409,8 @@ Here is the syntax of terms in BNF. And here it is formalised in Agda. -
{% raw %}
+
+
 infixlTerm
-{% endraw %}

+
+
#### Special characters @@ -663,7 +669,8 @@ Here are a couple of example terms, `not` of type `(๐”น โ‡’ ๐”น) โ‡’ ๐”น โ‡’ ๐”น` which takes a function and a boolean and applies the function to the boolean twice. -
{% raw %}
+
+
 f)
-{% endraw %}

+
+
#### Bound and free variables @@ -928,6 +936,9 @@ is sometimes called _alpha renaming_. As we descend from a term into its subterms, variables that are bound may become free. Consider the following terms. + + + * `` ฮป[ f โˆถ ๐”น โ‡’ ๐”น ] ฮป[ x โˆถ ๐”น ] ` f ยท (` f ยท ` x) `` Both variable `f` and `x` are bound. @@ -980,373 +991,375 @@ to be weaker than application. For instance, - abbreviates `` (ฮป[ f โˆถ ๐”น โ‡’ ๐”น ] (ฮป[ x โˆถ ๐”น ] (` f ยท (` f ยท ` x)))) `` - and not `` (ฮป[ f โˆถ ๐”น โ‡’ ๐”น ] (ฮป[ x โˆถ ๐”น ] ` f)) ยท (` f ยท ` x) ``. -
{% raw %}
-
+
+ex₁ : (𝔹 ⇒ (𝔹) ⇒ ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 ≡ (𝔹 ⇒ (𝔹) ⇒ ⇒ (𝔹) ⇒ ⇒ 𝔹)
-ex₁ = refl
-
-ex₂ : two · not · true ≡ (two𝔹 ·⇒ not𝔹) · true
 ex₂ex₁ = refl
 
 ex₃ex₂ : λ[two · not · true ≡ (two · not) · true
+ex₂ = refl
+
+ex₃ : f ∶ 𝔹 ⇒ 𝔹 ] λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · (` x)f · ` x)
       ≡ (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (`λ[ x ∶ 𝔹 ] f · (` f · f · (` f · ` x))))
 ex₃ = refl
-{% endraw %}
+ + #### Quiz @@ -1392,134 +1405,136 @@ as values. The predicate `Value M` holds if term `M` is a value. -
{% raw %}
-
+
+data Value : Term → Set where
   value-λ     : ∀ {x A{x N}A → Value (λ[ x ∶ A ] N)} → Value (λ[ x ∶ A ] N)
   value-true  :  : Value true
   value-false : Value false
-{% endraw %}
+ + We let `V` and `W` range over values. @@ -1586,650 +1601,652 @@ name. Here is the formal definition in Agda. -
{% raw %}
-
+
+_[_:=_] : Term → Id Id → Term → Term
 (` x′) [ x := V:= V ] with x ≟ x′ x′
 ... | yes _ = V
 ... | no  _ no  _ = ` x′ x′
 (λ[ x′ ∶x′ A′∶ A′ ] N′) [ x := := V ] with x ≟ x′ x′
 ... | yes _ = λ[ x′λ[ ∶x′ A′∶ ]A′ N′] N′
 ... | no  _ no  _ = λ[ x′λ[ ∶x′ A′∶ A′ ] (N′ [ x := V:= ])V ])
 (L′ · M′) [ x := V ] =  (L′ [ x := V ] =  (L′ [ x V:= ])V ]) · (M′ [ x := V:= ])V ])
 (true) [ x := := V ] = true
 (false) [ x := := V ] = false
 (if L′ thenL′ M′then M′ else N′) [ x := := V ] =
   if (L′ [ x := V:= ])V ]) then (M′ [ x := V:= ])V ]) else (N′ [ x := V:= V ])
-{% endraw %}
+ + The two key cases are variables and abstraction. @@ -2255,670 +2272,672 @@ Note that โ€ฒ (U+2032: PRIME) is not the same as ' (U+0027: APOSTROPHE). Here is confirmation that the examples above are correct. -
{% raw %}
-
+
+ex₁₁ : ` f [ f := not:= not ] ≡  not
 ex₁₁ = refl
 
 ex₁₂ : true [ f := := not ] ≡ true
 ex₁₂ = refl
 
 ex₁₃ : (` f(` f · true) [ f := not:= not ] ≡ not · true
 ex₁₃ = refl
 
 ex₁₄ : (` f · (` f · f(` f · true)) [ f := not:= not ] ≡ not · (not · true)
 ex₁₄ = refl
 
 ex₁₅ : (λ[ x ∶ 𝔹 ] ` f · (` f · (` x)) [ f :=· ` x)) [ f := not ] ≡ λ[ xλ[ x ∶ 𝔹 ] not · (not · ` x) x)
 ex₁₅ = refl
 
 ex₁₆ : (λ[ y ∶ 𝔹 ] ` y) y) [ x := := true ] ≡ λ[ yλ[ y ∶ 𝔹 ] ` y
 ex₁₆ = refl
 
 ex₁₇ : (λ[ x ∶ 𝔹 ] ` x) [ x) :=[ x := true ] ≡ λ[ xλ[ x ∶ 𝔹 ] ` x
 ex₁₇ = refl
-{% endraw %}
+ + #### Quiz @@ -2986,573 +3005,575 @@ and indeed such rules are traditionally called beta rules. Here are the above rules formalised in Agda. -
{% raw %}
-
+
+infix 10 10 _⟹_ 
 
 data _⟹_ : Term → Term → Set where
   ξ·₁ : ∀ {L L′{L M}L′ M} →
     L ⟹ L′ L′ →
     L · M ⟹ L′ ·L′ · M
   ξ·₂ : ∀ {V M M′} →
-    Value {V M M′} →
     Value V →
+    M ⟹ M′ M′ →
     V · M ⟹ V · M′ M′
   βλ· : ∀ {x {x A N V} → Value V} → Value V →
     (λ[ x ∶ A ] N) · V ⟹ N) · V ⟹ N [ x := V:= V ]
   ξif : ∀ {L L′{L ML′ N}M N} →
     L ⟹ L′ L′ →    
     if L then M else N ⟹ if L′if L′ then M else N
   βif-true : ∀ {M N}{M N} →
     if true then M else N ⟹ M
   βif-false : ∀ {M N}{M N} →
     if false then M else N ⟹ N
-{% endraw %}
+ + #### Special characters @@ -3616,193 +3637,195 @@ are written as follows. Here it is formalised in Agda. -
{% raw %}
-
+
+infix 10 10 _⟹*_ 
 infixr 2 _⟹⟨_⟩_
 infix  3 _∎  3 _∎
 
 data _⟹*_ : Term → Term → Set where
   _∎ : ∀ M → M ⟹* ⟹* M
   _⟹⟨_⟩_ : ∀ L {ML N}{M →N} → L ⟹ M → M ⟹* N → L ⟹* N → L ⟹* N
-{% endraw %}
+ + We can read this as follows. @@ -3816,481 +3839,483 @@ The names of the two clauses in the definition of reflexive and transitive closure have been chosen to allow us to lay out example reductions in an appealing way. -
{% raw %}
-
+
+reduction₁ : not · true ⟹* ⟹* false
 reduction₁ =
     not · true
   ⟹⟨ βλ· value-true ⟩
     if true then false else true
   ⟹⟨ βif-true ⟩
     false
   ∎
 
 reduction₂ : two · not · true ⟹* ⟹* true
 reduction₂ =
     two · not · true
   ⟹⟨ ξ·₁ (βλ· value-λ) ⟩
     (λ[ x ∶ 𝔹 ] not · (not · ` x)) · true
   ⟹⟨ βλ· value-true ⟩
     not · (not · true)
   ⟹⟨ ξ·₂ value-λ (βλ· value-true) ⟩
     not · (if true then false else true)
   ⟹⟨ ξ·₂ value-λ βif-true  ⟩  ⟩
     not · false
   ⟹⟨ βλ· value-false ⟩
     if false then false else true
   ⟹⟨ βif-false ⟩
     true
   ∎
-{% endraw %}
+ +