Modify small-step reduction to eliminate "stuck" expressions#2
Merged
ivg merged 4 commits intoBinaryAnalysisPlatform:masterfrom May 16, 2018
Merged
Modify small-step reduction to eliminate "stuck" expressions#2ivg merged 4 commits intoBinaryAnalysisPlatform:masterfrom
ivg merged 4 commits intoBinaryAnalysisPlatform:masterfrom
Conversation
This is achieved by: a) replacing premises of the form e ~> v with "step" rules that do incremental evaluation of subexpresions, and b) reworking variable and let rules to avoid the need to modify the context while evaluating subexpressions
ivg
requested changes
May 16, 2018
Member
ivg
left a comment
ivg
left a comment
There was a problem hiding this comment.
Nice job, now it's much better!
Can you please add some wording for the multistep reduce rule? It appears only in the last page but is used in the premises from the very beginning without any ado. And although intuition tells correctly what it does, it is better not to rely on other's intuition :)
ivg
reviewed
May 16, 2018
bil.ott
Outdated
| delta |- e ~>* e | ||
|
|
||
| delta1 |- e1 ~> e2 | ||
| delta2 |- e2 ~>* e3 |
Member
There was a problem hiding this comment.
Why are we using different deltas here? To my understanding it should be
delta |- e1 ~> e2
delta |- e2 ~>* e3
----------------------- reduce
delta |- e1 ~>* e3
Contributor
Author
There was a problem hiding this comment.
You are correct - sorry for this error (it's a hold-over from the previous iteration that had the expression reduction relation modify the environment).
I'll fix this and add a sentence or two explaining the ~>* relation to the latex file.
ivg
requested changes
May 16, 2018
bil.tex
Outdated
| \end{description} | ||
|
|
||
| This section also defines $\Delta \vdash e_1 \leadsto^{*} e_2$. This relation | ||
| is the reflexive, transitive closure of $\leadsto$ and use useful to describe |
ivg
approved these changes
May 16, 2018
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is achieved by:
a) replacing premises of the form e ~> v with "step" rules that do
incremental evaluation of subexpresions, and
b) reworking variable and let rules to avoid the need to modify the
context while evaluating subexpressions