Hostname: page-component-cd9895bd7-p9bg8 Total loading time: 0 Render date: 2024-12-23T11:02:00.740Z Has data issue: false hasContentIssue false
  • English
  • Français

Tabling, Rational Terms, and Coinduction Finally Together!

Published online by Cambridge University Press:  21 July 2014

THEOFRASTOS MANTADELIS ,
RICARDO ROCHA  and
PAULO MOURA
THEOFRASTOS MANTADELIS
Affiliation:
CRACS & INESC TEC, Faculty of Sciences, University of Porto, Rua do Campo Alegre, 1021/1055, 4169-007 Porto, Portugal (e-mail: [email protected], [email protected], [email protected])
RICARDO ROCHA
Affiliation:
CRACS & INESC TEC, Faculty of Sciences, University of Porto, Rua do Campo Alegre, 1021/1055, 4169-007 Porto, Portugal (e-mail: [email protected], [email protected], [email protected])
PAULO MOURA
Affiliation:
CRACS & INESC TEC, Faculty of Sciences, University of Porto, Rua do Campo Alegre, 1021/1055, 4169-007 Porto, Portugal (e-mail: [email protected], [email protected], [email protected])
Get access Rights & Permissions [Opens in a new window]

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 improves computational 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 then use this extension to implement a tabling based approach to coinduction. We compare our approach with current coinductive transformations and describe the implementation. In addition, we present an algorithm that ensures a canonical representation for rational terms.

Keywords

TablingRational TermsCoinductionImplementation
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 14 , Special Issue 4-5: 30th International Conference on Logic Programming , July 2014 , pp. 429 - 443
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Ancona, D. 2013. Regular Corecursion in Prolog. Computer Languages, Systems & Structures 39, 4, 142–162. Special issue on the Programming Languages track at the 27th ACM Symposium on Applied Computing.CrossRefGoogle Scholar
Bagnara, R., Gori, R., Hill, P. M., and Zaffanella, E. 2001. Finite-Tree Analysis for Constraint Logic-Based Languages: The Complete Unabridged Version.Google Scholar
Chen, W. and Warren, D. S. 1996. Tabled Evaluation with Delaying for General Logic Programs. Journal of the ACM 43, 1, 20–74.CrossRefGoogle Scholar
Colmerauer, A. 1982. Prolog and Infinite Trees. In Logic Programming, Clark, K. L. and Tärnlund, S.-A., Eds. Academic Press, 231–251.Google Scholar
Giannesini, F. and Cohen, J. 1984. Parser generation and grammar manipulation using prolog's infinite trees. The Journal of Logic Programming 1, 3, 253–265.Google Scholar
Gordon, A. D. 1994. A Tutorial on Co-induction and Functional Programming. In Glasgow Functional Programming Workshop. Springer-Verlag, 78–95.Google Scholar
Gupta, G., Bansal, A., Min, R., Simon, L., and Mallya, A. 2007. Coinductive logic programming and its applications. In Logic Programming. LNCS, vol. 4670. Springer-Verlag, 27–44.Google Scholar
Hopcroft, J. E. and Karp, R. M. 1971. A linear algorithm for testing equivalence of finite automata. Tech. rep., Cornell University.Google Scholar
Jaffar, J. and Stuckey, P. J. 1986. Semantics of Infinite Tree Logic Programming. Theoretical Computer Science 46, 0, 141–158.CrossRefGoogle Scholar
Meister, M. and Frühwirth, T. 2006. Complexity of the CHR rational tree equation solver. In Constraint Handling Rules. Vol. 452. 77–92.Google Scholar
Moura, P. 2013. A Portable and Efficient Implementation of Coinductive Logic Programming. In International Symposium on Practical Aspects of Declarative Languages. LNCS, vol. 7752. Springer-Verlag, 77–92.Google Scholar
Raimundo, J. and Rocha, R. 2010. Compact Lists for Tabled Evaluation. In International Symposium on Practical Aspects of Declarative Languages. Number 5937 in LNCS. Springer-Verlag, 249–263.Google Scholar
Ramakrishnan, I. V., Rao, P., Sagonas, K., Swift, T., and Warren, D. S. 1999. Efficient Access Mechanisms for Tabled Logic Programs. Journal of Logic Programming 38, 1, 31–54.Google Scholar
Santos Costa, V., Rocha, R., and Damas, L. 2012. The YAP Prolog System. Journal of Theory and Practice of Logic Programming 12, 1&2, 5–34.Google Scholar
Schrijvers, T. and Oliveira, B. C. 2012. Rational Term Equality, Functionally. In Implementation and Application of Functional Languages, 24th Symposium, Pre-Proceedings, R. Hinze, Ed.Google Scholar
Simon, L., Bansal, A., Mallya, A., and Gupta, G. 2007. Co-Logic Programming: Extending Logic Programming with Coinduction. In Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 4596. Springer-Verlag, 472–483.CrossRefGoogle Scholar
Stickel, M. E. 1988. A prolog technology theorem prover: Implementation by an extended prolog compiler. Journal of Automated Reasoning 4, 4, 353–380.Google Scholar
Swift, T. and Warren, D. S. 2012. XSB: Extending Prolog with Tabled Logic Programming. Theory and Practice of Logic Programming 12, 1 & 2, 157–187.CrossRefGoogle Scholar
Wielemaker, J., Schrijvers, T., Triska, M., and Lager, T. 2012. SWI-Prolog. Journal of Theory and Practice of Logic Programming 12, 1&2, 67–96.Google Scholar
Supplementary material: PDF

MANTADELIS et al.

Tabling, Rational Terms, and Coinduction Finally Together!

Download MANTADELIS et al.(PDF)
PDF 229.6 KB