database theory based on Heyting algebra instead of Boolean algebra
Hello, I'm sorry that this a bit off topic (but both algebras are categories), but I don't know where to post in order to get an intelligent answer. Is there any research to base data base queries on Heyting algebra, i.e. intuistionistic logic? Thanks, Vasili [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Vasili, Are you familiar with the use of monads as an approach to modeling storage semantics and access? The most high profile of these efforts is LINQ. XQuery's FLWOR expressions are also based around this. i've been investigating a very rich generalization. You get a logic out of the following data: - a distributive law, d, between - a monad, T, representing the algebra of your term language (think what's described by the DB schema) - a monad, S, representing some notion of collection (set, list, tree, graph...) The distributive law, d : ST -> TS is showing how collections of terms ST are representable as terms over collections, TS. Then SELECT-FROM-WHERE is precisely a comprehension which as Wadler shows maps clearly onto monadic semantics. The generalization allows you to consider collections that have notions of state. As a toy example, if your notion of collection is a quantale, then you get a (not very convincing) notion of update. This is closely related to current experiments factoring transactional semantics through a monadic presentation. In fact, i've recently been helping folks looking at the JTA specification arrived at a comprehension-based presentation. (Check out the Scala and Lift mailing lists for that thread.) i've written up and coded examples of how this works for 3 different term languages: the usual notion of tuples (resulting in what one would expect, a relational calculus), a graph algebra (resulting in a query language for graphs), and a process algebra. You can find a blog entry about it, with pointers to working code here<http://biosimilarity.blogspot.com/2009/01/3-applications-of-indexed-composition.html> . Another nice thing about this approach is that it factors nicely through languages with reduction semantics such as lambda calculi or process calculi. So, you can extend the query semantics to include symbolic reduction. In some sense, you turn a model-checker into a query engine allowing you to add Hennessy-Milner-style modal operators to the query language. Best wishes, --greg On Wed, Jun 10, 2009 at 1:42 AM, Vasili I. Galchin <vigalchin@gmail.com>wrote:
Hello,
I'm sorry that this a bit off topic (but both algebras are categories), but I don't know where to post in order to get an intelligent answer. Is there any research to base data base queries on Heyting algebra, i.e. intuistionistic logic?
Thanks,
Vasili
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Vasili, I'm not sure how much this will answer your questions, but there was some research towards the end of the last century relating databases and powerdomains. In a sense, then, the associated logic of database queries is that of the open sets of the domain, i.e. geometric logic, and hence (at least in its finitary form) a fragment of intuitionistic logic. The names I associate with this work are Carl Gunter and Peter Buneman. I wrote a 1992 paper "Geometric Theories and Databases" that was inspired by them, though its main content was a topos-theoretic construction. Regards, Steve Vickers. Vasili I. Galchin wrote:
Hello,
I'm sorry that this a bit off topic (but both algebras are categories), but I don't know where to post in order to get an intelligent answer. Is there any research to base data base queries on Heyting algebra, i.e. intuistionistic logic?
Thanks,
Vasili
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (3)
-
Greg Meredith -
Steve Vickers -
Vasili I. Galchin