Mode checking using constrained regular trees

Lee Naish

In a previous paper we presented a high level polymorphic mode system for logic programs. In this paper we present an algorithm which checks if a program is well moded, given that is it well-typed in the sense of Mycroft and O'Keefe. A program is well-moded if the set of ground atoms defined by mode declarations is a superset of the success set. The novelty of the algorithm is the expressiveness of the mode declarations. Constrained regular trees are used to define sets of terms and atoms. These are based on polymorphic types but allow set and multiset constraints over type variables. The expressiveness of this domain makes it very promising for many program analysis applications. Complexity is also (exponentially) better than other proposed domains for certain analysis tasks.

Keywords: logic programming, modes, types, constrained regular trees, aliasing, linearity, set constraints, multisets