diff --git a/out/Basics.md b/out/Basics.md index d0202f22..15285abe 100644 --- a/out/Basics.md +++ b/out/Basics.md @@ -4,8 +4,7 @@ layout : page permalink : /Basics --- -
-
+
{% raw %}
 open)
-
-

+{% endraw %}
The functional programming style brings programming closer to simple, everyday mathematics: If a procedure or method has no side @@ -89,8 +87,7 @@ very simple example. The following declaration tells Agda that we are defining a new set of data values -- a _type_. -
-
+
{% raw %}
 dataDay
-
-

+{% endraw %}
The type is called `day`, and its members are `monday`, `tuesday`, etc. The second and following lines of the definition @@ -211,8 +207,7 @@ can be read "`monday` is a `day`, `tuesday` is a `day`, etc." Having defined `day`, we can write functions that operate on days. -
-
+
{% raw %}
 nextWeekdaymonday
-
-

+{% endraw %}
One thing to note is that the argument and return types of this function are explicitly declared. Like most functional @@ -375,8 +369,7 @@ above example to Agda, and observe the result. Second, we can record what we _expect_ the result to be in the form of an Agda type: -
-
+
{% raw %}
 test-nextWeekdaytuesday
-
-

+{% endraw %}
This declaration does two things: it makes an assertion (that the second weekday after `saturday` is `tuesday`), and it gives the assertion a name @@ -418,8 +410,7 @@ that can be used to refer to it later. Having made the assertion, we must also verify it. We do this by giving a term of the above type: -
-
+
{% raw %}
 test-nextWeekdayrefl
-
-

+{% endraw %}
There is no essential difference between the definition for `test-nextWeekday` here and the definition for `nextWeekday` above, diff --git a/out/Maps.md b/out/Maps.md index 62703ef3..b03eabb4 100644 --- a/out/Maps.md +++ b/out/Maps.md @@ -32,8 +32,7 @@ much difference, though, because we've been careful to name our own definitions and theorems the same as their counterparts in the standard library, wherever they overlap. -
-
+
{% raw %}
 open)
-
-

+{% endraw %}
Documentation for the standard library can be found at . @@ -231,8 +229,7 @@ maps. For this purpose, we again use the type `Id` from the [Lists](sf/Lists.html) chapter. To make this chapter self contained, we repeat its definition here. -
-
+
{% raw %}
 dataId
-
-

+{% endraw %}
We recall a standard fact of logic. -
-
+
{% raw %}
 contrapositive)
-
-

+{% endraw %}
Using the above, we can decide equality of two identifiers by deciding equality on the underlying strings. -
-
+
{% raw %}
 _≟_refl
-
-

+{% endraw %}
## Total Maps @@ -735,8 +727,7 @@ We build partial maps in two steps. First, we define a type of _total maps_ that return a default value when we look up a key that is not present in the map. -
-
+
{% raw %}
 TotalMapA
-
-

+{% endraw %}
Intuitively, a total map over anfi element type `A` _is_ just a function that can be used to look up ids, yielding `A`s. -
-
+
{% raw %}
 modulewhere
-
-

+{% endraw %}
The function `always` yields a total map given a default element; this map always returns the default element when applied to any id. -
-
+
{% raw %}
   alwaysv
-
-

+{% endraw %}
More interesting is the update function, which (as before) takes a map `ρ`, a key `x`, and a value `v` and returns a new map that takes `x` to `v` and takes every other key to whatever `ρ` does. -
-
+
{% raw %}
   infixly
-
-

+{% endraw %}
This definition is a nice example of higher-order programming. The update function takes a _function_ `ρ` and yields a new @@ -1060,8 +1044,7 @@ function that behaves like the desired map. For example, we can build a map taking ids to naturals, where `x` maps to 42, `y` maps to 69, and every other key maps to 0, as follows: -
-
+
{% raw %}
   modulerefl
-
-

+{% endraw %}
This completes the definition of total maps. Note that we don't need to define a `find` operation because it is just function @@ -1345,8 +1327,7 @@ the lemmas! #### Exercise: 1 star, optional (apply-always) The `always` map returns its default element for all keys: -
-
+
{% raw %}
   postulatev
-
-

+{% endraw %}
#### Exercise: 2 stars, optional (update-eq) @@ -1538,8 +1516,7 @@ Next, if we update a map `ρ` at a key `x` with a new value `v` and then look up `x` in the map resulting from the update, we get back `v`: -
-
+
{% raw %}
   postulatev
