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

small fixes to Lambda

Browse source
This commit is contained in:
Philip Wadler 2019-01-09 11:12:23 +00:00
parent ad6f853946
commit 56ac5c007e
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/plfa/Lambda.lagda
View file

@ -464,7 +464,7 @@ Let's unpack the first three cases:
with `x`, the variable in the term. If they are the same, with `x`, the variable in the term. If they are the same,
we yield `V`, otherwise we yield `x` unchanged. we yield `V`, otherwise we yield `x` unchanged.
* For abstractions, we compare `w`, the variable we are substituting for, * For abstractions, we compare `y`, the substituted variable,
with `x`, the variable bound in the abstraction. If they are the same, with `x`, the variable bound in the abstraction. If they are the same,
we yield the abstraction unchanged, otherwise we subsititute inside the body. we yield the abstraction unchanged, otherwise we subsititute inside the body.
@ -531,14 +531,14 @@ In an informal presentation of the operational semantics,
the rules for reduction of applications are written as follows: the rules for reduction of applications are written as follows:
L —→ L′ L —→ L′
-------------- ξ-·₁ --------------- ξ-·₁
L · M —→ L′ · M L · M —→ L′ · M
M —→ M′ M —→ M′
-------------- ξ-·₂ -------------- ξ-·₂
V · M —→ V · M′ V · M —→ V · M′
---------------------------- β-ƛ ----------------------------- β-ƛ
(ƛ x ⇒ N) · V —→ N [ x := V ] (ƛ x ⇒ N) · V —→ N [ x := V ]
The Agda version of the rules below will be similar, except that universal The Agda version of the rules below will be similar, except that universal