nach oben

Tipp

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, um Zugang zu erhalten

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 möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

über 69.000 Bücher
über 500 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 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

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.013 MathSciNetCrossRefMATH

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.1061323 CrossRefMATH

16.

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

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/bf01113560 MathSciNetCrossRefMATH

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.001 MathSciNetCrossRefMATH

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

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Fast Left Kan Extensions Using the Chase

Abstract

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Abstract

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 4/2022

Verifying Whiley Programs with Boogie

Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic

A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column

A Formalization of the Smith Normal Form in Higher-Order Logic

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

Pardinus: A Temporal Relational Model Finder

Premium Partner