Re: Constraints and Functional Dependencies

From: Marshall <marshall.spight_at_gmail.com>
Date: 24 Feb 2007 08:09:28 -0800
Message-ID: <1172333368.439634.100140_at_t69g2000cwt.googlegroups.com>


On Feb 24, 6:18 am, paul c <toledobythe..._at_oohay.ac> wrote:
> Marshall wrote:
> > ...
> > In a data management context, there is some value to restricting
> > what we can quantify over as being only attributes of declared
> > relations (whether variables or constants.) So, we can't express
> > the "no-upper-bound" property of the natural numbers; they aren't
> > a database table so we can't quantify over them.
> > ...
>
> Thanks for a theory topic at last. Minor question - is it not rather
> that we can express it, but agree not to because we can't always compute it?

It is true that the reason behind it all is that we can't check it. Here by
"check" I mean specifically that the technique of doing the computation
for every value in the set being discussed is impossible. (Even in the case of, say, 32 bit ints the technique, while not impossible, is
likely
prohibitive.)

In response to that, I proposed some specific restrictions on range variables that actually do make it impossible to express. But it's true that expressing it using standard quantifiers is no problem.

  not exists n in N: forall m in N: n > m

I believe there are software systems that can work with expressions of this form. I don't know whether they could automatically find a proof of this specific formula, but I suspect they could if you prodded them enough. They could certainly verify a supplied proof.

> eg., if n is not infinite, just has a finite number of values, wouldn't
> R(n) OR NOT R(n) enumerate all possible values of n?

If R is finite and n is an attribute of R, then you can express a constraint on all values of n (even with my restrictions) with just:

  forall R(n): ...

Marshall Received on Sat Feb 24 2007 - 17:09:28 CET

Original text of this message