Proving Operational Termination of Declarative Programs in General Logics

A declarative program P is a *theory* in a given computational logic L, so that *computation* with such a program is efficiently implemented as *deduction* in L. That is why *inference systems* are crucial: they both (i) *define* the logical semantics of a language in its underlying logic L, and (ii) *specify* the *execution* of programs in a correct implementation. The notion of *operational termination* (OT) of a declarative program P identifies termination with *absence of infinite inference* with P. We further develop the OT notion for declarative programs in general logics with schematic inference systems and characterize OT in terms of *chains of proof jumps*. We also generalize the dependency pair framework to an arbitrary schematic logic L, so that methods for proving declarative programs OT become available for a very wide range of declarative languages. We illustrate the usefulness of the general OT methods we propose by three case studies in three logics: that of Conditional Term Rewriting Systems, the Typed Lambda Calculus, and Membership Rewriting Logic. In particular, we show how various programs that could not be proved terminating with existing methods can be proved OT with the methods presented here.Partially supported by NSF grant CNS 13-19109. Salvador Lucas’ research was developed during a sabbatical year at the UIUC and was also supported by the EU (FEDER), Spanish MINECO projects TIN2010-21062-C02-02 and TIN 2013-45732-C4-1-P, and GV grant BEST/2014/026 and project PROMETEO/2011/052.Lucas Alba, S.; Meseguer, J. (2014). Proving Operational Termination of Declarative Programs in General Logics. ACM. https://doi.org/10.1145/2643135.2643152P. Aczel. Schematic Consequence. In D. Gabbay, editor, What is a Logical System, pages 261--272, Oxford University Press, 1994.B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, R. Gutiérrez, S. Lucas, P. Schneider-Kamp, and R. Thiemann. Improving Context-Sensitive Dependency Pairs. In Proc. of LPAR'08, LNCS 5330:636--651, 2008.B. Alarcón, S. Lucas, and J. Meseguer. A Dependency Pair Framework for A∨C-Termination. In Proc. of WRLA'10, LNCS 6381:35--51, 2010.H.P. Barendregt, W. Dekkers, and R. Statman. Lambda Calculus with Types. Cambridge University Press, 2013.M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott. All About Maude -- A High-Performance Logical Framework, LNCS volume 4350, 2007.M. Codish and C. Taboch. A semantic basis for the termination analysis of logic programs. Journal of Logic Programming 41:103--123, 1999.N. Dershowitz, N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. A General Framework for Automatic Termination of Logic Programs. Applicable Algebra in Engineering, Communication and Computing, 12:117--156, 2001.N. Dershowitz and Z. Manna. Proving Termination with Multiset Orderings. Communications of the ACM 22(8):465--476, 1979.F. Durán, S. Lucas, J. Meseguer, C. Marché, and X. Urbain. Proving Termination of Membership Equational Programs. In Proc. of PEPM'04, pages 147--158, ACM Press, New York, 2004.F. Durán, S. Lucas, C. Marché, J. Meseguer, X. Urbain, Proving Operational Termination of Membership Equational Programs, Higher-Order and Symbolic Computation 21(1-2):59--88, 2008.F. Durán, S. Lucas, J. Meseguer. Methods for Proving Termination of Rewriting-based Programming Languages by Transformation. Electronic Notes in Theoretical Computer Science, 248:93--113, 2009.F. Durán, S. Lucas, and J. Meseguer. MTT: The Maude Termination Tool (System Description). Proc. of IJCAR'08. LNAI 5195:313--319, 2008.S. Falke and D. Kapur. Dependency Pairs for Rewriting with Built-in Numbers and Semantic Data Structures. In Proc. of RTA'08, LNCS 5117:94--109, 2008.J. Giesl and D. Kapur. Dependency Pairs for Equational Rewriting. Proc. of RTA'01, LNCS 2051:93--108, 2001.J. Giesl, R. Thiemann, and P. Schneider-Kamp. The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. In Proc. of LPAR'04, LNAI 3452:301--331, 2004.J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Mechanizing and Improving Dependency Pairs. Journal of Automatic Reasoning, 37(3):155--203, 2006.R. Gutiérrez and S. Lucas. Proving Termination in the Context-Sensitive Depedency Pairs Framework. In Proc of WRLA'10 LNCS 6381:19--35, 2010.S. Lucas. Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming, 1998(1):1--61, January 1998.S. Lucas. Context-sensitive rewriting strategies. Information and Computation, 178(1):294--343, 2002.S. Lucas and J. Meseguer. 2D Dependency Pairs for Proving Operational Termination of CTRSs. In Proc. of WRLA'14, LNCS vol. 8663, to appear, 2014.S. Lucas and J. Meseguer. Order-Sorted Dependency Pairs. In Proc. of PPDP'08, pages 108--119, ACM Press, 2008.S. Lucas, C. Marché, and J. Meseguer. Operational termination of conditional term rewriting systems. Information Processing Letters, 95:446--453, 2005.J. Meseguer. General Logics. In H.-D. Ebbinghaus et al., editors, Logic Colloquium'87, pages 275--329, North-Holland, 1989.J. Meseguer. Membership algebra as a logical framework for equational specification. In Proc. of WADT'97, LNCS 1376:18--61, 1998.M. Nakamura, K. Ogata, and K. Futatsugi. On Proving Operational Termination Incrementally with Modular Conditional Dependency Pairs. International Journal of Computer Science, 40:2, 2013.M.T. Nguyen, J. Giesl, P. Schneider-Kamp, and D. De Schreye. Termination Analysis of Logic Programs Based on Dependency Graphs. In Proc. of LOPSTR 2007, LNCS 4915:8--22, 2007.E. Ohlebusch. Advanced Topics in Term Rewriting. Springer-Verlag, 2002.F. Schernhammer and B. Gramlich. Characterizing and proving operational termination of deterministic conditional term rewriting systems. Journal of Logic and Algebraic Programming 79:659--688, 2010.D. de Scheye and S. Decorte. Termination of Logic Programs: The Never-Ending Story. Journal of Logic Programming, 19:199--260, 1994.P. Schneider-Kamp, J. Giesl, and M.T. Nguyen. The Dependency Triple Framework for Termination of Logic Programs. In Proc. of LOPSTR 2009, LNCS 6037:37--51, 2009