An Emptiness Algorithm for Regular Types with Set Operators

. An algorithm to decide the emptiness of a regular type expression with set operators given a set of parameterised type definitions is presented. The algorithm can also be used to decide the equivalence of two regular type expressions and the inclusion of one regular type expression in another. The algorithm strictly generalises previous work in that tuple distributivity is not assumed and set operators are permitted in type expressions. Keywords: type, emptiness, prescriptive type 1 Introduction Types play an important role in programming languages [6]. They make programs easier to understand and help detect errors. Types have been introduced into logic programming in the forms of type checking and inference [5,9,12,26,32] or type analysis [25,33,17,19,13,22,7,23] or typed languages [16,21,28,31]. Recent logic programming systems allow the programmer to declare types for predicates and type errors are then detected either at compile time or at run time. The reader is referred to [2..