K-user mailing list

[Mark Hills <markhills1 AT gmail.com>]

It's probably not the match in the middle, it's more likely the condition, since (assuming this becomes a condition in Maude, I'm not familiar with the translation at this point) this will cause a huge amount of backtracking as the variables are bound, the condition is checked, it fails, and then Maude keeps trying new matches in an attempt to satisfy the condition. I would use Dorel's solution, which just leverages matching.

Cheers,

Mark

On Jul 18, 2013 6:23 PM, "Stefan Ciobaca" <stefan.ciobaca AT gmail.com> wrote:

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
>
_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user