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

merge

Browse source
This commit is contained in:
wadler 2020-03-04 19:16:36 -03:00
commit de8c6ae3ef
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/plfa/part2/BigStep.lagda.md
View file

@ -24,7 +24,7 @@ after we have developed a denotational semantics for the lambda
calculus, at which point the proof is an easy corollary of properties calculus, at which point the proof is an easy corollary of properties
of the denotational semantics. of the denotational semantics.
We present the call-by-name strategy as a relation between an an input We present the call-by-name strategy as a relation between an input
term and an output value. Such a relation is often called a _big-step term and an output value. Such a relation is often called a _big-step
semantics_, written `M ⇓ V`, as it relates the input term `M` directly semantics_, written `M ⇓ V`, as it relates the input term `M` directly
to the final result `V`, in contrast to the small-step reduction to the final result `V`, in contrast to the small-step reduction

2
src/plfa/part2/Bisimulation.lagda.md
View file

@ -449,7 +449,7 @@ In its structure, it looks a little bit like a proof of progress:
~ ~ ~ ~
| | | |
| | | |
(ƛ x ⇒ N†) · V† --- —→ --- N† [ x := V ] (ƛ x ⇒ N†) · V† --- —→ --- N† [ x := V† ]
Since simulation commutes with values and `V` is a value, `V†` is also a value. Since simulation commutes with values and `V` is a value, `V†` is also a value.
Since simulation commutes with substitution and `N ~ N†` and `V ~ V†`, Since simulation commutes with substitution and `N ~ N†` and `V ~ V†`,