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

tweak

Browse source
This commit is contained in:
Jeremy Siek 2020-03-11 13:47:25 -04:00
parent 7acc69d836
commit 552ec893c6
1 changed files with 5 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -400,14 +400,11 @@ id-app-id : ∀ {u : Value} → `∅ ⊢ id · id ↓ (u ↦ u)
id-app-id {u} = ↦-elim (↦-intro var) (↦-intro var) id-app-id {u} = ↦-elim (↦-intro var) (↦-intro var)
``` ```
Next we revisit the Church numeral two. Next we revisit the Church numeral two: `λ f. λ u. (f (f u))`.
This function has two parameters: a function `f` and an arbitrary value
ƛ ƛ (# 1 · (# 1 · # 0)) `u`, and it applies `f` twice. So `f` must map `u` to some value, which
we'll name `v`. Then for the second application,
This function has two parameters: a function and an arbitrary value `f` must map `v` to some value. Let's name it `w`. So the function's
`u`, and it applies the function twice. So the function must map `u`
to some value, which we'll name `v`. Then for the second application,
it must map `v` to some value. Let's name it `w`. So the function's
table must include two entries, both `u ↦ v` and `v ↦ w`. For each table must include two entries, both `u ↦ v` and `v ↦ w`. For each
application of the table, we extract the appropriate entry from it application of the table, we extract the appropriate entry from it
using the `sub` rule. In particular, we use the ⊑-conj-R1 and using the `sub` rule. In particular, we use the ⊑-conj-R1 and