A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog

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

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

Resumé

We present a new operational semantics for Prolog which covers all constructs in the corresponding ISO standard (including “non-logical” concepts like cuts, meta-programming, “all solution” predicates, dynamic predicates, and exception handling). In contrast to the classical operational semantics for logic programming, our semantics is linear and not based on search trees. This has the advantage that it is particularly suitable for automated program analyses such as termination and complexity analysis. We prove that our new semantics is equivalent to the ISO Prolog semantics, i.e., it computes the same answer substitutions and the derivations in both semantics have essentially the same length.
OriginalsprogEngelsk
TitelProceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12)
ForlagAssociation for Computing Machinery
Publikationsdato2012
Sider237-252
ISBN (Trykt)Lecture Notes in Computer Science
DOI
StatusUdgivet - 2012
NavnLecture Notes in Computer Science
Vol/bind7225
ISSN0302-9743

Fingeraftryk

Semantics
Logic programming
Substitution reactions

Citer dette

Ströder, T., Emmes, F., Schneider-Kamp, P., Giesl, J., & Fuhs, C. (2012). A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog. I Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12) (s. 237-252). Association for Computing Machinery. Lecture Notes in Computer Science, Bind. 7225 https://doi.org/10.1007/978-3-642-32211-2_16
Ströder, Thomas ; Emmes, Fabian ; Schneider-Kamp, Peter ; Giesl, Jürgen ; Fuhs, Carsten. / A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog. Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12). Association for Computing Machinery, 2012. s. 237-252 (Lecture Notes in Computer Science, Bind 7225).
@inproceedings{de7fef3dcec24da38666f6899d3739c8,
title = "A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog",
abstract = "We present a new operational semantics for Prolog which covers all constructs in the corresponding ISO standard (including “non-logical” concepts like cuts, meta-programming, “all solution” predicates, dynamic predicates, and exception handling). In contrast to the classical operational semantics for logic programming, our semantics is linear and not based on search trees. This has the advantage that it is particularly suitable for automated program analyses such as termination and complexity analysis. We prove that our new semantics is equivalent to the ISO Prolog semantics, i.e., it computes the same answer substitutions and the derivations in both semantics have essentially the same length.",
author = "Thomas Str{\"o}der and Fabian Emmes and Peter Schneider-Kamp and J{\"u}rgen Giesl and Carsten Fuhs",
year = "2012",
doi = "10.1007/978-3-642-32211-2_16",
language = "English",
isbn = "Lecture Notes in Computer Science",
pages = "237--252",
booktitle = "Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12)",
publisher = "Association for Computing Machinery",
address = "United States",

}

Ströder, T, Emmes, F, Schneider-Kamp, P, Giesl, J & Fuhs, C 2012, A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog. i Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12). Association for Computing Machinery, Lecture Notes in Computer Science, bind 7225, s. 237-252. https://doi.org/10.1007/978-3-642-32211-2_16

A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog. / Ströder, Thomas; Emmes, Fabian; Schneider-Kamp, Peter; Giesl, Jürgen; Fuhs, Carsten.

Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12). Association for Computing Machinery, 2012. s. 237-252 (Lecture Notes in Computer Science, Bind 7225).

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

TY - GEN

T1 - A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog

AU - Ströder, Thomas

AU - Emmes, Fabian

AU - Schneider-Kamp, Peter

AU - Giesl, Jürgen

AU - Fuhs, Carsten

PY - 2012

Y1 - 2012

N2 - We present a new operational semantics for Prolog which covers all constructs in the corresponding ISO standard (including “non-logical” concepts like cuts, meta-programming, “all solution” predicates, dynamic predicates, and exception handling). In contrast to the classical operational semantics for logic programming, our semantics is linear and not based on search trees. This has the advantage that it is particularly suitable for automated program analyses such as termination and complexity analysis. We prove that our new semantics is equivalent to the ISO Prolog semantics, i.e., it computes the same answer substitutions and the derivations in both semantics have essentially the same length.

AB - We present a new operational semantics for Prolog which covers all constructs in the corresponding ISO standard (including “non-logical” concepts like cuts, meta-programming, “all solution” predicates, dynamic predicates, and exception handling). In contrast to the classical operational semantics for logic programming, our semantics is linear and not based on search trees. This has the advantage that it is particularly suitable for automated program analyses such as termination and complexity analysis. We prove that our new semantics is equivalent to the ISO Prolog semantics, i.e., it computes the same answer substitutions and the derivations in both semantics have essentially the same length.

U2 - 10.1007/978-3-642-32211-2_16

DO - 10.1007/978-3-642-32211-2_16

M3 - Article in proceedings

SN - Lecture Notes in Computer Science

SP - 237

EP - 252

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

PB - Association for Computing Machinery

ER -

Ströder T, Emmes F, Schneider-Kamp P, Giesl J, Fuhs C. A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog. I Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12). Association for Computing Machinery. 2012. s. 237-252. (Lecture Notes in Computer Science, Bind 7225). https://doi.org/10.1007/978-3-642-32211-2_16