Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

discussion #1

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

discussion #1

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 24 additions & 4 deletions kore.maude
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,13 @@ mod KORE is
--- For example, we cannot write `_+_` in Maude; so we'll write #Label("_+_").
--- For maximum clarity, we will also include a separate sort for each type of token.
including STRING .
sorts Label Token Variable Application Item K KList . --- we call these "K Label", etc.
sorts Label Token Variable Application Item K KList Sort . --- we call these "K Label", etc.
subsorts Token Variable Application < Item < K < KList .
op #Label : String -> Label .
op #Token : String String -> Token .
op #Variable : String String -> Variable .
op _`(_`) : Label KList -> Application .
op #Token : Sort String -> Token . --- Cosmin: if we have sorts, it may be good to have them explicitly "String String" is confusing
op #Sort : String -> Sort .
op #Variable : Sort String -> Variable .
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good idea to move the Sort declaration here, and then to use the actual sort construct in variables and tokens.

op _`(_`) : Label KList -> Application . --- Cosmin: would it be correct to "Application => Term"?
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For uniformity, I would keep it Application. The other two (Token and Variable) are also Term constructs. We may replace Item with Term, but that would be confusing, because one can argue that K is also a term.

op .K : -> K . --- .::K instead of .K gives a parsing error
op _~>_ : K K -> K [assoc id: .K] . --- "assoc" has only parsing meaning here; id not needed
op .KList : -> KList .
Expand All @@ -19,6 +20,7 @@ mod KORE is
--- Not sure about _~>_ and _,_ being associative at this level. Like for other K
--- definitions, we may want to have a syntax for parsing KORE and another syntax
--- for the semantics of KORE
--- Cosmin: yes, the assoc problem for KList seems the same as the usual user lists problem, just at the meta-level
----------------------------------

*** K rewriting
Expand All @@ -34,6 +36,8 @@ mod KORE is
op next_ : K -> K .
op exists__ : Variable K -> K .
--- requires/ensures = sugar: "C[K1 => K2] requires K3 ensures K4" is "C[K1 /\ K3 => K2 /\ K4]"
--- Cosmin: yes, and it may be nice to move away from the sugar. "C[K1 /\ K3 => K2 /\ K4]" is both shorter and clearer.
--- also, even in the current Java backend implementation, /\ would work well and be faster

*** Attributes
--- In the past, I proposed to just use KList for Attributes, but my proposal was rejected.
Expand All @@ -44,6 +48,9 @@ mod KORE is
op .AttributeList : -> AttributeList .
op _,_ : Attribute AttributeList -> AttributeList [format(d d s d)] .
op [_] : AttributeList -> Attributes .
--- Cosmin: from my perspective, if we allow parsing empty KLists from "" instead of ".KList" (the same trick we do for user lists),
--- using labeled syntax for attributes should work well. It's annoying to write "foo(a, .KList)" and "foo(.KList)", but "foo(a)"
--- and "foo()" work well.

*** Outer
sort Definition .
Expand Down Expand Up @@ -220,23 +227,36 @@ 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
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the distinction between K and KItem could still be maintained at the sort level.

perspective, this will simplify traversal code even further.
- rename .::K and .::KList to . ? if we get rid of ~> as above, then we may
only need .::KList.
Cosmin: I agree.
- Should we allow empty productions instead of sort declarations? A pro
argument is that we have fewer syntactic constructs. A cons argument is
that a sort declaration may be regarded as a different entityr, with
different kinds of attributes.
Cosmin: I don't quite follow.
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It refers to this syntax declaration of sorts:

 op syntax__ : Sort Attributes -> Sentence .

That is, instead of

syntax Sort [Att]

to write

syntax Sort ::=   [Att]

(a normal production, but empty)

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't quite like this because syntax Sort ::= [Att] make it seem like this is a sort for nothing.

I have also been thinking of eliminating sort declarations, but not by replacing them with productions but by replacing them to with subsorts. Instead of writing:

syntax Foo

it would be

syntax Top ::= Foo

As I said before, my preference would to be have a special sort sentence and be able to do:

sort Foo < Top

I understand we may want to have all sorts represented as undeleted injections, but I think we're very far from there and introducing a sort sentence would clarify things in the meantime. It will also make it clearer if we represent sorts as injections. We would know that if we eliminate all the sort sentences we are there.