-
-

+{% endraw %}
#### Exercise: 2 stars, optional (update-neq) @@ -1879,8 +1853,7 @@ On the other hand, if we update a map `m` at a key `x` and then look up a _different_ key `y` in the resulting map, we get the same result that `m` would have given: -
-
+
{% raw %}
   update-neqrefl
-
-

+{% endraw %}
For the following lemmas, since maps are represented by functions, to show two maps equal we will need to postulate extensionality. -
-
+
{% raw %}
   postulateρ′
-
-

+{% endraw %}
#### Exercise: 2 stars, optional (update-shadow) If we update a map `ρ` at a key `x` with a value `v` and then @@ -2260,8 +2230,7 @@ resulting map behaves the same (gives the same result when applied to any key) as the simpler map obtained by performing just the second update on `ρ`: -
-
+
{% raw %}
   postulate)
-
-

+{% endraw %}
#### Exercise: 2 stars (update-same) @@ -2812,8 +2778,7 @@ Prove the following theorem, which states that if we update a map `ρ` to assign key `x` the same value as it already has in `ρ`, then the result is equal to `ρ`: -
-
+
{% raw %}
   postulateρ
-
-

+{% endraw %}
#### Exercise: 3 stars, recommended (update-permute) @@ -3194,8 +3156,7 @@ Prove one final property of the `update` function: If we update a map `m` at two distinct keys, it doesn't matter in which order we do the updates. -
-
+
{% raw %}
   postulate)
-
-

+{% endraw %}
## Partial maps @@ -4693,8 +4649,7 @@ Finally, we define _partial maps_ on top of total maps. A partial map with elements of type `A` is simply a total map with elements of type `Maybe A` and default element `nothing`. -
-
+
{% raw %}
 PartialMap)
+{% endraw %}

 
-
- -
-
+
{% raw %}
 modulewhere
+{% endraw %}

 
-
- -
-
+
{% raw %}
   ∅nothing
+{% endraw %}

 
-
- -
-
+
{% raw %}
   infixl)
-
-

+{% endraw %}
We now lift all of the basic lemmas about total maps to partial maps. -
-
+
{% raw %}
   apply-∅x
+{% endraw %}

 
-
- -
-
+
{% raw %}
   update-eq)
+{% endraw %}

 
-
- -
-
+
{% raw %}
   update-neqx≢y
+{% endraw %}

 
-
- -
-
+
{% raw %}
   update-shadow)
+{% endraw %}

 
-
- -
-
+
{% raw %}
   update-samex
+{% endraw %}

 
-
- -
-
+
{% raw %}
   update-permutex≢y
-
-

+{% endraw %}
We will also need the following basic facts about the `Maybe` type. -
-
+
{% raw %}
   just≢nothingrefl
-
-

+{% endraw %}
diff --git a/out/Stlc.md b/out/Stlc.md index 8a30e9c6..cd9f6b14 100644 --- a/out/Stlc.md +++ b/out/Stlc.md @@ -38,8 +38,7 @@ lists, records, subtyping, and mutable state. ## Imports -
-
+
{% raw %}
 open)
-
-

+{% endraw %}
## Syntax @@ -301,8 +299,7 @@ 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: @@ -409,8 +405,7 @@ Here is the syntax of terms in BNF. And here it is formalised in Agda. -
-
+
{% raw %}
 infixlTerm
-
-

