From dc7da4961b75b9e40bb41692aba13770bce7e72e Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Wed, 19 Feb 2020 15:59:44 -0500 Subject: [PATCH 1/2] fixed typo --- src/plfa/part2/Bisimulation.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/Bisimulation.lagda.md b/src/plfa/part2/Bisimulation.lagda.md index dfe23bc3..de161ea8 100644 --- a/src/plfa/part2/Bisimulation.lagda.md +++ b/src/plfa/part2/Bisimulation.lagda.md @@ -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 substitution and `N ~ N†` and `V ~ V†`, From 6f27a9b7e60169c36ba77258710a8dafdff1b629 Mon Sep 17 00:00:00 2001 From: Alexandre Moreno Date: Thu, 20 Feb 2020 13:10:04 +0800 Subject: [PATCH 2/2] fix typo --- src/plfa/part2/BigStep.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/BigStep.lagda.md b/src/plfa/part2/BigStep.lagda.md index 1db1a1fd..f438d258 100644 --- a/src/plfa/part2/BigStep.lagda.md +++ b/src/plfa/part2/BigStep.lagda.md @@ -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 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 semantics_, written `M ⇓ V`, as it relates the input term `M` directly to the final result `V`, in contrast to the small-step reduction