Map Structure
From CoreASM Wiki
Contents |
Preliminary consideration
Do we really need maps? Maps have traditionally be defined (encoded?) through dynamic functions, with the occasional "difficult" operation being the copying of a map, e.g.
forall k in dom(src) do dst(k):=src(k)
The mathematically pure definition of a map is, indeed, the same as a function: [1].
Implementing Maps
If we do decide that we need explicit Maps, there are several ways to implement the internal data structure of Maps in CoreASM:
A Universal Map Structure Function
We can model maps through a universal map structure function in the state that maintains the internal structure of any map (i.e., not having a Map background). Such a function would be defined as:
mapping: Map x Element --> Element
Then we would have:
getValue(('mapping', <m, k>)) = internalMapping(m, k)
and
rule SetValue(m, k, v) = internalMapping(m, k) := v
Where internalMapping represents the internal structure of maps in the engine's world.
So we would have the following pattern defined:
{ k1 -> v1, ..., kn -> vn } --> extend MAP_ELEMENT with m in
forall i in [1..n] do
internalMapping(m, ki) := vi
[[pos]] := (undef, undef, m)
Advantages
- Maps can be modified in CoreASM by simply updating the mapping function. For example, the following rules add a new pair to the map myMap and at the same time remove a pair from that map:
mapping(myMap, 1) := 10 mapping(myMap, 5) := undef
Disadvantages
- We won't have a map background. As a result, the real value of a controlled function can be changed, without that function being updated. For example, the following rule adds a new pair to the map at myMap while the function myMap itself is not updated through a regular ASM update:
// initially, myMap holds { 1 -> 5, 2 -> 10 }
mapping(myMap, 3) := 15
// now, myMap holds { 1 -> 5, 2 -> 10, 3 -> 15} while the function
// itself is not updated and it still holds the same value
- Another major disadvantage (related to the one above) is that we would loose value semantics for maps. In fact, myMap would logically be a reference to the map, not its value, hence we could end up in situations where two different maps compare equal under =, even if they map the same key to different values. In turn, this would destroy safety in function access, e.g. the location <f,myMap> would be the same of <f,otherMap>, even if myMap and otherMap have different values.
Maps with Internal Structures
We can model maps with an internal structure which is not explicit in the state. We can introduce a map background which holds all the possible maps. We will then have derived functions that allow us to see (i.e., read) the data of map values, and we will have rules with aggregation to update them.
With this approach, we can have a derived function mapping defined as follows:
mapping: Map x Element --> Element
where
getValue(('mapping', <m, k>)) = internalMapping(m, k)
We would then have the following rule forms to modify a map:
put (key, value) into map remove key from map
Those rules will generate update instructions that instrucuts respected changes to the location map and those instructions will be aggregated at the end to form a single update to the location map.
We would also define the following pattern:
{ k1 -> v1, ..., kn -> vn } --> extend MAP_ELEMENT with m in
forall i in [1..n] do
internalMapping(m, ki) := vi
[[pos]] := (undef, undef, m)
Advantages
- We have a map background. As a result, the problem that we had with the other approach disappears; i.e., real value of a controlled function that holds a map is changed if we modify that function. For example:
// initially, myMap holds { 1 -> 5, 2 -> 10 }
put (3, 15) into myMap
// now, myMap holds { 1 -> 5, 2 -> 10, 3 -> 15} and its value is changed through an update
Disadvantage
- We have to update maps through rules.
- To support simultaneous updates to a map, we have to define aggregation methods for map operations.
Not having maps
Do we really need maps? After all, a map is a function, e.g. (for a new function map)
map(k):=v
is equivalent to
map = { k->v }
Then, maybe we can just provide a constructor { ..->.. } to designate literals, and operations to merge/override functions, e.g.
map := map + { k->v }
Note: This line in fact should be@map := @map + { k -> v}asmapitself is a location which has no argument and updating that will not (and should not) update the function that is bind to the name map. It's the same with the second line above: there we should instead have@map := {k -> v}. This is a tricky issue and it also happens in discussion regarding sets.
Now, should we assign a location to@foowhere foo is a function name? We had some discussions here about this and I was planning to bring it up next week, after we released 0.9-beta. Uwe had a good point: one should be careful here as in theory one can change infinite locations in one step by a single update:@foo := @another-foo. There is also another issue: depending on the design, one may need to extend the meaning of inconsistent updates. I will write about this issue in more details. Now, I have to get back to 0.9-beta. :) Trident 10:07, 29 September 2006 (PDT)
would just add the mapping k->v to map, and would be equivalent (i.e., generate the same next state as)
map(k):=v
Notice however that in the latter case only the update ((map,<k>),v) is generated, whereas in the former updates for the entire domain of map, plus k, are generated.
In summary, we may opt not to have a Map type at all, but just a background which provides advanced operations on functions. Interactions with the proposed @function notation should also be considered.
Advantages
- Map-like operations are available in a generic way for any function.
- Semantics can be expressed in term of simpler ASM operations — no "special" knowledge required.
- Functions already behave as they should in all cases, so this model is relatively safe.
Disadvantages
- All maps have to be named with this approach; we won't be able to create runtime sets of maps that are not individually bound to state locations. Trident
- Why? A value like { 1->2 } would be a FunctionElement, not necessarily stored in the state (it would be the result of an expression, most like @f in the middle of expression evaluation). In fact, {1->2}(1) should yield 2, whereas {1->2}(x) for any other x would yield undef. --Vincenzo 17:49, 1 October 2006 (PDT)
- Several operations will have to loop over the entire domain of a function, and may be costly if used carelessly
