Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1145/2370776.2370778acmotherconferencesArticle/Chapter ViewAbstractPublication PagesppdpConference Proceedingsconference-collections
invited-talk

Symbolic evaluation graphs and term rewriting: a general methodology for analyzing logic programs

Published: 19 September 2012 Publication History

Abstract

There exist many powerful techniques to analyze termination and complexity of term rewrite systems (TRSs). Our goal is to use these techniques for the analysis of other programming languages as well. For instance, approaches to prove termination of definite logic programs by a transformation to TRSs have been studied for decades. However, a challenge is to handle languages with more complex evaluation strategies (such as Prolog, where predicates like the cut influence the control flow). In this paper, we present a general methodology for the analysis of such programs. Here, the logic program is first transformed into a symbolic evaluation graph which represents all possible evaluations in a finite way. Afterwards, different analyses can be performed on these graphs. In particular, one can generate TRSs from such graphs and apply existing tools for termination or complexity analysis of TRSs to infer information on the termination or complexity of the original logic program.

References

[1]
http://aprove.informatik.rwth-aachen.de/eval/ LPGraphs/.
[2]
K. R. Apt. From Logic Programming to Prolog. Prentice Hall, 1997.
[3]
M. Avanzini, G. Moser, and A. Schnabl. Automated implicit computational complexity analysis. In Proc. IJCAR '08, LNAI 5195, pages 132--138, 2008.
[4]
M. Avanzini and G. Moser. Dependency pairs and polynomial path orders. In Proc. RTA '09, LNCS 5595, pages 48--62, 2009.
[5]
M. Avanzini, N. Eguchi, and G. Moser. A path order for rewrite systems that compute exponential time functions. In Proc. RTA '11, LIPIcs 10, pages 123--138, 2011.
[6]
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
[7]
M. Brockschmidt, C. Otto, and J. Giesl. Modular termination proofs of recursive Java Bytecode programs by term rewriting. In Proc. RTA '11, LIPIcs 10, pages 155--170, 2011.
[8]
M. Brockschmidt, T. Ströder, C. Otto, and J. Giesl. Automated detection of non-termination and NullPointerExceptions for Java Bytecode. In Proc. FoVeOOS '11, LNCS 7421, pages 123--141, 2012.
[9]
M. Brockschmidt, R. Musiol, C. Otto, and J. Giesl. Automated termination proofs for Java programs with cyclic data. In Proc. CAV '12, LNCS 7358, pages 105--122, 2012.
[10]
S. K. Debray, N.-W. Lin, and M. V. Hermenegildo. Task granularity analysis in logic programs. In Proc. PLDI '90, pages 174--188. ACM Press, 1990. 15 {1} also contains a version of the paper with all proofs {18}.
[11]
S. K. Debray and N.-W. Lin. Cost analysis of logic programs. ACM Transactions on Programming Languages and Systems, 15:826--875, 1993.
[12]
S. K. Debray, P. López-García, M. V. Hermenegildo, and N.-W. Lin. Lower bound cost estimation for logic programs. In Proc. ILPS '97, pages 291--305. MIT Press, 1997.
[13]
N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1--2), pages 69--116, 1987.
[14]
C. Fuhs, J. Giesl, M. Plücker, P. Schneider-Kamp, and S. Falke. Proving termination of integer term rewriting. In Proc. RTA '09, LNCS 5595, pages 32--47, 2009.
[15]
J. Giesl, P. Schneider-Kamp, and R. Thiemann. AProVE 1.2: Automatic termination proofs in the dependency pair framework. In Proc. IJCAR '06, LNAI 4130, pages 281--286, 2006.
[16]
J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Mechanizing and improving dependency pairs. Journal of Automated Reasoning, 37(3), pages 155--203, 2006.
[17]
J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, and R. Thiemann. Automated termination proofs for Haskell by term rewriting. ACM Transactions on Programming Languages and Systems, 33(2), 2011.
[18]
J. Giesl, T. Ströder, P. Schneider-Kamp, F. Emmes, and C. Fuhs. Symbolic evaluation graphs and term rewriting -- a general methodology for analyzing logic programs. Technical Report AIB 2012-12, RWTH Aachen University, 2012. Available from http://aib.informatik.rwth-aachen.de and {1}.
[19]
M. V. Hermenegildo, G. Puebla, F. Bueno, and P. López-García. Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor). Science of Computer Programming, 58(1--2):115--140, 2005.
[20]
M. V. Hermenegildo, F. Bueno, M. Carro, P. López-García, E. Mera, J. F. Morales, and G. Puebla. An overview of Ciao and its design philosophy. Theory and Practice of Logic Programming, 12:219--252, 2012.
[21]
N. Hirokawa and G. Moser. Automated complexity analysis based on the dependency pair method. In Proc. IJCAR '08, LNAI 5195, pages 364--379, 2008.
[22]
J. M. Howe and A. King. Efficient groundness analysis in Prolog. Theory and Practice of Logic Programming, 3(1):95--124, 2003.
[23]
ISO/IEC 13211-1. Information technology - Programming languages - Prolog. 1995.
[24]
A. King, K. Shen, and F. Benoy. Lower-bound time-complexity analysis of logic programs. In Proc. ILPS '97, pages 261--285. MIT Press, 1997.
[25]
A. King, L. Lu, and S. Genaim. Detecting determinacy in Prolog programs. In Proc. ICLP '06, LNCS 4079, pages 132--147, 2006.
[26]
J. Kriener and A. King. RedAlert: Determinacy inference for Prolog. In Proc. ICLP '11, Theory and Practice of Logic Programming, 11(4--5):537--553, 2011.
[27]
J. Kriener and A. King. Mutual exclusion by interpolation. In Proc. FLOPS '12, LNCS 7294, pages 182--196, 2012.
[28]
P. López-García, F. Bueno, and M. V. Hermenegildo. Automatic inference of determinacy and mutual exclusion for logic programs using mode and type analyses. New Generation Computing, 28(2):177--206, 2010.
[29]
T. Mogensen. A semantics-based determinacy analysis for Prolog with cut. In Proc. Ershov Memorial Conference '96, LNCS 1181, pages 374--385, 1996.
[30]
J. A. Navas, E. Mera, P. López-García, and M. V. Hermenegildo. User-definable resource bounds analysis for logic programs. In Proc. ICLP '07, LNCS 4670, pages 348--363, 2007.
[31]
M. T. Nguyen, J. Giesl, and P. Schneider-Kamp. Termination analysis of logic programs based on dependency graphs. In Proc. LOPSTR '07, LNCS 4915, pages 8--22, 2008.
[32]
L. Noschinski, F. Emmes, and J. Giesl. The dependency pair framework for automated complexity analysis of term rewrite systems. In Proc. CADE '11, LNAI 6803, pages 422--438, 2011.
[33]
E. Ohlebusch. Termination of logic programs: Transformational methods revisited. Applicable Algebra in Engineering, Communication and Computing, 12(1--2):73--116, 2001.
[34]
D. Sahlin. Determinacy analysis for full Prolog. In Proc. PEPM '91, pages 23--30. ACM Press, 1991.
[35]
P. Schneider-Kamp, J. Giesl, A. Serebrenik, and R. Thiemann. Automated termination proofs for logic programs by term rewriting. ACM Transactions on Computational Logic, 11(1), 2009.
[36]
P. Schneider-Kamp, J. Giesl, and M. T. Nguyen. The dependency triple framework for termination of logic programs. In Proc. LOPSTR '09, LNCS 6037, pages 37--51, 2010.
[37]
P. Schneider-Kamp, J. Giesl, T. Ströder, A. Serebrenik, and R. Thiemann. Automated termination analysis for logic programs with cut. In Proc. ICLP '10, Theory and Practice of Logic Programming, 10(4--6):365--381, 2010.
[38]
M. H. Sørensen and R. Glück. An algorithm of generalization in positive supercompilation. In Proc. ILPS '95, pages 465--479. MIT Press, 1995.
[39]
T. Ströder. Towards termination analysis of real Prolog programs. Diploma Thesis, RWTH Aachen University, 2010. Available from {1}.
[40]
T. Ströder, P. Schneider-Kamp, and J. Giesl. Dependency triples for improving termination analysis of logic programs with cut. In Proc. LOPSTR '10, LNCS 6564, pages 184--199, 2011.
[41]
T. Ströder, F. Emmes, P. Schneider-Kamp, J. Giesl, and C. Fuhs. A linear operational semantics for termination and complexity analysis of ISO Prolog. In Proc. LOPSTR '11, LNCS, 2012. To appear. Available from {1}.
[42]
H. Zankl and M. Korp. Modular complexity analysis via relative complexity. In Proc. RTA '10, LIPIcs 6, pages 385--400, 2010.
[43]
H. Zantema. Termination. In Terese, editor, Term Rewriting Systems, pages 181--259. Cambridge University Press, 2003.

