wisnesky

6 ms·

1.
by wisnesky 11mo ago
That's the approach we're taking to verify LLM-generated SQL code at http://sql.ai .
2.
Graphs Are Programs(gdotv.com)
4 points by wisnesky 1y ago|1 comments
3.
by wisnesky 1y ago
Hydra is a programming language that uses mathematical abstraction to model graphs within the language itself. It’s an open-source project spearheaded by Josh Shinavier, co-creator of Apache TinkerPop. In Josh’s own words: “In Hydra, progra
4.
Sql Semantic Search(github.com)
2 points by wisnesky 1y ago|1 comments
5.
by wisnesky 1y ago
An open source project to search SQL code 'semantically': up to the meaning of parse trees. For example, searching for 'select from A,B' matches 'select from B,A'.
6.
by wisnesky 2y ago
The code in database vs database in code duality has a long history, and one way to formalize it mathematically uses category theory: the notion of LINQ (language integrated query, such as collection comprehensions) is formally related to t
7.
by wisnesky 2y ago
There is a partial solution to this problem: use formal methods such as symbolic logic and theorem proving to check the LLM output for correctness. We are launching a semantic validator for LLM-generated SQL code at sql.ai even now. (It c
8.
by wisnesky 3y ago
Yes; categories extend traditional graphs with systems of equations. Hypergraphs extend traditional graphs by allowing edges to be between multiple nodes. Most operations on categories are formally undecidable because of the systems of eq
9.
by wisnesky 3y ago
At https://www.categoricaldata.net we claim that symbolic AI is also generative, when eg used in data warehousing. Instead of eg new images, the generatively gives you new primary and foreign keys, new ontologies, contradiction
10.
by wisnesky 3y ago
We use it for data integration https://www.categoricaldata.net
11.
by wisnesky 3y ago
Yes, at least with a strong enough arithmetic (such as Peano's), but that is usually more complicated; for example, you might have to create a Godel numbering or some other "deep embedding" to represent each set as a number.
12.
by wisnesky 3y ago
A foundation for mathematics is any formalism sufficient to prove the results typically taken as axioms in practical mathematics. For example, in ZFC you can define numbers as sets in many different ways and prove that 1+1=2 for each of th
13.
by wisnesky 3y ago
Yes, although Dijkstra was interested in proving programs correct in general, not just in how lambda calculi correspond to logics correspond to categories (a proof technique for program correctness, among other things).
14.
by wisnesky 3y ago
We've used Poly to prove results about functorial data migration.
15.
by wisnesky 3y ago
Yes, in the sense that "math is programming paper instead of computers", being better at one translates to being better at the other. This intuition can even be made precise via the "Curry-Howard isomorphism", upon whic
16.
by wisnesky 4y ago
If you have a symmetric system, you can use group theory to make predictions about it. Similarly, if you have a compositional system, you can use category theory to make predictions about it. As for whether those predictions are useful, o
17.
Hydra: Type-aware transformations for data and programs(hackage.haskell.org)
5 points by wisnesky 4y ago|2 comments
18.
by wisnesky 4y ago
Hydra is a transformation toolkit along the lines of Dragon (Uber), but open source, and with a more advanced type system and other new features. Hydra maps data and schemas between languages in a way which maintains type conformance. It wi
19.
by wisnesky 4y ago
You might try pages 8-16 of this presentation: https://www.categoricaldata.net/cql/lambdaconf.pdf . The examples are relational to relational and simplistic but they do illustrate running the same transformation both
20.
by wisnesky 4y ago
Bi-directional data exchange has many uses. For example, given a set of conjunctive queries Q, because coeval_Q is left adjoint to eval_Q, the composition coeval_Q o eval_Q forms a monad, whose unit can be used to quantify the extent to wh
21.
by wisnesky 4y ago
The way to run conjunctive SQL queries forward and backward is described in this paper, https://www.cambridge.org/core/journals/journal-of-functiona... , (also available on the arxiv), where they are referred to a
22.
by wisnesky 4y ago
Category theory does provide new algorithms if you unroll all of its definitions. For example, it reveals that SQL conjunctive queries can be run both "forward" and "backward" - an algorithm that is invisible in traditio
23.
by wisnesky 4y ago
When I write math papers I often use proof assistants such as Coq to leverage my programming background to avoid some pencil and paper proofs altogether and rule out many sources of human error. If you consider yourself better at programmi
24.
by wisnesky 5y ago
Welcome to the applied category theory community :-)
25.
by wisnesky 5y ago
The answer is yes. There's even a notion of 'categorical normal form' that extends 3NF that guarantees the direct representability of such relational databases as set-valued functors. Spivak talks about it in e.g. http:&#x
26.
by wisnesky 5y ago
The trade-off has to do with computability: because (finitely presented) categories can express so much, reasoning about them (for example, the 'word problem' for them) is undecidable. So to use CT as a modeling language requires
27.
by wisnesky 5y ago
The categorical databases formalism is also known as 'sketches'. For example, here are some slides from NASA et al that connect to David's work but use this alternative phrasing. It shows how to use category theory to &#x27
28.
by wisnesky 5y ago
Open source implementation and academic papers on using CT for databases: https://www.categoricaldata.net
29.
by wisnesky 6y ago
Sum types are harder to express as data integrity constraints that product types - for example, Horn clause constraints can be used to express that a table is a product (or limit, more generally) of other tables, but to express that a table
30.
by wisnesky 6y ago
Oh, such as a list of statements unprovable under a specific Godel numbering? Definitely much more difficult - I never saw such a list in grad school, although I wouldn't rule out the existence of one.

More ›