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.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC 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!news4.google.com!feeder1-2.proxad.net!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: Ada.Strings.Bounded Newsgroups: comp.lang.ada User-Agent: 40tude_Dialog/2.0.15.1 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Reply-To: mailbox@dmitry-kazakov.de Organization: cbb software GmbH References: <96x8my4o4m7e.fskzcb6i31ty$.dlg@40tude.net> <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> Date: Wed, 16 Apr 2008 20:28:52 +0200 Message-ID: <15389tuelo6x6$.1c1a6yixordts$.dlg@40tude.net> NNTP-Posting-Date: 16 Apr 2008 20:28:52 CEST NNTP-Posting-Host: 94b97629.newsspool2.arcor-online.net X-Trace: DXC=NUd2iik\=D=L2C_`koXfC5A9EHlD;3Yc24Fo<]lROoR1Fl8W>\BH3Y2dNlZGHZ]fc>DNcfSJ;bb[5IRnRBaCd2=kM?6Y^oZ0jmM=Hb;he?3 X-Complaints-To: usenet-abuse@arcor.de Xref: g2news1.google.com comp.lang.ada:20976 Date: 2008-04-16T20:28:52+02: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. How so? Clearly "+" is not closed in Universal_Integer. For any compiler, there always exists an Ada program such that: M : constant := ; -- 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 := ; 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