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/ ]