Re: 3DLDF

[Hans Aberg]

At 01:08 +0100 2004/08/15, Frank Heckenbach wrote:
>No, it's just a different paradigm. C wants to specify the internal
>representation (floating point), while Pascal (not sure about
>FORTRAN) wants to provide a real type (i.e., a type of some real
>numbers) without specifying the internal representation.

Why don't you stick to calling the float types "reals", so that we get some
peace and quiet in this list. :-) You are free to do it, even though the
floats only have some values in common with the real numbers in math, and
do not obey the arithmetic rules of real numbers. Parallel to this
discussion, the part of this thread that deals with the subject "3DLDF", we
are trying to attack computational problems that arises from the fact that
floats cannot represent real numbers properly.

>> >> I think I pointed out that the set of real numbers is in math, as well in
>> >> computers, when done correctly, developed using an axiomatic system.
>> >
>> >And so are integers. What does this have to do with the terminology?
>>
>> I have lost you here.
>
>Same here. You brought up this topic of axiomatic systems. I don't
>know how it's related to the discussion.

This is how the set of real numbers are introduced in math as well as in
computers.

>> >> The use of float and int in say C is is more or less correct, as one
>> >> speficies which values can be used, and all those values are potentially
>> >> reachable.
>> >
>> >Not in C (where those terms are used).
>>
>> Sure, check the header <limits.h>.
>
>This header states the limits. Numbers outside the bounds are not
>reachable. Of course, this depends on the C implementation, platform
>etc., and for any integer or floating point number there can
>potentially be a C implementation that supports this number.

So in C, the floating point types are evidently finite in their potential
values. This need not be so, of course, in multiprecision packages.
(Perhaps this can be achieved in GNU GMP.)

>Similarly, for any given real number, there can potentially be a
>Pascal implementation that supports this number. (Even if
>transcendent, it could just define this particular number as a
>special symbol.) So, according to this definition, all real values
>are potentially reachable. (With a big emphasis on potentially, of
>course.)

So go ahead and make a single Pascal compiler that potentially admits all
real numbers. I feel sure that the original designer never had this idea in
his head.

>Just as little as C `int' values satisfy basic arithmetic
>properties, so it's hard to think of them as integral numbers?

The integral types of C contains "integral numbers", but as type does not
represent the set of integers in math. If you want to have a set of
integral numbers in math which are not the set of integers, just take the
integral numbers in an algebraic number field.

>IMHO it's possible to think of them as such in both cases, as long
>as you're aware of the restrictions, which applies to many other
>areas of programming.

You may think of them as whatever you like, but that is not what they are
logically. You may think of the set of real numbers as a continuous line,
but nobody has produced a real line in reality. It is essential in math to
create very powerful images, intuitive to humans, but that should not be
confused with their logical structure.
>> >Yes, but still it can only represent a tiny fraction of all real
>> >numbers, or of all lists of integer numbers etc.
>>
>> You can only do that in pure math as well, as you are limited by expressing
>> them via a metamathematical system, which is only potentially countable
>> infinite. This is essentially a special case of the Skolem "paradox".
>
>But mathematicians don't claim they can write down every real
>number, and don't make a distinction between those they can and
>can't write down (except in special situations, e.g. when dealing
>with computability etc., but not generally when using numbers or
>proving theorems about real numbers).

In object mathematics one does not make a distinction between numbers one
can write down and cannot write down, but one certainly does that in
metamathematics. And the latter is what one uses when implementing the
object math in a computer.

I, as well as a number of other people, are working on implementing this
stuff in a computer. Not many years form now there will commonly programs
that combines what is now different programing language styles. There is
also a crisscross of ideas, for example, ML, predecessor to Haskell, was
created as a metalanguage to the theorem prover Isabelle. These type
theories then sprung out from attempts to solve problems in metamathematics
of higher order theories. As these developments are taking place, it is
important to straighten out the earlier, sometimes sloppy, terminology.

Here are some references on theorem proving:
  http://www-unix.mcs.anl.gov/AR/others.html
  FAQ of newsgroup comp.constraints.
  http://www.afm.sbu.ac.uk/
  http://www.cse.psu.edu/~dale/lProlog/
 Qu-Prolog:
  http://www.itee.uq.edu.au/~pjr/HomePages/QuPrologHome.html
Qu-Prolog, for example, has a ZF axiomatic set theory as a library, so one
can define a proper real numbers type using that.

  Hans Aberg