- Should we add constant AttributeKeys which have special semantics, like
"strict", as constants?
Cosmin: we may want to discuss the attribute syntax separately.
- Brackets and disappearing injections are the same thing, arent's they? A
production which only has one non-terminal and the production disappears
from the AST.
Cosmin: Yes, I also think they can be seen as the same thing. That being
said, I would really like for injections to not dissapear. If something
is meant to dissapear, it should be declared as a subsort. And the
dissapearing injections (including subsorts) could be done via rules as
we discussed before.
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would be reluctant to add a new construct, subsort. Can we for now use it as an attribute to productions that can be subsorts? I am actually tempted to not encourage the use of subsorts, as they get very very complicated quickly. For example, a term does not always have a least sort unless some tricky regularity restrictions are respected. I've spent several years doing research on order-sorted algebra, my first paper was on that topic, and it is a hugely complicated matter theoretically. That's why Meseguer, one of its fathers, invented the more general membership equational logic.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've stared arguing for this again in the previous message. I agree it would be nice to do without sorts but the reality is that we do have them now. Keeping them as second-hand citizens for which magic things happen is confusing. Changing the default behavior of syntax A ::= B from subsorting to a regular production would help.

Can we for now use it as an attribute to productions that can be subsorts?

I'm a bit worried about adding semantics to the attributes, but it could work as an intermediate solution from my perspective.

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I forgot to answer this. We already have many attributes that have semantic meaning. The "bracket" attribute is perhaps the closest in spirit to what "subsort" would do (i.e., not add a node in the AST). So I'd be tempted to keep it as is for now, that is, to have two different syntax constructs, one for introducing sorts and another for productions (https://github.com/grosu/kore-in-maude/blob/master/kore.maude#L88-L89).

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok. The question is: is the injection klabel from syntax A ::= B (written exactly like this, with no attributes) automatically removed?

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No. I think by default all productions should have unique labels associated to them. If you do not want a label, then you can put some attribute, like bracket or subsort, which will generate a rule that removes the label. I am not concerned about attaching semantics to labels, because we already do it anyway with several of them, and so does maude, obj, cafeobj, etc.

Sent from my Verizon Wireless 4G LTE smartphone

