K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

You will also need a rule for the case when the key is not in the map.
Something like this should work (I did not test it, you may need to replace . 
with .Map):

rule (remove-from-map, (Key |-> _ => .) _, Key)
rule (remove-from-map, M, Key) => M when notBool Key in keys(M)

Grigore



________________________________________
From: 
k-user-bounces AT cs.uiuc.edu
 
[k-user-bounces AT cs.uiuc.edu]
 on behalf of Dorel Lucanu 
[dlucanu AT info.uaic.ro]
Sent: Thursday, July 18, 2013 1:12 PM
To: 
k-user AT cs.uiuc.edu
Subject: Re: [K-user] learn from my mistake: rule lead to exponential   
behavior

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

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user