Comparison of priority rules in pattern matching and term rewriting

AbstractProgramming languages such as ML provide function calls with pattern matching. For each function, there is a given set of patterns for arguments with the corresponding definition of the function. Cases corresponding to different patterns of a given function may not be exclusive, and often a priority rule (typically the order of the program text) is followed to disambiguate overlapping cases. In this paper, term rewriting systems are taken as models for function calls with pattern matching. It is shown that, in the useful set of constructors based linear systems, all priority rules are essentially equivalent. Moreover the translation from one rule to another one may be mechanically done. These results hold both for lazy and eager evaluations