Abstract
Bottom-up logic programming can be used to declaratively specify many algorithms in a succinct and natural way, and McAllester and Ganzinger have shown that it is possible to define a cost semantics that enables reasoning about the running time of algorithms written as inference rules. Previous work with the programming language Lollimon demonstrates the expressive power of logic programming with linear logic in describing algorithms that have imperative elements or that must repeatedly make mutually exclusive choices. In this paper, we identify a bottom-up logic programming language based on linear logic that is amenable to efficient execution and describe a novel cost semantics that can be used for complexity analysis of algorithms expressed in linear logic.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
McAllester, D.A.: On the complexity analysis of static analyses. J. ACM 49(4), 512–537 (2002)
Nielson, F., Nielson, H.R., Seidl, H.: Automatic complexity analysis. In: Le Métayer, D. (ed.) ESOP 2002 and ETAPS 2002. LNCS, vol. 2305, pp. 243–261. Springer, Heidelberg (2002)
Liu, Y.A., Stoller, S.D.: From Datalog rules to efficient programs with time and space guarantees. In: PPDP 2003: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, pp. 172–183. ACM, New York (2003)
Ganzinger, H., McAllester, D.A.: A new meta-complexity theorem for bottom-up logic programs. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 514–528. Springer, Heidelberg (2001)
Ganzinger, H., McAllester, D.A.: Logical algorithms. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 209–223. Springer, Heidelberg (2002)
Greco, S., Zaniolo, C.: Greedy algorithms in Datalog. Theory Pract. Log. Program. 1(4), 381–407 (2001)
Chang, B.Y.E., Chaudhuri, K., Pfenning, F.: A judgmental analysis of linear logic. Technical Report CMU-CS-03-131, Carnegie Mellon University (April 2003)
Nomikos, C., Rondogiannis, P., Gergatsoulis, M.: Temporal stratification tests for linear and branching-time deductive databases. Theor. Comput. Sci. 342(2-3), 382–415 (2005)
Arni, F., Ong, K., Tsur, S., Wang, H., Zaniolo, C.: The Deductive Database System LDL++. Theory Pract. Log. Program. 3(1), 61–94 (2003)
Pfenning, F.: Linear logical algorithms. In: Workshop on Programming Logics in memory of Harald Ganzinger, Saarbrücken (June 2005) (invited talk)
López, P., Pfenning, F., Polakow, J., Watkins, K.: Monadic concurrent linear logic programming. In: PPDP 2005: Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 35–46. ACM, New York (2005)
Chaudhuri, K.: The Focused Inverse Method for Linear Logic. PhD thesis, Carnegie Mellon University (December 2006)
Chaudhuri, K., Pfenning, F., Price, G.: A Logical Characterization of Forward and Backward Chaining in the Inverse Method. In: Automated Reasoning, vol. 4130, pp. 97–111. Springer, Heidelberg (2006)
Simmons, R.J., Pfenning, F.: Linear Logical Algorithms. Technical Report CMU-CS-08-104, Carnegie Mellon University (May 2008)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Simmons, R.J., Pfenning, F. (2008). Linear Logical Algorithms. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds) Automata, Languages and Programming. ICALP 2008. Lecture Notes in Computer Science, vol 5126. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70583-3_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-70583-3_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70582-6
Online ISBN: 978-3-540-70583-3
eBook Packages: Computer ScienceComputer Science (R0)