# 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:

```>>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).

Would the following do?

exists R(a): true

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

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

)

(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

Original text of this message