tutorial

Proving Operational Termination of Declarative Programs in General Logics

Authors:

Salvador Lucas,

José MeseguerAuthors Info & Claims

PPDP '14: Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming

Pages 111 - 122

https://doi.org/10.1145/2643135.2643152

Published: 08 September 2014 Publication History

Abstract

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 for Term Rewriting Systems 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 λ-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.

References

[1]

P. Aczel. Schematic Consequence. In D. Gabbay, editor, What is a Logical System, pages 261--272, Oxford University Press, 1994.

Digital Library

[2]

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.

Digital Library

[3]

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.

Digital Library

[4]

H.P. Barendregt, W. Dekkers, and R. Statman. Lambda Calculus with Types. Cambridge University Press, 2013.

Digital Library

[5]

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.

Digital Library

[6]

M. Codish and C. Taboch. A semantic basis for the termination analysis of logic programs. Journal of Logic Programming 41:103--123, 1999.

[7]

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.

[8]

N. Dershowitz and Z. Manna. Proving Termination with Multiset Orderings. Communications of the ACM 22(8):465--476, 1979.

Digital Library

[9]

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.

Digital Library

[10]

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.

Digital Library

[11]

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.

Digital Library

[12]

F. Durán, S. Lucas, and J. Meseguer. MTT: The Maude Termination Tool (System Description). Proc. of IJCAR'08. LNAI 5195:313--319, 2008.

Digital Library

[13]

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.

Digital Library

[14]

J. Giesl and D. Kapur. Dependency Pairs for Equational Rewriting. Proc. of RTA'01, LNCS 2051:93--108, 2001.

Digital Library

[15]

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.

[16]

J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Mechanizing and Improving Dependency Pairs. Journal of Automatic Reasoning, 37(3):155--203, 2006.

Digital Library

[17]

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.

[18]

S. Lucas. Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming, 1998(1):1--61, January 1998.

[19]

S. Lucas. Context-sensitive rewriting strategies. Information and Computation, 178(1):294--343, 2002.

Digital Library

[20]

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.

[21]

S. Lucas and J. Meseguer. Order-Sorted Dependency Pairs. In Proc. of PPDP'08, pages 108--119, ACM Press, 2008.

Digital Library

[22]

S. Lucas, C. Marché, and J. Meseguer. Operational termination of conditional term rewriting systems. Information Processing Letters, 95:446--453, 2005.

Digital Library

[23]

J. Meseguer. General Logics. In H.-D. Ebbinghaus et al., editors, Logic Colloquium'87, pages 275--329, North-Holland, 1989.

[24]

J. Meseguer. Membership algebra as a logical framework for equational specification. In Proc. of WADT'97, LNCS 1376:18--61, 1998.

Digital Library

[25]

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.

[26]

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.

[27]

E. Ohlebusch. Advanced Topics in Term Rewriting. Springer-Verlag, 2002.

Digital Library

[28]

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.

[29]

D. de Scheye and S. Decorte. Termination of Logic Programs: The Never-Ending Story. Journal of Logic Programming, 19:199--260, 1994.

[30]

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.

Digital Library

Cited By

Gutiérrez RLucas S(2020)Automatically Proving and Disproving Feasibility ConditionsAutomated Reasoning10.1007/978-3-030-51054-1_27(416-435)Online publication date: 24-Jun-2020
https://doi.org/10.1007/978-3-030-51054-1_27
Lucas S(2019)Using Well-Founded Relations for Proving Operational TerminationJournal of Automated Reasoning10.1007/s10817-019-09514-2Online publication date: 11-Feb-2019
https://doi.org/10.1007/s10817-019-09514-2
Lucas SGutiérrez R(2018)Automatic Synthesis of Logical Models for Order-Sorted First-Order TheoriesJournal of Automated Reasoning10.1007/s10817-017-9419-360:4(465-501)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10817-017-9419-3
Show More Cited By

Recommendations

Operational Termination of Membership Equational Programs: the Order-Sorted Way

Our main goal is automating termination proofs for programs in rewriting-based languages with features such as: (i) expressive type structures, (ii) conditional rules, (iii) matching modulo axioms, and (iv) context-sensitive rewriting. Specifically, we ...
Proving operational termination of membership equational programs

Reasoning about the termination of equational programs in sophisticated equational languages such as Elan , Maude , OBJ , CafeOBJ , Haskell , and so on, requires support for advanced features such as evaluation strategies, rewriting modulo, use of ...
A methodology for proving termination of general logic programs

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PPDP '14: Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming

September 2014

288 pages

ISBN:9781450329477

DOI:10.1145/2643135

General Chairs:
Olaf Chitil
University of Kent, UK
,
Andy King
University of Kent, UK
,
Program Chair:
Olivier Danvy
Aarhus University, Denmark

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 September 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Tutorial
Research
Refereed limited

Conference

PPDP '14

Sponsor:

SIGPLAN

PPDP '14: 16th International Symposium on Principles and Practice of Declarative Programming

September 8 - 10, 2014

Canterbury, United Kingdom

Acceptance Rates

PPDP '14 Paper Acceptance Rate 22 of 43 submissions, 51%;

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
29
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Gutiérrez RLucas S(2020)Automatically Proving and Disproving Feasibility ConditionsAutomated Reasoning10.1007/978-3-030-51054-1_27(416-435)Online publication date: 24-Jun-2020
https://doi.org/10.1007/978-3-030-51054-1_27
Lucas S(2019)Using Well-Founded Relations for Proving Operational TerminationJournal of Automated Reasoning10.1007/s10817-019-09514-2Online publication date: 11-Feb-2019
https://doi.org/10.1007/s10817-019-09514-2
Lucas SGutiérrez R(2018)Automatic Synthesis of Logical Models for Order-Sorted First-Order TheoriesJournal of Automated Reasoning10.1007/s10817-017-9419-360:4(465-501)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10817-017-9419-3
Lucas S(2016)Use of Logical Models for Proving Operational Termination in General LogicsRewriting Logic and Its Applications10.1007/978-3-319-44802-2_2(26-46)Online publication date: 18-Aug-2016
https://doi.org/10.1007/978-3-319-44802-2_2
Lucas S(2015)Synthesis of models for order-sorted first-order theories using linear algebra and constraint solvingElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.200.3200(32-47)Online publication date: 19-Dec-2015
https://doi.org/10.4204/EPTCS.200.3
Lucas SMeseguer J(2014)Models for Logics and Conditional Constraints in Automated Proofs of TerminationArtificial Intelligence and Symbolic Computation10.1007/978-3-319-13770-4_3(9-20)Online publication date: 2014
https://doi.org/10.1007/978-3-319-13770-4_3

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents