discussion #1
discussion #1
Conversation
| @@ -220,18 +227,30 @@ Questions about this definition: | |||
| - do we really need ~> as a K construct? Can it be a label and thus the way K | |||
| deal with evaluation contexts just a particular methodology and not an | |||
| intrisic part of K ? Same question for =>. | |||
| Cosmin: Syntacticly at least, I would say "no" for both. From the implementation | |||
There was a problem hiding this comment.
When you say "no for both" you mean that we should NOT keep any of them as constructors, that is, that we should just replace them with particular labels? Since => actually has a meaning in K, I am tempted to at least keep this one as a constructor. Also, if we make ~> into a KLabel, then there is no point in keeping .K as a constructor, either. In fact, the two act together as what it called a "monad" in the denotational semantics world. In some sense, when one thinks of K, one also thinks of these two constructs; they occur in almost all definitions, repeatedly.
There was a problem hiding this comment.
Another issue with making ~> into a KLabel is that we'd then make no syntactic distinction between K and Item, which turned out several times to be a desired distinction.
There was a problem hiding this comment.
From an implementation perspective, I do want to modify the KORE data structure to allow for traversal of => and ~> as regular terms -- it makes lots of code smaller. Semantically, and in the K definition of KORE, I have no strong preference. I am also inclined to leave => as is. ~> on the other hand could be made into a regular assoc list easily -- from what I remember, it already is in the latest Java backend implementation.
There was a problem hiding this comment.
I think the distinction between K and KItem could still be maintained at the sort level.
not meant to be merged.