-
Presenting Profunctors
Authors:
Gabriel Goren-Roig,
Joshua Meyers,
Emilio Minichiello
Abstract:
Motivated by problems in categorical database theory, we introduce and compare two notions of presentation for profunctors, uncurried and curried, which arise intuitively from thinking of profunctors either as functors $\mathcal{C}^\text{op} \times \mathcal{D} \to \textbf{Set}$ or $\mathcal{C}^\text{op} \to \textbf{Set}^{\mathcal{D}}$. Although the Cartesian closure of $\textbf{Cat}$ means these t…
▽ More
Motivated by problems in categorical database theory, we introduce and compare two notions of presentation for profunctors, uncurried and curried, which arise intuitively from thinking of profunctors either as functors $\mathcal{C}^\text{op} \times \mathcal{D} \to \textbf{Set}$ or $\mathcal{C}^\text{op} \to \textbf{Set}^{\mathcal{D}}$. Although the Cartesian closure of $\textbf{Cat}$ means these two perspectives can be used interchangeably at the semantic level, a surprising amount of subtlety is revealed when looking through the lens of syntax. Indeed, we prove that finite uncurried presentations are strictly more expressive than finite curried presentations, hence the two notions do not induce the same class of finitely presentable profunctors. Moreover, an explicit construction for the composite of two curried presentations shows that the class of finitely curried presentable profunctors is closed under composition, in contrast with the larger class of finitely uncurried presentable profunctors, which is not. This shows that curried profunctor presentations are more appropriate for computational tasks that use profunctor composition. We package our results on curried profunctor presentations into a double equivalence from a syntactic double category into the double category of profunctors. Finally, we study the relationship between curried and uncurried presentations, leading to the introduction of curryable presentations. These constitute a subcategory of uncurried presentations which is equivalent to the category of curried presentations, therefore acting as a bridge between the two syntactic choices.
△ Less
Submitted 17 December, 2024; v1 submitted 1 April, 2024;
originally announced April 2024.
-
Fast Left Kan Extensions Using The Chase
Authors:
Joshua Meyers,
David I. Spivak,
Ryan Wisnesky
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 algorit…
▽ More
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.
△ Less
Submitted 4 May, 2022;
originally announced May 2022.
-
Undecidable First-Order Theories of Affine Geometries
Authors:
Antti Kuusisto,
Jeremy Meyers,
Jonni Virtema
Abstract:
Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation β, and a quaternary equidistance relation \equiv. Tarski established, inter alia, that the first-order (FO) theory of (R^2,β,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,β) with unary predicates is decidable.…
▽ More
Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation β, and a quaternary equidistance relation \equiv. Tarski established, inter alia, that the first-order (FO) theory of (R^2,β,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,β) with unary predicates is decidable. We refute this conjecture by showing that for all n>1, the FO-theory of the class of expansions of (R^2,β) with just one unary predicate is not even arithmetical. We also define a natural and comprehensive class C of geometric structures (T,β), and show that for each structure (T,β) in C, the FO-theory of the class of expansions of (T,β) with a single unary predicate is undecidable. We then consider classes of expansions of structures (T,β) with a restricted unary predicate, for example a finite predicate, and establish a variety of related undecidability results. In addition to decidability questions, we briefly study the expressivities of universal MSO and weak universal MSO over expansions of (R^n,β). While the logics are incomparable in general, over expansions of (R^n,β), formulae of weak universal MSO translate into equivalent formulae of universal MSO.
△ Less
Submitted 25 December, 2013; v1 submitted 28 October, 2013;
originally announced October 2013.
-
Undecidable First-Order Theories of Affine Geometries
Authors:
Antti Kuusisto,
Jeremy Meyers,
Jonni Virtema
Abstract:
Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation (β) and a quaternary equidistance relation (\equiv). Tarski established, inter alia, that the first-order (FO) theory of (R^2,β,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,β) with unary predicates is decidabl…
▽ More
Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation (β) and a quaternary equidistance relation (\equiv). Tarski established, inter alia, that the first-order (FO) theory of (R^2,β,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,β) with unary predicates is decidable. We refute this conjecture by showing that for all n>1, the FO-theory of monadic expansions of (R^2,β) is Π^1_1-hard and therefore not even arithmetical. We also define a natural and comprehensive class C of geometric structures (T,β), where T is a subset of R^2, and show that for each structure (T,β) in C, the FO-theory of the class of monadic expansions of (T,β) is undecidable. We then consider classes of expansions of structures (T,β) with restricted unary predicates, for example finite predicates, and establish a variety of related undecidability results. In addition to decidability questions, we briefly study the expressivity of universal MSO and weak universal MSO over expansions of (R^n,β). While the logics are incomparable in general, over expansions of (R^n,β), formulae of weak universal MSO translate into equivalent formulae of universal MSO.
This is an extended version of a publication in the proceedings of the 21st EACSL Annual Conferences on Computer Science Logic (CSL 2012).
△ Less
Submitted 24 August, 2012;
originally announced August 2012.
