Numbers and subtypes

[Russell Wallace]

The latest version of the TPTP specification includes among other
things integers and rational numbers, which are disjoint types.

I was quite disconcerted at this, since in mathematics - correct me if
I'm wrong - it is usual to regard integers as a subset of rational
numbers.

Though thinking it over, it arguably makes sense if you consider that
the TPTP, like other higher-order logic systems today, is statically
typed. In statically typed languages that provide rational numbers,
e.g. F# in the standard library or C++ with GMP, the rational number
2/1 is not the same thing as the integer 2. That's quite different
from e.g. Lisp where the rational number 2/1 is indeed the same thing
as the integer 2.

So if we hope for a system that is fundamentally dynamically typed,
arguably we should then aim to end up having the integers indeed be a
subtype of the rational numbers. I think this is reasonably
uncontroversial so far, someone please correct me if I'm wrong?

Now consider Boolean. A logic system that is not statically typed,
does still have to have a notion of the Boolean type, apart from
anything else to license inferences like ~~x = x.

And of course, in the statically typed lambda calculus, Boolean is
disjoint from all other types. Which makes sense, this being the most
obvious way to do it with static typing.

But if we are aiming for a system that is fundamentally dynamically
typed, is there any reason why we can't make Boolean a subtype of
integer?

Apart from anything else, it would also allow us to say that Boolean
is a subtype of probability, which is a subtype of the real numbers.
That feels intuitively right. Of course we still can't feed
probabilities into the crisp Boolean operators, but we can do the
reverse, e.g. have a probabilistic not operator pnot(x) = 1-x defined
on [0..1], which can also accept crisp Boolean values.

Are there any caveats I'm missing?

[Abram Demski]

Russel,

I really like Church numerals. If we arrange things properly, we even get that 0 is "false", in the sense of if-then-else statements (where "true" is the function of two arguments which returns the first argument, and "false" is the function of 2 arguments which returns the second). Unfortunately, 1 and "true" are distinct...

--A natural number n is a function which takes f and x, and returns f(f(...f(x)...)) with n applications of f.
--Zero just returns x, 1 returns f(x), et cetera.
--n+m is found by feeding the result of n into m (with the same choice of f)
--n times m is found by using one to iteratively apply the other

If we also have an untyped "choice" operator (analogous to the typed choice operator in HOL Light), we get (what I think is) a really nice representation of integers, rational numbers, complex numbers, and many other generalisations.

--A (generalised) number is just a function which yields the identity function when applied to the identity function
--Negative n is just a number such that we get 0 when we add it to n
--The reciprocal of a number n is just a number such that we get 1 when we multiply it by n; rational numbers are arbitrary combination of integers and reciprocals of integers via multiplication
--Real numbers are gotten by taking the supremum of arbitrary sets of rational numbers (sets being represented by predicates)
--The square root of n is just a number which yields n when multiplied with itself, giving us a definition for the square root of negative numbers

What's neat about this is that certain types of numbers (that is, negative, complex, etc) make sense for a certain f on a certain data structure, whereas others do not; the choice operator would take care of this question, returning a function if one made sense and refusing if none did.

--Negative numbers make sense of f is reversible on the given data structure
--Complex numbers make sense if there is "rotation" on that data structure with respect to f
--Fractions make sense if the function can be performed in arbitrarily small increments
--etc

Two questions:
--What's the best way to make a predicate which recognises just integers (or just natural numbers)?
--What's the best way to define the ordering of the rationals, which we need for the definition of supremum used to get real numbers?

--
You received this message because you are subscribed to the Google Groups "One Logic" group.
To post to this group, send email to one-...@googlegroups.com.
To unsubscribe from this group, send email to one-logic+...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/one-logic?hl=en.

--
Abram Demski
http://lo-tho.blogspot.com/
http://groups.google.com/group/one-logic

[Russell Wallace]

Erm... Church numbers are definitely a cool hack in the proof of
concept sense, a demonstration that you could (in principle, given
unlimited computing power) build numbers out of pure lambda functions.

But efficiency considerations alone dictate that in practice we
implement numbers in the usual binary format. (Specifically, I'm using
GMP.) Am I missing something?

[Abram Demski]

Russel,

Nah, not missing anything, I'm just being impractical, thinking about how numbers would work logically rather than in implementation.

Ideally, one would be able to prove the equivalence of the binary representation, and then be able to use it from then on.

Anyway, I don't see a problem with integers being a true subset of real numbers. On the other hand, if not, then there's at least a nice structure-preserving injection of them into the reals...

--Abram