Rewrite rules containing mappings

[twillems]

There might be an issue with pattern matching when using mappings as an argument of other mappings, as the following specification, derived from an example by Myrthe Spronck, suggests:

map N:Nat;
    modify: Nat # List(Nat) -> List(Nat);
var l:List(Nat);
eqn N = 10;
    modify(N,l) = l;

act a;
proc P(l:List(Nat)) = a. P(modify(N,l));
init P([0,1]);

Replacing the mapping N in the rule for modify by the value 10 resolves the issue and leads to a finite state space. The example as it is currently generates an infinite number of states.

Steps to reproduce: glue the specification in mcrl2IDE and try generating a state space.

[tneele]

To make the issue more clear, consider the following. Load the specification above into a file a.mcrl2 and execute:

mcrl22lps a.mcrl2 a.lps
mcrl2i a.lps

In the prompt of mcrl2i, enter the following:

mCRL2 interpreter (type h for help)
? e modify(N, [])
modify(10, [])

According to @twillems, the expected result is [], while the actual result is modify(10, []).

[jgroote]

I think this is expected behaviour.

Within the context of the rewrite rules:

eqn N = 10; modify(N,l) = l;

the expression modify(N,[]) rewrites to modify(10,[]). This does not match with modify(N,l), because 10 does not match with N.

Hence, it does not rewrite.

This problem occurs in more contexts and is in my opinion a real disadvantage of using rewrite rules. Question is should we change this, and then the question is what is the correct way, and how to implement this. A suggestion could be to rewrite the lhs of the rewrite rules to normal form, before generating a rewrite system. But should we do this until we reach a fixed point in the form of the lhs's?