Re: Ada.Strings.Bounded

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Wed, 16 Apr 2008 07:40:32 -0700 (PDT), Eric Hughes wrote:

> By my
> previous proof about universal_integer, the expression 'm+1' is also a
> universal_integer.

How so? Clearly "+" is not closed in Universal_Integer. For any compiler,
there always exists an Ada program such that:

   M : constant := <some-literal>; -- Compiles
   N : constant := M + 1;  -- Does not compile

[...]
> By assumption, every universal_integer that appears in that program is
> a member of Large_Enough_Integer.

No. It does not include Universal_Integer, Root_Integer and BigNum if the
latter two will ever come. Certainly any of these types (should they become
named) would have either no attribute S'Range defined, or else one raising
Constraint_Error.

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

Universal_Integer is a type, merely because ARM tells so. As I said before
it is not what you hold it for. Further, you cannot have what you want,
because that would be incomputable.

> A compiler, in theory (though certainly not in present practice), is
> capable of generating expressions for arbitrarily large integers.

Any compiler is a program with a finite number of states. Let each state of
it compiles a legal Ada program (in reality the ratio is much lower than
that). Now consider the following set of programs Foo_n:

procedure Foo_n is
   N : constant := <decimal-literal-of-n>;
begin
   null;
end Foo_n;

Clearly, this set is larger that the set of all states. Therefore, there
exists m, such that Foo_m is not compilable. q.e.d.

[Surely, you could design an Ada compiler which would compile one given
legal Ada program. But you cannot have a compiler which would compile any
legal program.]

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de