Tabling, Rational Terms, and Coinduction Finally Together!

ABSTRACT. Tabling is a commonly used technique in logic programming for avoiding cyclic behavior of logic programs and enabling more declarative program definitions. Furthermore, tabling often results in improved computation performance. Rational term are terms with one or more infinite sub-terms but with a finite representation. Rational terms can be generated in Prolog by omitting the occurs check when unifying two terms. Applications of rational terms include definite clause grammars, constraint handling systems, and coinduction. In this paper we report our extension of Yap's Prolog tabling mechanism to support rational terms. We describe the internal representation of rational terms within the table space and prove its correctness. We use this extension to implement a novel approach to coinduction with the use of tabling. We present the similarities with current coinductive transformations and describe the implementation. In addition, we address some limitations of rational terms support by Prolog compilers and describe an approach to ensure a canonical representation for rational terms.