# Re: Constraints and Functional Dependencies

Date: Sat, 24 Feb 2007 18:08:27 GMT

Message-ID: <va%Dh.744$PV3.10980_at_ursa-nb00s0.nbnet.nb.ca>

Marshall wrote:

> 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

*>*

> Does the term "domain constraint" mean anything different

*> than "type constraint?"*

*>*

*> It is mind bendingly whacky to me to think of merging type*

*> constraints into the general constraint system. This is very*

*> different from the usual programming languages way of*

*> thinking about them, at least for me. But I have to say*

*> I am very intrigued by the idea.*

*>*

*>*

>>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.*

Suppose one has an extent function that returns a relation representing the extent of a type. Then "extent(natural)" is the name for a relation representing the set of all natural numbers.

However, in a real computer, the natural type will be finite not infinite and the unbounded constraint above would always fail (except for empty relations ironically).

How does one express that R has at least one tuple? Or that a specific instance exists?

If that works, I suppose one could describe the extent of the natural numbers as:

(exists extent(natural)(value): value = 1)
and

(forall extent(natural)(value'):

exists extent(natural)(value''): value'' = value' + 1

)

Of course, a finite computer would have to amend the above as follows:

(exists extent(natural)(value): value = 1)
and

(forall extent(natural)(value'):

value' = max(natural) or exists extent(natural)(value''): value'' = value' + 1

)

Assuming a max function that returns the largest value in an ordered type.

> 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
**>
*

Received on Sat Feb 24 2007 - 19:08:27 CET