Tabling, Rational Terms, and Coinduction Finally Together!

Theofrastos Mantadelis, Ricardo Rocha and Paulo Moura

July 2014

---

Abstract

Tabling is a commonly used technique in logic programming for avoiding cyclic behavior of logic programs and enabl ing more declarative program definitions. Furthermore, tabling often improves computational performance. Rational term are terms with one or more infinite sub-terms but with a finite representation. Rational terms can be generat ed 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 th e internal representation of rational terms within the table space and prove its correctness. We then use this ext ension to implement a tabling based approach to coinduction. We compare our approach with current coinductive tran sformations and describe the implementation. In addition, we present an algorithm that ensures a canonical represe ntation for rational terms.

Bibtex

@Article{mantadelis-iclp14,
  author =    {T. Mantadelis and R. Rocha and P. Moura},
  title =     {{Tabling, Rational Terms, and Coinduction Finally Together!}},
  journal =   {Journal of Theory and Practice of Logic Programming, 
               30th International Conference on Logic Programming (ICLP 2014), Special Issue},
  pages =     {429--443},
  volume =    {14},
  number =    {4 \& 5},
  month =     {July},
  year =      {2014},
}

Download Paper

PDF file
Cambridge University Press
Computing Research Repository (CoRR)