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

an example got out of sync with the text

Browse source
This commit is contained in:
Jeremy Siek 2020-03-11 13:35:52 -04:00
parent 40f287e050
commit 1c54d99cbe
1 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/plfa/part3/Denotational.lagda.md
View file

@ -341,7 +341,7 @@ lambda abstraction results in a single-entry table that maps the input
`v` to the output `w`, provided that evaluating the body in an `v` to the output `w`, provided that evaluating the body in an
environment with `v` bound to its parameter produces the output `w`. environment with `v` bound to its parameter produces the output `w`.
As a simple example of this rule, we can see that the identity function As a simple example of this rule, we can see that the identity function
maps `⊥` to `⊥`. maps `⊥` to `⊥` and also that it maps `⊥ ↦ ⊥` to `⊥ ↦ ⊥`.
``` ```
id : ∅ ⊢ ★ id : ∅ ⊢ ★
@ -349,11 +349,11 @@ id = ƛ # 0
``` ```
``` ```
denot-id : ∀ {γ v} → γ ⊢ id ↓ v ↦ v denot-id1 : ∀ {γ} → γ ⊢ id ↓ ⊥ ↦ ⊥
denot-id = ↦-intro var denot-id1 = ↦-intro var
denot-id-two : ∀ {γ v w} → γ ⊢ id ↓ (v ↦ v) ⊔ (w ↦ w) denot-id2 : ∀ {γ} → γ ⊢ id ↓ (⊥ ↦ ⊥) ↦ (⊥ ↦ ⊥)
denot-id-two = ⊔-intro denot-id denot-id denot-id2 = ↦-intro var
``` ```
Of course, we will need tables with many rows to capture the meaning Of course, we will need tables with many rows to capture the meaning
@ -366,12 +366,12 @@ abstraction, it pre-evaluates the function on a bunch of randomly
chosen arguments, using many instances of the rule `↦-intro`, and then chosen arguments, using many instances of the rule `↦-intro`, and then
joins them into a big table using many instances of the rule `⊔-intro`. joins them into a big table using many instances of the rule `⊔-intro`.
In the following we show that the identity function produces a table In the following we show that the identity function produces a table
containing both of the previous results, `⊥ ↦ ⊥` and `(⊥ ↦ ⊥) ↦ (⊥ ↦ containing both of the previous results, `⊥ ↦ ⊥` and
⊥)`. `(⊥ ↦ ⊥) ↦ (⊥ ↦ ⊥)`.
``` ```
denot-id3 : `∅ ⊢ id ↓ (⊥ ↦ ⊥) ⊔ (⊥ ↦ ⊥) ↦ (⊥ ↦ ⊥) denot-id3 : `∅ ⊢ id ↓ (⊥ ↦ ⊥) ⊔ (⊥ ↦ ⊥) ↦ (⊥ ↦ ⊥)
denot-id3 = denot-id-two denot-id3 = ⊔-intro denot-id1 denot-id2
``` ```
We most often think of the judgment `γ ⊢ M ↓ v` as taking the We most often think of the judgment `γ ⊢ M ↓ v` as taking the