Cited By

View all
  • (2023)Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency PairsAutomated Deduction – CADE 2910.1007/978-3-031-38499-8_20(344-364)Online publication date: 2-Sep-2023
  • (2022)Scheduling Complexity of Interleaving SearchFunctional and Logic Programming10.1007/978-3-030-99461-7_9(152-170)Online publication date: 3-May-2022
  • (2021)Cost Analysis of Smart Contracts Via Parametric Resource AnalysisStatic Analysis10.1007/978-3-030-65474-0_2(7-31)Online publication date: 13-Jan-2021
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences
PPDP '12: Proceedings of the 14th symposium on Principles and practice of declarative programming
September 2012
226 pages
ISBN:9781450315227
DOI:10.1145/2370776
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

  • Kuleuven Belgium: Kuleuven Belgium

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 September 2012

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. complexity
  2. determinacy
  3. logic programs
  4. prolog
  5. term rewriting
  6. termination

Qualifiers

  • Invited-talk

Conference

PPDP'12
Sponsor:
  • Kuleuven Belgium

Acceptance Rates

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)1
  • Downloads (Last 6 weeks)1
Reflects downloads up to 16 Nov 2024

Other Metrics

Citations

Cited By

View all
  • (2023)Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency PairsAutomated Deduction – CADE 2910.1007/978-3-031-38499-8_20(344-364)Online publication date: 2-Sep-2023
  • (2022)Scheduling Complexity of Interleaving SearchFunctional and Logic Programming10.1007/978-3-030-99461-7_9(152-170)Online publication date: 3-May-2022
  • (2021)Cost Analysis of Smart Contracts Via Parametric Resource AnalysisStatic Analysis10.1007/978-3-030-65474-0_2(7-31)Online publication date: 13-Jan-2021
  • (2019)Transforming Derivational Complexity of Term Rewriting to Runtime ComplexityFrontiers of Combining Systems10.1007/978-3-030-29007-8_20(348-364)Online publication date: 14-Aug-2019
  • (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
  • (2017)Analyzing Program Termination and Complexity Automatically with AProVEJournal of Automated Reasoning10.1007/s10817-016-9388-y58:1(3-31)Online publication date: 1-Jan-2017
  • (2016)Analyzing Runtime and Size Complexity of Integer ProgramsACM Transactions on Programming Languages and Systems10.1145/286657538:4(1-50)Online publication date: 2-Aug-2016
  • (2016)A Transformational Approach to Parametric Accumulated-Cost Static ProfilingFunctional and Logic Programming10.1007/978-3-319-29604-3_11(163-180)Online publication date: 21-Feb-2016
  • (2015)Concolic Execution and Test Case Generation in PrologLogic-Based Program Synthesis and Transformation10.1007/978-3-319-17822-6_10(167-181)Online publication date: 23-Apr-2015
  • (2014)Alternating Runtime and Size Complexity Analysis of Integer ProgramsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-642-54862-8_10(140-155)Online publication date: 2014
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media