+{% endraw %}
#### Special characters @@ -645,7 +639,6 @@ for use later to indicate that a variable appears free in a term, and eschew `::` because we consider it too ugly. - #### Formal vs informal In informal presentation of formal semantics, one uses choice of @@ -670,252 +663,250 @@ 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 x y : Id
 f  =  id 0
 x  =  id 1
 y  =  id 2
 
 not two : Term 
 not =  λ[ x ∶ 𝔹 ] (if ` x then false else true)
 two =  λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x)
-
-
+{% endraw %} #### Bound and free variables @@ -923,11 +914,12 @@ and applies the function to the boolean twice. In an abstraction `λ[ x ∶ A ] N` we call `x` the _bound_ variable and `N` the _body_ of the abstraction. One of the most important aspects of lambda calculus is that names of bound variables are -irrelevant. Thus the four terms +irrelevant. Thus the five terms * `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) `` * `` λ[ g ∶ 𝔹 ⇒ 𝔹 ] λ[ y ∶ 𝔹 ] ` g · (` g · ` y) `` * `` λ[ fred ∶ 𝔹 ⇒ 𝔹 ] λ[ xander ∶ 𝔹 ] ` fred · (` fred · ` xander) `` +* `` λ[ 👿 ∶ 𝔹 ⇒ 𝔹 ] λ[ 😄 ∶ 𝔹 ] ` 👿 · (` 👿 · ` 😄) `` * `` λ[ x ∶ 𝔹 ⇒ 𝔹 ] λ[ f ∶ 𝔹 ] ` x · (` x · ` f) `` are all considered equivalent. This equivalence relation @@ -980,379 +972,377 @@ Thus, We choose the binding strength for abstractions and conditionals to be weaker than application. For instance, -* `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) `` abbreviates - `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` f · (` f · ` x)))) `` and not - `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] ` f)) · (` f · ` x) ``. +* `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) `` + - 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₂ : λ[ ftwo ∶· 𝔹 ⇒not 𝔹· ] λ[true x≡ ∶(two 𝔹 ] ` f · not) (` f · true ` x)
-      ≡ex₂ (= refl
+
+ex₃ : λ[ f ∶ 𝔹f ⇒∶ 𝔹 ]⇒ (λ[𝔹 ] λ[ x ∶ 𝔹 ] (` f` ·f (`· f(` ·f `· ` x)
+      ≡ (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` f · (` f · ` x))))
 ex₃ = refl
