Re: Constraints and Functional Dependencies
Date: 24 Feb 2007 08:53:14 -0800
Message-ID: <1172335994.298831.89100_at_8g2000cwh.googlegroups.com>
On Feb 24, 7:55 am, Bob Badour <bbad..._at_pei.sympatico.ca> wrote:
> Marshall wrote:
> > [...]
>
> Those look good to me. Domain constraints are very easy:
>
> forall R(a1,...an): a1 in d1 and ... an in dn
> I don't know why you think one cannot express unboundedness--not that
> the constraint is meaningful for finite computers.
>
> forall R(a): exists R(a'): a' = a + 1
>
> or
>
> forall R(a): exists R(a'): a' > a
One can express unboundedness, but since I was proposing limiting what one can quantify over to named relations, and since the natural numbers are something other than that, (an infinite set) my expressiveness restrictions make it impossible to express the unboundedness *of the natural numbers* specifically.
Although as I mentioned in another post, there do exist
systems that can prove (static) properties of the natural
numbers, using algebraic manipulations, not exhaustive
computation. (Clearly, as you mentioned, the technique
of exhaustive computation is inapplicable to infinite sets.)
Marshall