research-article

Open access

Functorial semantics for partial theories

Authors:

Ivan Di Liberti,

Fosco Loregian,

Paweł SobocińskiAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL

Article No.: 57, Pages 1 - 28

https://doi.org/10.1145/3434338

Published: 04 January 2021 Publication History

Abstract

We provide a Lawvere-style definition for partial theories, extending the classical notion of equational theory by allowing partially defined operations. As in the classical case, our definition is syntactic: we use an appropriate class of string diagrams as terms. This allows for equational reasoning about the class of models defined by a partial theory. We demonstrate the expressivity of such equational theories by considering a number of examples, including partial combinatory algebras and cartesian closed categories. Moreover, despite the increase in expressivity of the syntax we retain a well-behaved notion of semantics: we show that our categories of models are precisely locally finitely presentable categories, and that free models exist.

References

[1]

J. Adámek, F.W. Lawvere, and J. Rosicky`. 2003. On the duality between varieties and algebraic theories. Algebra universalis 49, 1 ( 2003 ), 35-49.

[2]

J. Adamek and J. Rosicky`. 1994. Locally Presentable and Accessible Categories. Cambridge University Press.

[3]

J. Adámek, J. Rosicky`, and E.M. Vitale. 2011. Algebraic theories. Cambridge Tracts in Mathematics 184 ( 2011 ), 1.

[4]

I. Bethke. 1988. Notes on Partial Combinatory Algebras. Ph.D. Dissertation. Universiteit von Amsterdam.

[5]

G. Birkhof. 1935. On the structure of abstract algebras. In Mathematical proceedings of the Cambridge philosophical society, Vol. 31. Cambridge University Press, 433-454.

[6]

S. L. Bloom and Z. Ésik. 1993. Iteration Theories: The Equational Logic of Iterative Processes.

[7]

F. Bonchi, D. Pavlovic, and P. Sobocinski. 2017. Functorial Semantics for Relational Theories. arXiv preprint arXiv:1711.08699 ( 2017 ).

[8]

F. Bonchi, P. Sobociński, and F. Zanasi. 2018. Deconstructing Lawvere with Distributive Laws. Journal of Logical and Algebraic Methods in Programming 95 ( 2018 ), 128-146. https://doi.org/10.1016/j.jlamp. 2017. 12.002 F. Borceux and D. Dejean. 1986. Cauchy completion in category theory. Cahiers de Topologie et Géométrie Diférentielle Catégoriques 27, 2 ( 1986 ), 133-146.

[9]

A. Carboni. 1991. Matrices, relations, and group representations. Journal of Algebra 136, 2 ( 1991 ), 497-529.

[10]

A. Carboni and R.F.C. Walters. 1987. Cartesian Bicategories I. Journal of Pure and Applied Algebra 49 ( 1987 ), 11-32.

[11]

C. Centazzo. 2004. Generalised Algebraic Models. Presses universitaires de Louvain. https://books.google.cz/books?id= WKTk1n6ggKsC

[12]

C. Centazzo and E.M. Vitale. 2002. A duality relative to a limit doctrine. Theory and Applications of Categories 10 ( 2002 ), 486-497.

[13]

E. Cheng. 2020. Distributive laws for Lawvere theories. Compositionality 2 ( 2020 ), 1.

[14]

J.R.B. Cockett, X. Guo, and J.W Hofstra, P. 2012. Range Categories II: towards regularity. Theory and Applications of Categories 26 ( 2012 ), 453-500.

[15]

J.R.B. Cockett and P.J.W. Hofstra. 2008. Introduction to Turing Categories. Annals of Pure and Applied Logic 156 ( 2008 ), 183-209.

[16]

J.R.B. Cockett and S. Lack. 2002. Restriction Categories I: categories of partial maps. Theoretical Computer Science 270 ( 2002 ), 223-259.

[17]

J.R.B. Cockett and S. Lack. 2007. Restriction Categories III: colimits, partial limits, and extensivity. Mathematical Structures in Computer Science 17 ( 2007 ), 775-817.

[18]

B. Coecke and R. Duncan. 2008. Interacting Quantum Observables. In ICALP' 08. 298-310.

[19]

P.L. Curien and A. Obtułowicz. 1989. Partiality, Cartesian Closedness, and Toposes. Information and Computation 80 ( 1989 ), 50-95.

[20]

D. Dugger. 2001. Combinatorial model categories have presentations. Advances in Mathematics 164, 1 ( 2001 ), 177-201.

[21]

T. Fox. 1976. Coalgebras and cartesian categories. Communications in Algebra 4 ( 1976 ), 665-667.

[22]

P. Freyd. 1966. Algebra valued functors in general and tensor products in particular. In Colloquium mathematicum, Vol. 14. Institute of Mathematics Polish Academy of Sciences, 89-106.

[23]

P. Freyd. 1972. Aspects of topoi. Bulletin of the Australian Mathematical Society 7, 1 ( 1972 ), 1-76.

[24]

P.J. Freyd and A. Scedrov. 1990. Categories, allegories. North-Holland.

[25]

P. Gabriel and F. Ulmer. 1971. Lokal präsentierbare Kategorien. Springer-Verlag, Berlin. v+ 200 pages.

[26]

B. Giles. 2014. An Investigation of some Theoretical Aspects of Reversible Computing. Ph.D. Dissertation. The University of Calgary.

[27]

M. Hyland and J. Power. 2007. The category theoretic understanding of universal algebra: Lawvere theories and monads. Electronic Notes in Theoretical Computer Science 172 ( 2007 ), 437-458.

[28]

J. Kock. 2003. Frobenius algebras and 2D topological quantum field theories. Cambridge University Press.

[29]

S. Lack. 2004. Composing PROPs. Theory and Applications of Categories 13, 9 ( 2004 ), 147-163.

[30]

F.W. Lawvere. 1963. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences of the United States of America 50, 5 ( 1963 ), 869.

[31]

F.E.J. Linton. 1966. Some Aspects of Equational Categories. In Proceedings of the Conference on Categorical Algebra, S. Eilenberg, D. K. Harrison, S. MacLane, and H. Röhrl (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 84-94.

[32]

J.-L. Loday and B. Vallette. 2012. Algebraic operads. Grundlehren der Mathematischen Wissenschaften [Fundamental Principles of Mathematical Sciences], Vol. 346. Springer, Heidelberg. xxiv+ 634 pages. https://doi.org/10.1007/978-3-642-30362-3

[33]

S. Mac Lane. 1965. Categorical algebra. Bull. Amer. Math. Soc. 71, 1 ( 1965 ), 40-106.

[34]

M. Makkai and R. Paré. 1989. Accessible categories: the foundations of categorical model theory. Contemporary Mathematics, Vol. 104. American Mathematical Society, Providence, RI. viii+ 176 pages. https://doi.org/10.1090/conm/104 M. Markl, S. Shnider, and J. Stashef. 2002. Operads in algebra, topology and physics. Mathematical Surveys and Monographs, Vol. 96. American Mathematical Society, Providence, RI. x+ 349 pages.

[35]

E. Palmgren. 2009. Constructivist and Structuralist Foundations: Bishop's and Lawvere's Theories of Sets.

[36]

E. Palmgren and S.J. Vickers. 2007. Partial Horn logic and cartesian categories. Annals of Pure and Applied Logic 145 ( 2007 ), 314-353.

[37]

D. Pavlovic. 2013. Monoidal Computer I: Basic Computability by String Diagrams. Information and Computation 226 ( 2013 ), 94-116.

[38]

J. Power. 2006. Countable Lawvere theories and computational efects. Electronic Notes in Theoretical Computer Science 161 ( 2006 ), 59-71.

[39]

E.P. Robinson and G. Rosolini. 1988. Categories of Partial Maps. Information and Computation 79 ( 1988 ), 94-130.

[40]

R. Street. 1972. The formal theory of monads. Journal of Pure and Applied Algebra 2, 2 ( 1972 ), 149-168.

Cited By

Earnshaw MSobociński P(2024)Regular planar monoidal languagesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100963139(100963)Online publication date: Jun-2024
https://doi.org/10.1016/j.jlamp.2024.100963
Di Lavore ERomán M(2023)Evidential Decision Theory via Partial Markov Categories2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175776(1-14)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175776
Pavlovic D(2022)Lambek pregroups are Frobenius spiders in preordersCompositionality10.32408/compositionality-4-14(1)Online publication date: 13-Apr-2022
https://doi.org/10.32408/compositionality-4-1
Show More Cited By

Index Terms

Functorial semantics for partial theories
1. Theory of computation
  1. Semantics and reasoning
    1. Program semantics
      1. Categorical semantics

Recommendations

From Comodels to Coalgebras

We investigate the notion of a comodel of a (countable) Lawvere theory, an evident dual to the notion of model. By taking the forgetful functor from the category of comodels to Set, every (countable) Lawvere theory generates a comonad on Set. But while ...
Semantics for Local Computational Effects

Starting with Moggi's work on monads as refined to Lawvere theories, we give a general construct that extends denotational semantics for a global computational effect canonically to yield denotational semantics for a corresponding local computational ...
Nominal lawvere theories
WoLLIC'11: Proceedings of the 18th international conference on Logic, language, information and computation

Lawvere theories provide a category theoretic view of equational logic, identifying equational theories with small categories equipped with finite products. This formulation allows equational theories to be investigated as first class mathematical ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 5, Issue POPL

January 2021

1789 pages

EISSN:2475-1421

DOI:10.1145/3445980

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 January 2021

Published in PACMPL Volume 5, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

European Science Foundation
Czech Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
829
Total Downloads

Downloads (Last 12 months)156
Downloads (Last 6 weeks)24

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Earnshaw MSobociński P(2024)Regular planar monoidal languagesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100963139(100963)Online publication date: Jun-2024
https://doi.org/10.1016/j.jlamp.2024.100963
Di Lavore ERomán M(2023)Evidential Decision Theory via Partial Markov Categories2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175776(1-14)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175776
Pavlovic D(2022)Lambek pregroups are Frobenius spiders in preordersCompositionality10.32408/compositionality-4-14(1)Online publication date: 13-Apr-2022
https://doi.org/10.32408/compositionality-4-1
Nester C(2021)A Variety Theorem for Relational Universal AlgebraRelational and Algebraic Methods in Computer Science10.1007/978-3-030-88701-8_22(362-377)Online publication date: 22-Oct-2021
https://doi.org/10.1007/978-3-030-88701-8_22

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents