From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,640b65cbfbab7216 X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!postnews.google.com!w4g2000prd.googlegroups.com!not-for-mail From: Eric Hughes Newsgroups: comp.lang.ada Subject: Re: Ada.Strings.Bounded Date: Sun, 20 Apr 2008 17:44:56 -0700 (PDT) Organization: http://groups.google.com Message-ID: <4c1be2a2-0178-4c1f-8c96-526020550f42@w4g2000prd.googlegroups.com> References: <276e98e3-3b3b-4cbf-b85c-dcae79f11ec5@b5g2000pri.googlegroups.com> <013e1d52-c25f-49ea-83ef-6ac4860858bf@s13g2000prd.googlegroups.com> <8g2rpvi2ahu0$.1ebsyq5yu1whf.dlg@40tude.net> <9a3ad8ca-9f44-42db-9f7c-c5f9e3ee60f3@w1g2000prd.googlegroups.com> <1jdzw15tbj376$.nyv9yml75wj4$.dlg@40tude.net> <80c6fdca-1a89-4d98-b61d-9a405e57d8e5@s13g2000prd.googlegroups.com> <1wh7cbu67y4wz$.7iu8likx0fct.dlg@40tude.net> <144w648u50r6q.1erjxxu0cplbw.dlg@40tude.net> <611360e0-595c-43a7-b5cb-137a278ec0c1@s13g2000prd.googlegroups.com> <15389tuelo6x6$.1c1a6yixordts$.dlg@40tude.net> NNTP-Posting-Host: 166.70.57.218 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: posting.google.com 1208738697 19603 127.0.0.1 (21 Apr 2008 00:44:57 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Mon, 21 Apr 2008 00:44:57 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: w4g2000prd.googlegroups.com; posting-host=166.70.57.218; posting-account=5RIiTwoAAACt_Eu87gmPAJMoMTeMz-rn User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.8.1.14) Gecko/20080404 Firefox/2.0.0.14,gzip(gfe),gzip(gfe) Xref: g2news1.google.com comp.lang.ada:21009 Date: 2008-04-20T17:44:56-07:00 List-Id: 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 . On Apr 16, 12:28 pm, "Dmitry A. Kazakov" 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