nach oben

Journal of Automated Reasoning

Erschienen in:

06.07.2022

Fast Left Kan Extensions Using the Chase

verfasst von: Joshua Meyers, David I. Spivak, Ryan Wisnesky

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2022

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel Verifying Whiley Programs with Boogie

Nächster Artikel Faster Linear Unification Algorithm

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nur mit Berechtigung zugänglich

A benign set-theoretic assumption to avoid set-of-all-sets paradoxes.

This definition is not the same as that given in [19], but it is equivalent.

Our definition differs from that in [13] in that we do not mandate finiteness.

[x] denotes the equivalence class of x.

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”.

Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley, New York (1996)MATH

Adamek, J., Rosicky, J.: Locally Presentable and Accessible Categories. London Mathematical Society Lecture Note Series. Cambridge University Press (1994). https://doi.org/10.1017/CBO9780511600579

Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)CrossRefMATH

Barr, M., Wells, C.: Category Theory for Computing Science. Prentice-Hall Inc., Upper Saddle River (1990)MATH

Barr, M., Wells, C.: Toposes, Triples and Theories. Springer, Heidelberg (2002)MATH

Bauslaugh, B.L.: Homomorphisms of infinite directed graphs. Ph.D. thesis, Simon Fraser University (1994). http://oatd.org/oatd/record?record=oai:summit.sfu.ca:6543 &q=bauslaugh

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)

Brown, K.S., Spivak, D.I., Wisnesky, R.: Categorical data integration for computational science. Comput. Mater. Sci. 164, 127–132 (2019)CrossRef

Bush, M.R., Leeming, M., Walters, R.F.C.: Computing left Kan extensions. J. Symb. Comput. 35(2), 107–126 (2003)MathSciNetCrossRefMATH

10.

Carmody, S., Leeming, M., Walters, R.: The Todd-Coxeter procedure and left Kan extensions. J. Symb. Comput. 19(5), 459–488 (1995)MathSciNetCrossRefMATH

11.

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)CrossRefMATH

12.

Casacuberta, C., Gutiérrez, J.J., Rosický, J.: Are all localizing subcategories of stable homotopy categories coreflective? Adv. Math. 252, 158–184 (2014). https://doi.org/10.1016/j.aim.2013.10.013MathSciNetCrossRefMATH

13.

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.

Doan, A., Halevy, A., Ives, Z.: Principles of Data Integration, 1st edn. Morgan Kaufmann Publishers Inc., San Francisco (2012)

15.

Fagin, R., Kolaitis, P.G., Popa, L.: Data exchange: getting to the core. ACM Trans. Database Syst. 30(1), 174–210 (2005). https://doi.org/10.1145/1061318.1061323CrossRefMATH

16.

Garner, R.: Understanding the small object argument. Appl. Categ. Struct. (2008). https://doi.org/10.1007/s10485-008-9126-7MathSciNetCrossRefMATH

17.

Garner, R., Shulman, M.: Enriched categories as a free cocompletion. Adv. Math. 289, 1–94 (2016)MathSciNetCrossRefMATH

18.

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.

Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium, vol. 2. Clarendon Press, Oxford (2002)MATH

20.

Kainen, P.C.: Weak adjoint functors. Math. Z. 122(1), 1–9 (1971). https://doi.org/10.1007/bf01113560MathSciNetCrossRefMATH

21.

Kapur, D., Narendran, P.: The Knuth-Bendix completion procedure and Thue systems. SIAM J. Comput. 14(4), 1052–1072 (1985)MathSciNetCrossRefMATH

22.

Kelly, G.: The basic concepts of enriched category theory. Reprints in Theory and Applications of Categories [electronic only] 2005(10) (2005)

23.

Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980)MathSciNetCrossRefMATH

24.

nLab authors: cograph of a functor. http://ncatlab.org/nlab/show/cograph%20of%20a%20functor (2021). Revision 16

25.

nLab authors: essentially algebraic theory. http://ncatlab.org/nlab/show/essentially%20algebraic%20theory (2021). Revision 22

26.

nLab authors: weak factorization system. http://ncatlab.org/nlab/show/weak%20factorization%20system (2022)

27.

Onet, A.: The Chase Procedure and its Applications in Data Exchange. In: P.G. Kolaitis, M. Lenzerini, N. Schweikardt (eds.) Data Exchange, Integration, and Streams, Dagstuhl Follow-Ups, vol. 5, pp. 1–37. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2013). 10.4230/DFU.Vol5.10452.1. http://drops.dagstuhl.de/opus/volltexte/2013/4288

28.

Palmgren, E., Vickers, S.: Partial horn logic and cartesian categories. Ann. Pure Appl. Logic 145(3), 314–353 (2007). https://doi.org/10.1016/j.apal.2006.10.001MathSciNetCrossRefMATH

29.

Patterson, E.: Knowledge representation in bicategories of relations. https://arxiv.org/abs/1706.00526 (2017)

30.

Reyes, M.L.P., Reyes, G.E., Zolfaghari, H.: Generic figures and their glueings: a constructive approach to functor categories. Polimetrica (2004)

31.

Riehl, E.: Category Theory in Context. Dover Publication Inc., Mineola (2016)MATH

32.

Schultz, P., Spivak, D.I., Vasilakopoulou, C., Wisnesky, R.: Algebraic databases. Theory Appl. Categ. 32(16), 547–619 (2017)MathSciNetMATH

33.

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)CrossRefMATH

34.

Schultz, P., Wisnesky, R.: Algebraic data integration. J. Funct. Program. 27, e24 (2017)

35.

Sedgewick, R., Wayne, K.: Algorithms, 4th edn. Addison-Wesley Professional, New York (2011)

36.

Spivak, D.I.: Database queries and constraints via lifting problems. Math. Struct. Comput. Sci. (2014). https://doi.org/10.1017/S0960129513000479

37.

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.

Wells, C.: Sketches: Outline with references. In: Dept. of Computer Science, Katholieke Universiteit Leuven (1994)

Titel: Fast Left Kan Extensions Using the Chase
verfasst von: Joshua Meyers
David I. Spivak
Ryan Wisnesky
Publikationsdatum: 06.07.2022
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 4/2022
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-022-09634-2

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 4/2022

Set of Support, Demodulation, Paramodulation: A Historical Perspective

Tuple Interpretations for Termination of Term Rewriting

Larry Wos: Visions of Automated Reasoning

A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory

From Specification to Testing: Semantics Engineering for Lua 5.2

Correction to: Local is Best: Efficient Reductions to Modal Logic K