database theory based on Heyting algebra instead of Boolean algebra

database theory based on Heyting algebra instead of Boolean algebra

[Vasili I. Galchin]

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

Re: database theory based on Heyting algebra instead of Boolean algebra

[Steve Vickers]

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

Re: database theory based on Heyting algebra instead of Boolean algebra

[Greg Meredith]

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