Skip to main content
main-content
Top

Hint

Swipe to navigate through the articles of this issue

06-07-2022

Fast Left Kan Extensions Using the Chase

Authors: Joshua Meyers, David I. Spivak, Ryan Wisnesky

Published in: Journal of Automated Reasoning

Login to get access
share
SHARE

Abstract

We show how computation of left Kan extensions can be reduced to computation of free models of cartesian (finite-limit) theories. We discuss how the standard and parallel chase compute weakly free models of regular theories and free models of cartesian theories and compare the concept of “free model” with a similar concept from database theory known as “universal model”. We prove that, as algorithms for computing finite-free models of cartesian theories, the standard and parallel chase are complete under fairness assumptions. Finally, we describe an optimized implementation of the parallel chase specialized to left Kan extensions that achieves an order of magnitude improvement in our performance benchmarks compared to the next fastest left Kan extension algorithm we are aware of.
Appendix
Available only for authorised users
Footnotes
1
A benign set-theoretic assumption to avoid set-of-all-sets paradoxes.
 
2
This definition is not the same as that given in [19], but it is equivalent.
 
3
Our definition differs from that in [13] in that we do not mandate finiteness.
 
4
[x] denotes the equivalence class of x.
 
5
Note that the uniqueness of the isomorphism from these tables to any other left Kan extension does not imply there are no automorphisms of the input (for example, we may certainly swap Prof. Finn and Prof. Gil), but rather that there will be at most one isomorphism of the tables above with any other left Kan extension. If desired, we may of course restrict ourselves to only considering those morphisms that leave their inputs fixed, ruling out the swapping of Prof. Finn and Prof. Gil, described in various places in this paper as “leaving Prof. Finn, Prof. Gill as constants”.
 
