A strange convention in K update map function.

[liyili2]

Hi, When I use the map function in the following rules:

module TEST

     configuration <k>$PGM:K</k><types>.Map</types>

     syntax KItem ::= "start"

     syntax Type ::= "int"

     syntax Id ::= "$x"

     rule <k> start => .</k>
          <types>M => M [int <- $x]</types>

endmodule

If I run the program "start", I found that the output is like:

<k>
    .K
</k>
<types>
    int |-> $x
</types>

There is nothing wrong with the implementation of the update function in Map. However, the convention is very strange. When you hand the syntax "M[ K2 <- K1]" to someone in programming language field, 99% people will think of updating the Map by mapping K1 to K2 instead of the opposite case such as mapping K2 to K1. In addition, I also checked the use of the mapping symbol in the original C semantics and the guy who creates C semantics actually use the same idea as M[ Value <- ID ]. I would strongly recommend we change the meaning of the symbol M[ID <- Value] back to M[Value <- ID], or we can change the symbol to M[ID -> Value].

[grosu]

Liyi,

This is standard notation in PL. See, for example, Pierce's book on types for PL.

When you hand the syntax "M[ K2 <- K1]" to someone in programming language field, 99% people will think of updating the Map by mapping K1 to K2 instead of the opposite case such as mapping K2 to K1.

Where did you come up with this 99% statistics? Just ask some people to see what they say. You will be surprised :)

In addition, I also checked the use of the mapping symbol in the original C semantics and the guy who creates C semantics actually use the same idea as M[ Value <- ID ].

I don't believe this. Show me. The typical alternatives are map[key <- value] vs map[value/key]. It is very rare the case you see map[value <- key], typically in confused students' homeworks. The reason we dropped map[value/key] is because that interferes with substitution, which has the same notation, as well as with arrays and division.

I would strongly recommend we change the meaning of the symbol M[ID <- Value] back to M[Value <- ID],

We have NEVER had M[Value <- ID].

Grigore

---

From: Liyi Li [notifications@github.com] Sent: Sunday, July 20, 2014 2:31 PM To: kframework/k Subject: [k] A strange convention in K update map function. (#737)

Hi, When I use the map function in the following rules:

module TEST

 configuration <k>$PGM:K</k><types>.Map</types>

 syntax KItem ::= "start"

 syntax Type ::= "int"

 syntax Id ::= "$x"

 rule <k> start => .</k>
      <types>M => M [int <- $x]</types>

endmodule

If I run the program "start", I found that the output is like:

.K int |-> $x

There is nothing wrong with the implementation of the update function in Map. However, the convention is very strange. When you hand the syntax "M[ K2 <- K1]" to someone in programming language field, 99% people will think of updating the Map by mapping K1 to K2 instead of the opposite case such as mapping K2 to K1. In addition, I also checked the use of the mapping symbol in the original C semantics and the guy who creates C semantics actually use the same idea as M[ Value <- ID ]. I would strongly recommend we change the meaning of the symbol M[ID <- Value] back to M[Value <- ID], or we can change the symbol to M[ID -> Value].

— Reply to this email directly or view it on GitHubhttps://github.com/kframework/k/issues/737.

[liyili2]

If you think "map[Id <- Value]" is more common, it is fine for me to keep this convention; however, I think "map[Value/Id]" and "map[Id -> Value]" are more common notations. I rarely see papers to use the notation of "map[Id <- Value]". This is just my opinion.

[liyili2]

However, I don't agree with that you claim that "We have NEVER had M[Value <- ID]", that is why I see in the C semantics in Maude, and it is defined by the guy who designed the C semantics. I think it must appear in somewhere sometime. Otherwise, it is hard for me to believe that the guy will use the notation and give the rules for the notation without seeing it in some K definitions.

[grosu]

Liyi, you already said that M[Value <- ID] is more common, and I asked you for proof. Show us ONE place where they use M[Value <- ID] to mean what we now mean by M[ID <- Value]. Now you are just repeating yourself without bringing any proof. Also, please be careful at the orientation of <-, because in the message before the previous one you suddenly wrote -> instead of <-.

Grigore

---

From: Liyi Li [notifications@github.com] Sent: Monday, July 21, 2014 1:26 AM To: kframework/k Cc: Rosu, Grigore Subject: Re: [k] A strange convention in K update map function. (#737)

If you think "map[Id <- Value]" is more common, it is fine for me to keep this convention; however, I think "map[Value/Id]" and "map[Id -> Value]" are more common notation. I rarely see papers to use the notation of "map[Id <- Value]". This is just my opinion.

— Reply to this email directly or view it on GitHubhttps://github.com/kframework/k/issues/737#issuecomment-49574918.

[grosu]

Note that, besides the notations M[X <- V] and M[V/X] that we used for map updates so far, there is a plethora of other notations in the literature: M[X |-> V], M{X |-> V}, [X |-> V]M, {X |-> V}M, all the above with X := V instead of X |-> V, etc. But I have never seen M[V <- X]. The notation M[X <- V] is relatively common, and is inspired from the fact that X <- V means "X takes the value V" in some languages (OCAML, F#).

Grigore

---

From: Liyi Li [notifications@github.com] Sent: Monday, July 21, 2014 1:31 AM To: kframework/k Cc: Rosu, Grigore Subject: Re: [k] A strange convention in K update map function. (#737)

However, I don't agree with that you claim that "We have NEVER had M[Value <- ID]", that is why I see in the C semantics in Maude, and it is defined by the guy who designed the C semantics. I think it must appear in somewhere sometime. Otherwise, it is hard for me to believe that the guy will use the notation and give the rules for the notation without seeing it in some K definitions.

— Reply to this email directly or view it on GitHubhttps://github.com/kframework/k/issues/737#issuecomment-49575139.