K-user mailing list

[Dorel Lucanu <dlucanu AT info.uaic.ro>]

Did you try the following rule?

rule (remove-from-map,
       Head:Map Key2:Int |-> Value:K Tail:Map,
       Key2)
     =>
     Head Tail

?


On 7/18/13 7:21 PM, Stefan Ciobaca 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