Transformation of Map Elements in Function

[dreamqin68]

Hello,

I've encountered difficulty in recursively exchanging elements in a map from (key, value) to (value, key) using a function.

While method can achieve such transformations, I'm curious if there are any approaches that utilize function for this purpose.

method revKeyVal(oldMap:map<nat, string>) returns (newMap:map<string, nat>)
{
    var items := oldMap.Items;
    newMap := map[];

    while items != {}
        decreases |items|
    {
        var item :| item in items;
        newMap := newMap + map[item.1 := item.0];

        items := items - { item };
    }

    return newMap;
}

Thanks!

[racko]

I'm curious if there are any approaches that utilize function for this purpose.

Yes, there are. Do you have more concrete questions we can help you with? 🙂

Two tips:

• Using Map Comprehension Expressions you can usually avoid even the recursive function. You will probably get "Error: key expressions might be referring to the same value", which should raise a few questions.
• Adapting https://leino.science/papers/krml275.html should help you avoid some pitfalls in solving the problem using a recursive function. Just remember that the paper was written when function was function method and ghost function was function.

[dreamqin68]

Thanks a lot!

When writing the statement var x :| x in s; // s is a set within a function, an error occurs stating

to be compilable, the value of a let-such-that expression must be uniquely determined.

Placing this statement in a ghost function does not produce this error.

function MapToSequence<A,B>(m: map<A,B>): seq<(A,B)> 
{
  var keys := SetToSequence(m.Keys);
  seq(|keys|, i requires 0 <= i < |keys| => (keys[i], m[keys[i]]))
}

ghost function SetToSequence<A>(s: set<A>): seq<A>
  ensures var q := SetToSequence(s);
    forall i :: 0 <= i < |q| ==> q[i] in s
{
  if s == {} then [] else
    var x :| x in s;
    [x] + SetToSequence(s - {x})
}

Yet, attempting to call the ghost function within a function results in another error:

ghost variables such as keys are allowed only in specification contexts. keys was inferred to be ghost based on its declaration or initialization.

It's apparent that a ghost function can only be invoked in a ghost context.

I'm seeking clarification on how to establish a ghost context such that the MapToSequence function can be successfully verified. Thanks!

[racko]

I'm seeking clarification on how to establish a ghost context such that the MapToSequence function can be successfully verified.

I don't think that this is going in the right direction.

The second link I provided above explains how to implement MapToSequence. Concretely sections 2. Making the function compilable to 4. Proving there's a minimum answer it for the concrete case of set<int> comparable to your original question about map<nat, string> and sections 5. Total orders to 8. Coming back to map to sequence answer it for the generic case you are asking about here.

For the nat case, here's a bit more to help you along:

lemma MinKeyExists(m: map<nat, string>)
  requires m != map[]
  ensures exists key <- m :: forall k <- m :: key <= k

function revKeyVal(oldMap: map<nat, string>): map<string, nat>
{
  if oldMap == map[] then
    map[]
  else
    MinKeyExists(oldMap);
    var key :| key in oldMap && forall k <- oldMap :: key <= k;
    revKeyVal(oldMap - {key})[oldMap[key] := key]
}

[dreamqin68]

It's really helpful! Thank you!

[parno]

You could also use the Invert function from the standard library:

dafny/Source/DafnyStandardLibraries/src/Std/Collections/Map.dfy

Line 98 in 7e81f44

ghost function {:opaque} Invert<X, Y>(m: map<X, Y>): map<Y, X>

[dreamqin68]

Thanks a lot! It's really a straightforward and useful ghost function.