K-user mailing list

[Charles Jacobsen <charlie.jacobsen AT utah.edu>]

Hi all --

Being the newb that I am, I made a mistake when writing a rule that I wanted to share. Perhaps someone could explain why it lead to exponential behavior (it seems clear that it would), and if there is a built-in that accomplishes the same thing.

I wrote a simple rule for removing an item from a map. Here was the first version:

syntax Map ::= "(" "remove-from-map" "," Map "," Int ")" [function]
// (Assuming the key is in the map)
rule (remove-from-map,
       Head:Map Key1:Int |-> Value:K Tail:Map,
       Key2)
     =>
     Head Tail
     when Key1 ==Int Key2

This works correctly and I tested it with small maps, but for big maps, krun never terminates. I changed it to a "recursive" style:

syntax Map ::= "(" "remove-from-map" "," Map "," Int ")" [function]
// (Assuming key is in map, would probably want a base case otherwise)
// keys match, return new map with pair removed
rule (remove-from-map,
       Key1:Int |-> Value:K Tail:Map,
       Key2)
     =>
     Tail
     when Key1 ==Int Key2
// keys do not match, recurse on tail
rule (remove-from-map,
       Key1:Int |-> Value:K Tail:Map,
       Key2)
     =>
     Key1 |-> Value (remove-from-map, Tail, Key2)
     when notBool ( Key1 ==Int Key2 )

and this works too, but it's much faster. Apparently, matching in the middle leads to exponential behavior.