Abstract
We present an algebraic theory for a fragment of predicate logic. The fragment has disjunction, existential quantification and equality. It is not an algebraic theory in the classical sense, but rather within a new framework that we call ‘parameterized algebraic theories’.
We demonstrate the relevance of this algebraic presentation to computer science by identifying a programming language in which every type carries a model of the algebraic theory. The result is a simple functional logic programming language.
We provide a syntax-free representation theorem which places terms in bijection with sieves, a concept from category theory.
We study presentation-invariance for general parameterized algebraic theories by providing a theory of clones. We show that parameterized algebraic theories characterize a class of enriched monads.
Chapter PDF
References
Aczel, P.: A general Church-Rosser theorem (1978)
Adámek, J., Borceux, F., Lack, S., Rosický, J.: A classification of accessible categories. J. Pure Appl. Algebra 175(1-3), 7–30 (2002)
Adámek, J., Rosický, J.: On sifted colimits and generalized varieties. Theory Appl. Categ. 8(3), 33–53 (2001)
Adams, R.: Lambda-free logical frameworks. Ann. Pure Appl. Logic (to appear)
Altenkirch, T., Chapman, J., Uustalu, T.: Monads Need Not Be Endofunctors. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 297–311. Springer, Heidelberg (2010)
Amato, G., Lipton, J., McGrail, R.: On the algebraic structure of declarative programming languages. Theor. Comput. Sci. 410(46), 4626–4671 (2009)
Antoy, S., Hanus, M.: Functional logic programming. C. ACM 53(4), 74–85 (2010)
Asperti, A., Martini, S.: Projections instead of variables: A category theoretic interpretation of logic programs. In: Proc. ICLP 1989 (1989)
Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. arXiv:1203.1539v1
Berger, C., Melliès, P.-A., Weber, M.: Monads with arities and their associated theories. J. Pure Appl. Algebra 216(8-9), 2029–2048 (2012)
Braßel, B., Fischer, S., Hanus, M., Reck, F.: Transforming Functional Logic Programs into Monadic Functional Programs. In: Mariño, J. (ed.) WFLP 2010. LNCS, vol. 6559, pp. 30–47. Springer, Heidelberg (2011)
Bronsard, F., Reddy, U.S.: Axiomatization of a Functional Logic Language. In: Kirchner, H., Wechler, W. (eds.) ALP 1990. LNCS, vol. 463, pp. 101–116. Springer, Heidelberg (1990)
Clouston, R.A., Pitts, A.M.: Nominal equational logic. In: Computation, Meaning, and Logic. Elsevier (2007)
Cohn, P.M.: Universal algebra, 2nd edn. D Reidel (1981)
Curien, P.-L.: Operads, clones and distributive laws. In: Operads and Universal Algebra. World Scientific (2012)
Finkelstein, S.E., Freyd, P.J., Lipton, J.: Logic Programming in Tau Categories. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 249–263. Springer, Heidelberg (1995)
Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proc. LICS 1999 (1999)
Fiore, M., Hur, C.-K.: Second-Order Equational Logic (Extended Abstract). In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 320–335. Springer, Heidelberg (2010)
Fiore, M., Mahmoud, O.: Second-Order Algebraic Theories. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 368–380. Springer, Heidelberg (2010)
Gabbay, M.J., Mathijssen, A.: One and a halfth order logic. J. Logic Comput. 18 (2008)
Jagadeesan, R., Panangaden, P., Pingali, K.: A fully abstract semantics for a functional language with logic variables. In: LICS 1989 (1989)
Johann, P., Simpson, A., Voigtländer, J.: A generic operational metatheory for algebraic effects. In: LICS 2010 (2010)
Johnstone, P.T.: Sketches of an Elephant. OUP (2002)
Kammar, O., Plotkin, G.D.: Algebraic foundations for effect-dependent optimisations. In: Proc. POPL 2012 (2012)
Kelly, G.M., Power, A.J.: Adjunctions whose counits are coequalisers. J. Pure Appl. Algebra 89, 163–179 (1993)
Kinoshita, Y., Power, A.J.: A fibrational Semantics for Logic Programs. In: Herre, H., Dyckhoff, R., Schroeder-Heister, P. (eds.) ELP 1996. LNCS, vol. 1050, pp. 177–191. Springer, Heidelberg (1996)
Komendantskaya, E., Power, J.: Coalgebraic Semantics for Derivations in Logic Programming. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 268–282. Springer, Heidelberg (2011)
Kurz, A., Petrişan, D.: Presenting functors on many-sorted varieties and applications. Inform. Comput. 208(12), 1421–1446 (2010)
Lack, S., Rosický, J.: Notions of Lawvere theory. Appl. Categ. Structures 19(1) (2011)
Melliès, P.-A.: Segal condition meets computational effects. In: Proc. LICS 2010 (2010)
Møgelberg, R.E., Staton, S.: Linearly-Used State in Models of Call-by-Value. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 298–313. Springer, Heidelberg (2011)
Moggi, E.: Notions of computation and monads. Inform. Comput. 93(1) (1991)
Moreno-Navarro, J.J., Rodríguez-Artalejo, M.: Logic programming with functions and predicates. J. Log. Program 12(3&4), 191–223 (1992)
Plotkin, G.: Some Varieties of Equational Logic. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Goguen Festschrift. LNCS, vol. 4060, pp. 150–156. Springer, Heidelberg (2006)
Plotkin, G., Power, J.: Notions of Computation Determine Monads. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 342–356. Springer, Heidelberg (2002)
Plotkin, G.D., Power, J.: Algebraic operations and generic effects. Appl. Categ. Structures 11(1), 69–94 (2003)
Plotkin, G., Pretnar, M.: Handlers of Algebraic Effects. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 80–94. Springer, Heidelberg (2009)
Reddy, U.S.: Functional Logic Languages, Part I. In: Fasel, J.H., Keller, R.M. (eds.) Graph Reduction 1986. LNCS, vol. 279, pp. 401–425. Springer, Heidelberg (1987)
Saraswat, V.A., Rinard, M.C., Panangaden, P.: Semantic foundations of concurrent constraint programming. In: Proc. POPL 1991, pp. 333–352 (1991)
Schrijvers, T., Stuckey, P.J., Wadler, P.: Monadic constraint programming. J. Funct. Program. 19(6) (2009)
Staton, S.: Relating Coalgebraic Notions of Bisimulation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 191–205. Springer, Heidelberg (2009)
Velebil, J., Kurz, A.: Equational presentations of functors and monads. Math. Struct. in Comp. Science 21 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Staton, S. (2013). An Algebraic Presentation of Predicate Logic. In: Pfenning, F. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2013. Lecture Notes in Computer Science, vol 7794. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37075-5_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-37075-5_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37074-8
Online ISBN: 978-3-642-37075-5
eBook Packages: Computer ScienceComputer Science (R0)