Re: Constraints and Functional Dependencies

On Feb 24, 10:08 am, Bob Badour <bbad..._at_pei.sympatico.ca> wrote:
> Marshall wrote:
>
> > 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).

I would phrase that differently: in a real computer, the basic numeric type will be a finite moduo type, like the familiar 32 bit in from C. But yeah.

There are languages out there (scheme?) for which the basic integral type is an arbitrary precision integer. Of course "arbitrary precision"
is not the same thing as "infinite". But an arbitrary precision type is
nonetheless qualitatively different from a modular int type, because in the case of the second, the limitation is on the type itself, but in
the case of the first, the limitation is on the machine, not the type.

(Actually most arbitrary precision types are probably also finite and hence not truly arbitrary precision. I would expect a size limit of 2^32 bytes or words. Even in that case though, the type limit exceeds or approaches the machine limit. And even that limit can be broken, say with run length encoding.)

(Another aside: arbitrary precision isn't as useful as one might guess.
In fact I can only recall one instance in my entire career in which a 64 bit int wasn't sufficient: representing $250,000 in millionths of old Turkish lira. Ha ha! In another forum I recall someone saying that just 40 digits of pi was sufficient to calculate the circumference
of the universe to within one centimeter.)

> How does one express that R has at least one tuple? Or that a specific
> instance exists?
>
> Would the following do?
>
> exists R(a): true
>
> exists R(a): a = literal

Yes and yes, I would say. I asked that first question a while ago and Jan Hidders answered with "an empty existential constraint", which I take to mean

  exists R():

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

Yup.

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

That modification would be necessary if the software was going to actually
do the computation. However there are algebra and proof assistant systems
that don't need to make that modification because they don't do the computation
but rather they instead just manipulate the symbols. Maybe later I'll see if I can coax Coq into verifying a proof of the unboundedness of the
naturals.

Marshall Received on Sun Feb 25 2007 - 01:23:10 CET