Re: Ada.Strings.Bounded

[Eric Hughes <eric.eh9@gmail.com>]

On Apr 16, 2:16 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> Universal_Integer is merely an integer type.

OK, now you're just wrong.  Wrong, that is, assuming that by "integer
type" you mean an "integer type as defined by Ada" and not some other
notion of "integer type".  I've never seen you to acknowledge any
other kind of type here, so I believe I'm making that assumption in
good faith.

Suppose there existed some single and specific Ada integer type M
which is the same type as universal_integer.  All non-modular integer
types are defined by ranges (see 3.5.4 "Integer Types").  Since M is a
scalar type, the lower bound is M'First and the upper bound is M'Last
(see 3.5).  Since M is an integer type, it is declarable.  Let 'm' be
an integer literal by which the upper bound of M can be declared.  By
the premise, 'm' is an expression of universal_integer.  By my
previous proof about universal_integer, the expression 'm+1' is also a
universal_integer.  But 'm+1' is not a member of M.  Thus M cannot be
a type for universal_integer.

Now you'll come right back and cite things that aren't in the language
specification: specific compilers and specific programs.  Were you to
insist upon citing these, it would be tantamount to saying the
standard isn't actually normative, that instead practice is
normative.  But then I'd believe that you don't know the meaning of
the word "normative".

But I'll address them anyway, to forestall confusion.

Let's start with programs.  Take a the entire source code of any
program.  It's finite.  For that body of code, there's a
universal_integer expression of greatest absolute value.  Call it
'n'.  Declare the type
    type Large_Enough_Integer is range -n .. n ;
By assumption, every universal_integer that appears in that program is
a member of Large_Enough_Integer.  Furthermore, every integer type has
bounds that are members of Large_Enough_Integer.  Thus every integer
value that could ever be in that program has a value that's a member
of Large_Enough_Integer.  But Large_Enough_Integer is not the same as
universal_integer, because the value of 'n+1' is not in
Large_Enough_Integer and it is in universal_integer.  Thus, what's
true is the following predicate:
   For every program P,
   there exists an integer type N,
   for all executions E of P,
   for all times T within E,
   for all variables X within P,
   the value of X at time T within E is a value of N.

This predicate does not make N into universal_integer.  What it says
is that there's a relativized version of universal_integer which is
just barely adequate for every program.  But universal_integer is NOT
defined on a program-by-program basis.  It's defined for the language
as a whole.  For each program, there's a large-enough type, but that
type is not universal_integer.  It's supremum_integer_for_program_P.

The case for compilers is rather more subtle.  Let's dispose of the
easy case first.  Suppose there's some internal limit on the size of
integer types that a compiler accepts; call the type at that limit
'supremum_compilable_integer'.  Then that compiler does not accept
programs P where supremum_integer_for_program_P won't fit into
supremum_compilable_integer.  Now 'supremum_compilable_integer+1' is
also a universal_integer, but one that this compiler does not accept.
Now there's no requirement that a compiler be able to handle every
universal_integer in order to be a conformant compiler.  Such a
requirement would be impossible to satisfy, because it would require
an execution size that was unbounded, even though the compiler itself
could be bounded.  Hence for this case too, there's a relativized
version of universal_integer that applies to the compiler, but that
type isn't universal_integer either.

For a compiled program with an internally limited compiler, then, we
have the following sketch of potential type relationships:
    supremum_compilable_integer --> supremum_integer_for_program_P -->
root_integer
I didn't put universal_integer in there, though, because it's not a
type in the same sense that these others are.

A compiler, in theory (though certainly not in present practice), is
capable of generating expressions for arbitrarily large integers.
I'll be willing to discuss this case later, after the simpler cases
are properly disposed of.

Eric