Stop Losing Sleep Over Incomplete Data Type Specifications

Abstract

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.