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.
Supported by DFG grant GI 274/5-3, DFG Research Training Group 1298 (AlgoSyn), G.I.F. grant 966-116.6, and the Danish Natural Science Research Council.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Apt, K.R.: From Logic Programming to Prolog. Prentice Hall (1997)
Arbab, B., Berry, D.M.: Operational and denotational semantics of Prolog. Journal of Logic Programming 4, 309–329 (1987)
Börger, E., Rosenzweig, D.: A mathematical definition of full Prolog. Science of Computer Programming 24, 249–286 (1995)
Cerrito, S.: A linear semantics for allowed logic programs. In: LICS 1990, pp. 219–227. IEEE Press (1990)
Cheng, M.H.M., Horspool, R.N., Levy, M.R., van Emden, M.H.: Compositional operational semantics for Prolog programs. New Generat. Comp. 10, 315–328 (1992)
de Bruin, A., de Vink, E.P.: Continuation Semantics for Prolog with Cut. In: Díaz, J., Yu, Y. (eds.) CAAP 1989 and TAPSOFT 1989. LNCS, vol. 351, pp. 178–192. Springer, Heidelberg (1989)
de Vink, E.P.: Comparative semantics for Prolog with cut. Science of Computer Programming 13, 237–264 (1990)
Debray, S.K., Mishra, P.: Denotational and operational semantics for Prolog. Journal of Logic Programming 5(1), 61–91 (1988)
Debray, S.K., Lin, N.-W.: Cost analysis of logic programs. ACM Transactions on Programming Languages and Systems 15, 826–875 (1993)
Deransart, P., Ferrand, G.: An operational formal definition of Prolog: a specification method and its application. New Generation Computing 10, 121–171 (1992)
Deransart, P., Ed-Dbali, A., Cervoni, L.: Prolog: The Standard. Springer (1996)
Hirokawa, N., Moser, G.: Automated Complexity Analysis Based on the Dependency Pair Method. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 364–379. Springer, Heidelberg (2008)
ISO/IEC 13211-1. Information technology - Programming languages - Prolog (1995)
Jeavons, J.: An alternative linear semantics for allowed logic programs. Annals of Pure and Applied Logic 84(1), 3–16 (1997)
Jones, N.D., Mycroft, A.: Stepwise development of operational and denotational semantics for Prolog. In: SLP 1984, pp. 281–288. IEEE Press (1984)
Kulaš, M., Beierle, C.: Defining standard prolog in rewriting logic. In: WRLA 2000. ENTCS, vol. 36 (2001)
Nicholson, T., Foo, N.: A denotational semantics for Prolog. ACM Transactions on Programming Languages and Systems 11, 650–665 (1989)
Noschinski, L., Emmes, F., Giesl, J.: A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS(LNAI), vol. 6803, pp. 422–438. Springer, Heidelberg (2011)
Schneider-Kamp, P., Giesl, J., Ströder, T., Serebrenik, A., Thiemann, R.: Automated termination analysis for logic programs with cut. In: ICLP 2010, Theory and Practice of Logic Programming, vol. 10(4-6), pp. 365–381 (2010)
Ströder, T., Schneider-Kamp, P., Giesl, J.: Dependency Triples for Improving Termination Analysis of Logic Programs with Cut. In: Alpuente, M. (ed.) LOPSTR 2010. LNCS, vol. 6564, pp. 184–199. Springer, Heidelberg (2011)
Ströder, T., Emmes, F., Schneider-Kamp, P., Giesl, J., Fuhs, C.: Fuhs. A linear operational semantics for termination and complexity analysis of ISO Prolog. Technical Report AIB-2011-08, RWTH Aachen (2011), http://aib.informatik.rwth-aachen.de/
Zankl, H., Korp, M.: Modular complexity analysis via relative complexity. In: RTA 2010. LIPIcs, vol. 6, pp. 385–400 (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
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 . In: Vidal, G. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2011. Lecture Notes in Computer Science, vol 7225. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32211-2_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-32211-2_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32210-5
Online ISBN: 978-3-642-32211-2
eBook Packages: Computer ScienceComputer Science (R0)