-------- Original message --------
From: Cosmin Radoi [email protected]
Date: 04/07/2016 08:00 (GMT+01:00)
To: grosu/kore-in-maude [email protected]
Cc: "Rosu, Grigore" [email protected]
Subject: Re: [grosu/kore-in-maude] discussion (#1)

In kore.maudehttps://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_grosu_kore-2Din-2Dmaude_pull_1-23discussion-5Fr58822475&d=BQMCaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=gBub4ab7wvmjFVEDwsswdud0fptTHrGi3G4Zzc5Kwds&m=tMtUt_dmUvCV0T_JOIsgBhmzc6E1OutCg6ZyD-urFck&s=qKJvEl_2QoXxWYYUzeRrKbQiCLmlA7hIdeNiJwscfbo&e=:

  • Brackets and disappearing injections are the same thing, arent's they? A
    production which only has one non-terminal and the production disappears
    from the AST.
    • Cosmin: Yes, I also think they can be seen as the same thing. That being
    •      said, I would really like for injections to not dissapear. If something

    •      is meant to dissapear, it should be declared as a subsort. And the

    •      dissapearing injections (including subsorts) could be done via rules as

    •      we discussed before.

Ok. The question is: is the injection klabel from syntax A ::= B (written exactly like this, with no attributes) automatically removed?

—
You are receiving this because you commented.
Reply to this email directly or view it on GitHubhttps://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_grosu_kore-2Din-2Dmaude_pull_1_files_c30c2bc78e45acdfc81ba5555f94fbe58d537506-23r58822475&d=BQMCaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=gBub4ab7wvmjFVEDwsswdud0fptTHrGi3G4Zzc5Kwds&m=tMtUt_dmUvCV0T_JOIsgBhmzc6E1OutCg6ZyD-urFck&s=6H_YP_qGNYMqYS-rBZYqnKWwtOK_lzKSqL2BFTMWSD8&e=

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But I can always write

syntax Exp ::= "(" Exp ")"  [klabel(abc)]
rule abc(E) => E  [macro]

and I would expect it to mean exactly the same thing as

syntax Exp ::= "(" Exp ")"  [bracket]

Then what's the point in having two different internal representations for two things which are identical by all means?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree. We could simply go with the first representation if we want to get rid of a special attribute. I don't have any strong preference here.

My main concern is the production vs subsort sentence distinction.

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I'd prefer to keep KORE simpler. Whatever KORE we end up with after this discussion, is what I plan to call "the K Standard" that all implementations should support. I can easily see implementations which do not even want to have a "bracket" attribute.

Regarding the subsort vs production, I would have a bold proposal: let us get rid of subsorts all together from KORE, and let implementations decide on their own if they want to implement subsorts. That is, let us simply require that each production has a klabel, including all the injection productions. The injections will also need to be strict.

From a theoretical perspective, the order-sorted algebra community is well aware of the fact that subsorts can be simulated with injections, specifically by adding for any sorts S1 < S2 < S3 equations

eq injS2inS3(injS1inS2(X:S1)) = injS1inS3(X)

and then everything happens modulo such equations, including matching. The rest is just implementation detail, and I believe that some may not want to implement subsorts in their backend; for example the Coq backend.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I understand this and agree. The problem is that we do have sorts now, and many passes in the compiler and the backend rely on them. Removing them is not something we can solve in the short term. As we don't want them there eventually, we can avoid adding the subsort sentence to the KORE syntax. But I do want it there for the implementation. This will actually help when eventually removing sorts, as we have the productions clearly identified (via Java typing, not just checking for an elusive attribute).

So, my concrete proposal is:

  1. Have syntax A ::= B actually mean an injection, not a subsort. Subsorts would need to be syntax A ::= B [subsort]
  2. The data structures will have separate Production and Subsort classes, instantiated depending on the subsort attribute.
  3. Eliminate syntax A and replace it with syntax K ::= A [subsort] (I don't feel strongly about this)

What do you think?

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree with 1 and 2, but I would keep 3 as is, because in most definitions the sort K does not even appear. In the usual definitions, which are purely syntactic, the top sort K may even be looked at as just an implementation detail of the K framework. Also, the only reason for which we need sort declarations is because we want to attach them attributes, like hooks to builtin data-types. If we write it syntax K ::= A, people may think of it as an injection and of attaching the attributes to an injection and not to a sort. People may also think that they need to do explicitly inject all the sorts into K.

- Should #Label contain more structured information than just a String?
Cosmin: From my perspective, its semantics and any other information should live
with the definition (module), not within the label.

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So the answer is NO? I was thinking more about implementing kompile using Maude and this definition of KORE. In that case, instead of having a table holding for each KLabel where it comes from, including its argument sorts and its result sort, all that information could have already been part of the KLabel term. Or are you saying that we may only need to add the module name info to the KLabel term, and then we will be able to get the info from there?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So far, I kind of saw this as an implementation detail. Once "resolved" to a module, the information for the klabel is clear (modulo overloaded klabels). It's up to the particular backend to choose between looking up the information from the module every time, having a direct reference to the KLabel information, or doing something completely different (e.g., instantiates a different class).

I can also see the advantage is keeping the information attached to the KLabel in KORE already. It would allow us to drop all syntax productions from a definition and it would still be valid. But it will come with a space overhead. I'm not sure it is worth it.

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, it is too much to keep all the syntax information attached to the KLabel. It would make the KORE definitions almost unreadable, with a lot of repetition and redundancy. I was thinking of keeping only some crucial information, like the arity, or the module where the operation comes from. But at second thoughts I think we should not keep anything except its name. Since both sorts and labels act the same way wrt qualification, as symbols, then we would have to also keep the module attached to sorts, etc. Since until now we managed to survive without any additional information attached to labels, we will likely continue to survive.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree. Ok.

Comments about old kast.k and e-kore.k:
- Stop having particular module names mean particular things in KORE! You may do that in full K.
- Why do you call ATTRIBUTES a module which only defines one attribute?
- We agree on separating the attrbute listsand arguments with commas, not spaces.
- The current attributes are a mixture of K (you use the "token" attribute) and something
else. I continue to believe that attributes can be just a KList.
Cosmin: the attributes are definetely messed up and we should discuss and agree on them
- #emptyKProduction was never defined anywhere, but used in KProduction