Viewing profile — wisnesky

That's the approach we're taking to verify LLM-generated SQL code at http://sql.ai .

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…

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

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,…

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 vali…

Yes; categories extend traditional graphs with systems of equations. Hypergraphs extend traditional graphs by allowing edges to be between multiple nodes. Most operations on catego…

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 …

We use it for data integration https://www.categoricaldata.net

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 e…

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…

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 pr…

We've used Poly to prove results about functorial data migration.

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 th…

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 prediction…

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 betwee…

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 …

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…

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 arx…

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…

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 o…

Welcome to the applied category theory community :-)

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 functo…