K-user mailing list

[Stefan Ciobaca <stefan.ciobaca AT gmail.com>]

It's probably due to the matching in the middle: if you fix one key in
a map with n keys, there are 2^(n-1) ways to split the rest of the map
into Head and Tail.

Since you don't care about this separation into Head and Tail (you
concatenate them in the end), your second rule ("key |-> _ , Rest =>
Rest") works much better: there is only one way to choose Rest once
you fix the key.

Cheers,
Stefan

On Thu, Jul 18, 2013 at 6:14 PM, Charles Jacobsen
<charlie.jacobsen AT utah.edu>
 wrote:
> 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.
>
> _______________________________________________
> k-user mailing list
> k-user AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>