k-user AT lists.cs.illinois.edu
Subject: K-user mailing list
List archive
- From: Charles Jacobsen <charlie.jacobsen AT utah.edu>
- To: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
- Subject: [K-user] Semantics of lists, sets, and bags
- Date: Sat, 8 Jun 2013 01:19:21 +0000
- Accept-language: en-US
- List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
- List-id: <k-user.cs.uiuc.edu>
Greetings ---
Are the semantics of built-in lists, sets, and bags available? For example, I found the following simple rule natural, but wanted to see why it works (looking at the relevant rule):
<some-list-cell> ... (.List => ListItem(15)) ... </some-list-cell>
This means we can insert anywhere in a list.
This next rule is a bit perplexing, due to the configuration abstraction (found in the imp++ tutorial):
rule <k> spawn S => T ...</k> <env> Rho </env>
(. => <thread>... <k> S </k> <env> Rho </env> <id> T </id> ...</thread>)
It seems like the implied configuration, wrapping this, is:
rule <thread>
<k> spawn S => T ...</k> <env> Rho </env>
(. => <thread>... <k> S </k> <env> Rho </env> <id> T </id> ...</thread>)
</thread>
as only <k> and <env> cells appear in <thread> cells; but I think that is not correct. I think the implied configuration is:
rule <threads>
...
<thread>
...
<k> spawn S => T ...</k>
<env> Rho </env>
...
</thread>
Are the semantics of built-in lists, sets, and bags available? For example, I found the following simple rule natural, but wanted to see why it works (looking at the relevant rule):
<some-list-cell> ... (.List => ListItem(15)) ... </some-list-cell>
This means we can insert anywhere in a list.
This next rule is a bit perplexing, due to the configuration abstraction (found in the imp++ tutorial):
rule <k> spawn S => T ...</k> <env> Rho </env>
(. => <thread>... <k> S </k> <env> Rho </env> <id> T </id> ...</thread>)
It seems like the implied configuration, wrapping this, is:
rule <thread>
<k> spawn S => T ...</k> <env> Rho </env>
(. => <thread>... <k> S </k> <env> Rho </env> <id> T </id> ...</thread>)
</thread>
as only <k> and <env> cells appear in <thread> cells; but I think that is not correct. I think the implied configuration is:
rule <threads>
...
<thread>
...
<k> spawn S => T ...</k>
<env> Rho </env>
...
</thread>
(. => <thread>... <k> S </k> <env> Rho </env> <id> T </id> ...</thread>)
...
</threads>
...
</threads>
Is that correct? I am not sure.
Charlie (undergrad)
Charlie (undergrad)
- [K-user] Semantics of lists, sets, and bags, Charles Jacobsen, 06/07/2013
- Re: [K-user] Semantics of lists, sets, and bags, Dorel Lucanu, 06/08/2013
- Re: [K-user] Semantics of lists, sets, and bags, Charles Jacobsen, 06/08/2013
- Re: [K-user] Semantics of lists, sets, and bags, Dorel Lucanu, 06/08/2013
Archive powered by MHonArc 2.6.16.