-
-
+{% endraw %} #### Quiz @@ -1398,136 +1388,134 @@ as values. The predicate `Value M` holds if term `M` is a value. -
-
-{% raw %}
+data Value : Term → Set where
-  value-λ     : ∀ {x A N} → Value (λ[ x: ∶Term → Set where
+  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. @@ -1594,652 +1582,650 @@ name. Here is the formal definition in Agda. -
-
-{% raw %}
+_[_:=_] : Term → Id → Term → Term
-(` x′) [ x := V ] with x ≟ x′
-... | yes _Id =→ V
-...Term |→ no  _ =Term
+(` ` x′) [ x := V ] with x ≟ x′
 (λ[... x′| ∶yes A′ ] N′) [ x := V ] with_ x= ≟V x′
 ... | no yes   _ = λ[` x′
+(λ[ ∶x′ A′∶ ]A′ N′]
-... N′) |[ no  _x =:= λ[V x′] with ∶x A′≟ ]x′ (N′ [ x := V ])
 (L′... | yes _ = λ[ x′ ·∶ M′)A′ [ x := V ] =N′
+... | no  (L′_ = [λ[ xx′ :=∶ VA′ ]) · (M′N′ [ x := V ])
 (true)L′ [· M′) x[ :=x V:= ]V =] true
-(false) [ x := V ] =  (L′ false[ x := V ]) · (M′ [ x := V ])
 (if L′ thentrue) M′ else N′) [ x := V ] = true
-  if(false) [ x (L′ [ x := V ]) then= false
+(M′if [L′ then xM′ := V ]) else (N′) [ x := [V x] =
+  if (L′ [ x := V ]) then (M′ [ x := V ]) else (N′ [ x := V ])
-
-
+{% endraw %} The two key cases are variables and abstraction. @@ -2265,672 +2251,670 @@ 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
-ex₁₁ = refl
-
-ex₁₂ : true [ f := not ] ≡ true
-ex₁₂ =≡ refl  not
+ex₁₁ = refl
 
 ex₁₃ex₁₂ : (` f · true) [ f :=[ notf := ] ≡not not] ≡ · true
 ex₁₃ex₁₂ = = refl
 
 ex₁₄ex₁₃ : : (` f f· · (` f · true))) [ f := not ] ≡ not · ] ≡ not ·true
+ex₁₃ (not= ·refl true)
+
 ex₁₄ : (` =f refl
-
-ex₁₅· : (λ[` xf ∶· 𝔹true)) [ f := ] `not f] ·≡ (`not f · `(not x))· [ f := nottrue)
+ex₁₄ ]= ≡ λ[refl x ∶ 𝔹
+
+ex₁₅ ]: not(λ[ ·x (not∶ ·𝔹 ] ` x)f ·
-ex₁₅ (` f =· refl
-
-ex₁₆` :x)) [ f := (λ[not y] ∶≡ λ[ x ∶ 𝔹 ] ` y) [] not · (not · ` x := true ] ≡ λ[ y ∶ 𝔹)
+ex₁₅ ]= ` yrefl
+
 ex₁₆ = refl
-
-ex₁₇ : (λ[ xy ∶ 𝔹 ] ` y) ∶[ 𝔹x ] ` x) [ x := true ] ≡ λ[ y ∶ ]𝔹 ≡] λ[ x ∶ 𝔹 ] ` xy
 ex₁₇ex₁₆ = refl
 
-
+ex₁₇ : (λ[ x ∶ 𝔹 ] ` x) [ x := true ] ≡ λ[ x ∶ 𝔹 ] ` x +ex₁₇ = refl +{% endraw %} #### Quiz @@ -2998,575 +2982,573 @@ and indeed such rules are traditionally called beta rules. Here are the above rules formalised in Agda. -
-
-{% raw %}
+infix 10 _⟹_ 
 
 data _⟹_ : Term → Term → Set where
-  ξ·₁ : ∀ {L L′ M} →
-    L ⟹_⟹_ L′: Term →
-    L ·Term M→ ⟹ L′ ·Set Mwhere
   ξ·₂ : ∀ξ·₁ : ∀ {V M M′}L L′ M} →
     ValueL V⟹ L′ →
     ML ⟹ M′· →
-    V · M ⟹ VL′ · M′M
   βλ·ξ·₂ : ∀ {x A N V M M′} → Value V →
     Value V →
+    M ⟹ M′ (λ[ x ∶→
+    V A· ]M N) · V ⟹ V · M′ N [ x
+  βλ· := V ]
-  ξif : ∀ {Lx L′A M N} V} → Value V →
     L(λ[ x ⟹∶ L′A →    
-    if] L then M else N) · V ⟹ N [ x := V ]
+  ξif ⟹: if∀ {L L′ then M N} else N→
-  βif-trueL :⟹ ∀L′ {M→    
+    if N}L →
-    ifthen trueM else N then⟹ if ML′ then M else N ⟹ M
   βif-falseβif-true : ∀ {M N}{M N} →
     if falsetrue then M elseM Nelse ⟹N ⟹ M
+  βif-false : ∀ {M N} →
+    if false then M else N ⟹ N
-
-
+{% endraw %} #### Special characters @@ -3630,195 +3612,193 @@ are written as follows. Here it is formalised in Agda. -
-
-{% raw %}
+infix 10 _⟹*_ 
-infixr 2 _⟹⟨_⟩_
-infix  3 _∎
-
-data _⟹*_ : Term → Term10 →_⟹*_ 
+infixr Set2 where_⟹⟨_⟩_
-  infix  3 _∎ : ∀ M → M ⟹* M
-  _⟹⟨_⟩_data :_⟹*_ ∀: L {MTerm N} → LTerm ⟹→ M →Set M ⟹* N → Lwhere
+  _∎ ⟹*: ∀ M → M ⟹* M
+  _⟹⟨_⟩_ : ∀ L {M N} → L ⟹ M → M ⟹* N → L ⟹* N
-
-
+{% endraw %} We can read this as follows. @@ -3832,483 +3812,481 @@ 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-truenot · true ⟩⟹* false
+reduction₁ =
     if true then false elsenot · true
   ⟹⟨ βif-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
+  ⟹⟨ true
-  ⟹⟨ξ·₁ (βλ· value-truevalue-λ) ⟩
     not · (λ[ x ∶ 𝔹 ] not · ·(not true)
-  ⟹⟨· ` x)) ξ·₂· value-λtrue
+  ⟹⟨ (βλ· value-true) ⟩
     not · · (ifnot · true)
+  ⟹⟨ then falseξ·₂ else true)
-  ⟹⟨ ξ·₂ value-λ βif-true  (βλ· value-true) ⟩
     not · (if true then false else true)
   ⟹⟨ βλ· value-falseξ·₂ value-λ βif-true  ⟩
     ifnot · false then false else true
   ⟹⟨ βif-falseβλ· value-false ⟩
     if false then false else true
   ⟹⟨ βif-false ⟩
+    true
+  ∎
-
-
+{% endraw %}