Stop losing sleep over incomplete data type specifications
Jean-Jacques Thiel · 1984
We give an algorithm to test the completeness of definitions holding on the rewrite systems that they generate. At the opposite of existing techniques that are very restrictive (left-hand sides of definitions must be linear) or rather inefficient our solution is both powerful and efficient. Also, the algorithm that we give detects ambigous or/and incomplete definitions and can tell you why they are ambigous or/and incomplete. It applies too to definitions in presence of equations.