Re: Ada.Strings.Bounded

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

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.

As a reference, that message was
<b7c7de31-2e96-4f5b-882e-5e991d52ae93@a9g2000prl.googlegroups.com>.

On Apr 16, 12:28 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> How so? Clearly "+" is not closed in Universal_Integer.

No, addition is closed in universal integer.  It's an implication of
its definition. From 3.5.4/14
> Integer literals are all of the type universal_integer, the
> universal type (see 3.4.1) for the class rooted at root_integer,
> allowing their use with the operations of any integer type.

Every universal_integer has a literal expression 'm'. The expression 'm
+1' is also a literal.  All literals have type universal_integer (see
2.4/3).  Therefore 'm+1' is also a universal_integer.

The same kind argument works to argue to prove closure, although that
requires recursion on the structure of 'm'.  Writing up that proof
would be beside the point right now.

> Universal_Integer is a type, merely because ARM tells so.

I should have realized that this was the point of the agreement long
before.  The ARM is wrong on this point, or at the very least
inconsistent.  Either they'll have to just say it's not a type (that
is, an implementable Ada type) or they'll have to change the rules
about integer literals.  The above proof about 'm+1' can be taken as a
proof of inconsistency, if you like.

My attitude is that you can't declare a variable of universal_integer,
so it's no great harm if it's not an ordinary Ada type.  There's
another point I might have made earlier: universal_integer is a type
that could well appear in other programming languages, because it's a
completely abstract type, and I do not mean "abstract" in any of the
ways that's used as a reserved word in any programming language.  By
"completely abstract", I mean it's a pure concept of thought, a
mathematical abstraction.

It's the connection of such mathematically abstract types to
programming language types that was the point of contact with the
original posting.

Eric