Literature
1.
go back to reference Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley, New York (1996) MATH Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley, New York (1996) MATH
3.
go back to reference Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998) CrossRef Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998) CrossRef
4.
go back to reference Barr, M., Wells, C.: Category Theory for Computing Science. Prentice-Hall Inc., Upper Saddle River (1990) MATH Barr, M., Wells, C.: Category Theory for Computing Science. Prentice-Hall Inc., Upper Saddle River (1990) MATH
5.
go back to reference Barr, M., Wells, C.: Toposes, Triples and Theories. Springer, Heidelberg (2002) MATH Barr, M., Wells, C.: Toposes, Triples and Theories. Springer, Heidelberg (2002) MATH
7.
go back to reference Benedikt, M., Konstantinidis, G., Mecca, G., Motik, B., Papotti, P., Santoro, D., Tsamoura, E.: Benchmarking the chase. In: Proceedings of the 36th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS ’17, pp. 37–52. ACM, New York, NY, USA (2017) Benedikt, M., Konstantinidis, G., Mecca, G., Motik, B., Papotti, P., Santoro, D., Tsamoura, E.: Benchmarking the chase. In: Proceedings of the 36th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS ’17, pp. 37–52. ACM, New York, NY, USA (2017)
8.
go back to reference Brown, K.S., Spivak, D.I., Wisnesky, R.: Categorical data integration for computational science. Comput. Mater. Sci. 164, 127–132 (2019) CrossRef Brown, K.S., Spivak, D.I., Wisnesky, R.: Categorical data integration for computational science. Comput. Mater. Sci. 164, 127–132 (2019) CrossRef
9.
10.
go back to reference Carmody, S., Leeming, M., Walters, R.: The Todd-Coxeter procedure and left Kan extensions. J. Symb. Comput. 19(5), 459–488 (1995) MathSciNetCrossRef Carmody, S., Leeming, M., Walters, R.: The Todd-Coxeter procedure and left Kan extensions. J. Symb. Comput. 19(5), 459–488 (1995) MathSciNetCrossRef
11.
go back to reference Carmody, S., Walters, R.F.C.: Computing quotients of actions of a free category. In: Carboni, A., Pedicchio, M.C., Rosolini, G. (eds.) Category Theory, pp. 63–78. Springer, Berlin (1991) CrossRef Carmody, S., Walters, R.F.C.: Computing quotients of actions of a free category. In: Carboni, A., Pedicchio, M.C., Rosolini, G. (eds.) Category Theory, pp. 63–78. Springer, Berlin (1991) CrossRef
13.
go back to reference Deutsch, A., Nash, A., Remmel, J.: The chase revisited. In: Proceedings of the Twenty-seventh ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS ’08, pp. 149–158. ACM, New York, NY, USA (2008) Deutsch, A., Nash, A., Remmel, J.: The chase revisited. In: Proceedings of the Twenty-seventh ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS ’08, pp. 149–158. ACM, New York, NY, USA (2008)
14.
go back to reference Doan, A., Halevy, A., Ives, Z.: Principles of Data Integration, 1st edn. Morgan Kaufmann Publishers Inc., San Francisco (2012) Doan, A., Halevy, A., Ives, Z.: Principles of Data Integration, 1st edn. Morgan Kaufmann Publishers Inc., San Francisco (2012)
18.
go back to reference Haas, L.M., Hernández, M.A., Ho, H., Popa, L., Roth, M.: Clio grows up: From research prototype to industrial tool. In: Proceedings of the 2005 ACM SIGMOD International Conference on Management of Data, SIGMOD ’05, pp. 805–810. ACM, New York, NY, USA (2005) Haas, L.M., Hernández, M.A., Ho, H., Popa, L., Roth, M.: Clio grows up: From research prototype to industrial tool. In: Proceedings of the 2005 ACM SIGMOD International Conference on Management of Data, SIGMOD ’05, pp. 805–810. ACM, New York, NY, USA (2005)
19.
go back to reference Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium, vol. 2. Clarendon Press, Oxford (2002) MATH Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium, vol. 2. Clarendon Press, Oxford (2002) MATH
21.
go back to reference Kapur, D., Narendran, P.: The Knuth-Bendix completion procedure and Thue systems. SIAM J. Comput. 14(4), 1052–1072 (1985) MathSciNetCrossRef Kapur, D., Narendran, P.: The Knuth-Bendix completion procedure and Thue systems. SIAM J. Comput. 14(4), 1052–1072 (1985) MathSciNetCrossRef
22.
go back to reference Kelly, G.: The basic concepts of enriched category theory. Reprints in Theory and Applications of Categories [electronic only] 2005(10) (2005) Kelly, G.: The basic concepts of enriched category theory. Reprints in Theory and Applications of Categories [electronic only] 2005(10) (2005)
23.
27.
30.
go back to reference Reyes, M.L.P., Reyes, G.E., Zolfaghari, H.: Generic figures and their glueings: a constructive approach to functor categories. Polimetrica (2004) Reyes, M.L.P., Reyes, G.E., Zolfaghari, H.: Generic figures and their glueings: a constructive approach to functor categories. Polimetrica (2004)
31.
go back to reference Riehl, E.: Category Theory in Context. Dover Publication Inc., Mineola (2016) MATH Riehl, E.: Category Theory in Context. Dover Publication Inc., Mineola (2016) MATH
32.
go back to reference Schultz, P., Spivak, D.I., Vasilakopoulou, C., Wisnesky, R.: Algebraic databases. Theory Appl. Categ. 32(16), 547–619 (2017) MathSciNetMATH Schultz, P., Spivak, D.I., Vasilakopoulou, C., Wisnesky, R.: Algebraic databases. Theory Appl. Categ. 32(16), 547–619 (2017) MathSciNetMATH
33.
go back to reference Schultz, P., Spivak, D.I., Wisnesky, R.: Algebraic model management: a survey. In: James, P., Roggenbach, M. (eds.) Recent Trends in Algebraic Development Techniques, pp. 56–69. Springer, Cham (2017) CrossRef Schultz, P., Spivak, D.I., Wisnesky, R.: Algebraic model management: a survey. In: James, P., Roggenbach, M. (eds.) Recent Trends in Algebraic Development Techniques, pp. 56–69. Springer, Cham (2017) CrossRef
34.
go back to reference Schultz, P., Wisnesky, R.: Algebraic data integration. J. Funct. Program. 27, e24 (2017) Schultz, P., Wisnesky, R.: Algebraic data integration. J. Funct. Program. 27, e24 (2017)
35.
go back to reference Sedgewick, R., Wayne, K.: Algorithms, 4th edn. Addison-Wesley Professional, New York (2011) Sedgewick, R., Wayne, K.: Algorithms, 4th edn. Addison-Wesley Professional, New York (2011)
37.
go back to reference Spivak, D.I., Wisnesky, R.: Relational foundations for functorial data migration. In: Proceedings of the 15th Symposium on Database Programming Languages, DBPL 2015, pp. 21–28. ACM, New York, NY, USA (2015) Spivak, D.I., Wisnesky, R.: Relational foundations for functorial data migration. In: Proceedings of the 15th Symposium on Database Programming Languages, DBPL 2015, pp. 21–28. ACM, New York, NY, USA (2015)
38.
go back to reference Wells, C.: Sketches: Outline with references. In: Dept. of Computer Science, Katholieke Universiteit Leuven (1994) Wells, C.: Sketches: Outline with references. In: Dept. of Computer Science, Katholieke Universiteit Leuven (1994)
Metadata
Title
Fast Left Kan Extensions Using the Chase
Authors
Joshua Meyers
David I. Spivak
Ryan Wisnesky
Publication date
06-07-2022
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-022-09634-2

Premium Partner