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

added explanation to exercise

Browse source
This commit is contained in:
Jeremy Siek 2020-05-06 15:01:41 -04:00
parent 3d614523dc
commit fcf981cfec
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -374,9 +374,11 @@ cbn→reduce {M}{Δ}{δ}{N′} M⇓c
#### Exercise `big-alt-implies-multi` (practice)
Formulate an alternative big-step semantics, of the form `M ↓ N`,
for call-by-name that uses substitution instead of environments.
Prove that `M ↓ N` implies `M —↠ N`.
Formulate an alternative big-step semantics, of the form `M ↓ N`, for
call-by-name that uses substitution instead of environments. That is,
the analogue of the application rule `⇓-app` should perform
substitution, as in `N [ M ]`, instead of extending the environment
with `M`. Prove that `M ↓ N` implies `M —↠ N`.
```
-- Your code goes here