Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs

Jürgen Giesl, Thomas Ströder, Peter Schneider-Kamp, Fabian Emmes, Carsten Fuhs

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

Resumé

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.
OriginalsprogEngelsk
TitelProceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12)
Antal sider12
ForlagAssociation for Computing Machinery
Publikationsdato2012
ISBN (Trykt)978-1-4503-1522-7
DOI
StatusUdgivet - 2012
Begivenhed14th sSmposium on Principles and Practice of Declarative Programming - Leuven, Belgien
Varighed: 19. sep. 201221. sep. 2012

Konference

Konference14th sSmposium on Principles and Practice of Declarative Programming
LandBelgien
ByLeuven
Periode19/09/201221/09/2012

Fingeraftryk

Flow control
Computer programming languages

Citer dette

Giesl, J., Ströder, T., Schneider-Kamp, P., Emmes, F., & Fuhs, C. (2012). Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs. I Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12) Association for Computing Machinery. https://doi.org/10.1145/2370776.2370778
Giesl, Jürgen ; Ströder, Thomas ; Schneider-Kamp, Peter ; Emmes, Fabian ; Fuhs, Carsten. / Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs. Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12). Association for Computing Machinery, 2012.
@inproceedings{5c7ff26f5f5b48c19b575fef14337c86,
title = "Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs",
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.",
author = "J{\"u}rgen Giesl and Thomas Str{\"o}der and Peter Schneider-Kamp and Fabian Emmes and Carsten Fuhs",
year = "2012",
doi = "10.1145/2370776.2370778",
language = "English",
isbn = "978-1-4503-1522-7",
booktitle = "Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12)",
publisher = "Association for Computing Machinery",
address = "United States",

}

Giesl, J, Ströder, T, Schneider-Kamp, P, Emmes, F & Fuhs, C 2012, Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs. i Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12). Association for Computing Machinery, 14th sSmposium on Principles and Practice of Declarative Programming, Leuven, Belgien, 19/09/2012. https://doi.org/10.1145/2370776.2370778

Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs. / Giesl, Jürgen; Ströder, Thomas; Schneider-Kamp, Peter; Emmes, Fabian; Fuhs, Carsten.

Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12). Association for Computing Machinery, 2012.

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

TY - GEN

T1 - Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs

AU - Giesl, Jürgen

AU - Ströder, Thomas

AU - Schneider-Kamp, Peter

AU - Emmes, Fabian

AU - Fuhs, Carsten

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

U2 - 10.1145/2370776.2370778

DO - 10.1145/2370776.2370778

M3 - Article in proceedings

SN - 978-1-4503-1522-7

BT - Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12)

PB - Association for Computing Machinery

ER -

Giesl J, Ströder T, Schneider-Kamp P, Emmes F, Fuhs C. Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs. I Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12). Association for Computing Machinery. 2012 https://doi.org/10.1145/2370776.2370778