|
From: Dmitry A. Kazakov on 6 Sep 2005 04:20 On Mon, 05 Sep 2005 20:20:19 +0200, Georg Bauhaus wrote: > Dmitry A. Kazakov wrote: > >>>Likewise, a computer might surprise us in suggesting that our >>>fine mathematically thought-out program doesn't quite behave exactly >>>as we thought, because of the naughty computer thingy and its >>>quirks. >> >> You are mixing inadequate and inconsistent models. > > The world (our problem domain) *is* inconsistent, > otherwise, if it were consistent, how could we possibly > know what inconsistency is? Inconsistency means that you can derive P and ~P. So far, there were no evidences that the world doesn't obey logic. > We can agree on someting. > (As I said, HALT is the limit, I think we cannot even formally > decide, mathematically, whether consistency is consistent.) You cannot express the sentence above in a formal language. Which does not imply its undecidability. Only proper propositions can be decidable or not. > A computer, being a real world item, has a good chance of > being whatever it is, there is no complete knowledge of a > computer's consistency. Mathematically consistent programs > can be helpful when the set of preferred consistency rules > is both specified and relates to the program. You better show a case where [mathematically] inconsistent program could be usable. [Windows does not count! (:-))] >>>We have >>> lo, hi: arrays -> I, >>> item: arrays x I -> values > >> What about hi >= lo? > > No problem, as hi, lo: arrays -> I are just functions. > (These are "minimal" assumptions, really.) If hi and lo are just arbitrary values then take 3.456 and 1. They are easier to calculate. hi and lo are bounds, as such they have definite contracts. They cannot be "just" values. Once you formulate the contract, it will be pretty easy to show whether it is consistent = no any properly constructed array object violates the contract. It is not rocket science, really... >> Then what would you do >> with modular and enumeration types? > > Use subtypes. Computers are finite, so are types. I don't know what a finite type is. You might mean the domain set of a type. Then you are wrong, the sets of values of Ada's universal types aren't finite. You can have a type which values comprise an uncountable set of any cardinality [I cannot tell for unreachable cardinals, though (:-))] It is not the same as to be able enumerate all these values in one program! There is no any limitation on how bit patterns are mapped to the type values. I can have 0000->Pi, 0001->e, 0010-><whatsoever>. >> What I want is freedom. > > Then choose not use empty arrays, or test for 'length = 0, or > build your own array abstraction, use use Ada.Containers.Vectors, > .... or do not use Ada. Ah, that's your definition of freedom... (:-)) >> I don't want the compiler to decide for me whether >> there must be "off" values or not. > > The compiler does not force you to use "off" index values, > it forces you to use Ada. When this limit is not o.K., ... It sounds as if the whole language design would collapse if empty arrays were constructed otherwise [properly.] Do you really believe in that? >> I in A'First..A'Last that A'Range is 1) ordered, 2) has the lower and upper >> bounds, 3) these bounds belong to the array. These assumptions are not >> always required. Moreover, for some arrays they are wrong. > > A range with A'Last > A'First is not wrong, I see that you don't > like it. It seems you want to restrict Ada by disallowing > programmers to freely use this widespread idiom for expressing > empty arrays, because it violates your preferences for some > consistency of ordered indexing, right? Did I say that? The idiom you trying to push for has a clear application area. This area is *narrower* than one of the array idiom. Then with "off"-values or without them, A'Last shall *not* be less than A'First. Presently the case A'Last < A'First is used to indicate that there is no bounds. It is a quite silly way to handle errors. Instead of an immediate response you return nonsensical values in hope that inconsistency will be handled [or not] later. It is like to make Positive / 0 = -1, if you will use it, you'll get Constraint_Error, if you won't, then, let's call it a useful idiom of dividing to zero as opposed to impractical mathematical definition... -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Dmitry A. Kazakov on 6 Sep 2005 04:24 On 05 Sep 2005 18:13:16 -0400, Robert A Duff wrote: > But the Ada rule is _certainly_ not the "most efficient"! > > If all Strings start at 1, then we reduce the size of the array dope by > 4 bytes. If the average String length in your program is, say, 20 > bytes, you're saving 4 bytes for every 24, or about 17% of the memory > use, which is substantial. Saving memory generally speed up programs > due to cache effects. > > It's really annoying to me that the compiler stores zillions of copies > of the number 1 in memory (one copy for each String object), just > because some oddball String _might_ start at other than 1. > > Furthermore, bounds checking would be much faster, because there would > be no need to load the lower-bound from memory. Memory loads are often > slow on modern machines. > > Furthermore, consider the code generated for 'Length: In Ada, it's > something like: > > if X'First <= X'Last then > X'Last - X'First + 1 > else > 0 > end if; > > If X'First were known to be always 1, it would be: > > X'Last > > If X'First were known to be always 17, it would be: > > X'Last - 16 > > These latter are branch-free code sequences. Branches are often slow on > modern machines. Right. Here is another example to the list: almost any binary operation on strings should do: J := B'First; for I in A'Range loop do something to A(I) with B(J); J := J + 1; -- Can this overflow at the end of loop? (:-)) end loop; or its equivalent. It would be much less pain if either A'First = B'First (for some arrays, as a part of the contract), or at least array renaming worked properly (could shift the bounds.) -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Georg Bauhaus on 6 Sep 2005 05:26 Robert A Duff wrote: > Slices should slide to the lower bound. The Ada rule breaks > abstraction: I had thought that 'First and 'Last etc. are there just for building an abstraction, not to break one. It might well be that using 'First etc breaks people's habits or doesn't meet their assumptions (rather concrete assumptions about string bounds?). But how does it break the abstraction called String?
From: Jean-Pierre Rosen on 6 Sep 2005 05:03 Robert A Duff a ýcrit : > Jean-Pierre Rosen <rosen(a)adalog.fr> writes: > > >>Robert A Duff a ýcrit : > Really? I can see why you might have: > > type Declaration_Kind is (This, That, Mumble, Dumble); > subtype My_Kind is Declaration_Kind range This..That; > subtype Your_Kind is Declaration_Kind range Mumble..Dumble; > > type A1 is array(My_Kind) of Blah; > type A2 is array(Your_Kind) of Glorp; > > But do you really do this: > > type A is array(Declaration_Kind range <>) of Something; > subtype A1 is A(My_Kind); > subtype A2 is A(Your_Kind); Not that often, but it may happen. Especially if you have services like: procedure do_something (On : A); and want to be able to call it on A1 or A2. > "all the time"? Nothing wrong with it; I just think the former case > would be by far more common. More common, yes. But the other do happen. > And do you create *empty* arrays indexed by enums? All the time? ;-) Might happen as default values for the above do_something procedure. Not common, but not impossible. -- --------------------------------------------------------- J-P. Rosen (rosen(a)adalog.fr) Visit Adalog's web site at http://www.adalog.fr
From: Georg Bauhaus on 6 Sep 2005 07:52
Dmitry A. Kazakov wrote: > Inconsistency means that you can derive P and ~P. It's you who says this, stipulating the universal applicability of binary logic. How can I justify that I can only derive P from {}, and not ~P? Because it turns out to be useful. Not because the derivation works. > So far, there were no > evidences that the world doesn't obey logic. Tons. Starting at those things for which there is no explanation. But we don't have a proof that the world is (binary) logical. Wittgestein has made an attempt, but (of course) he had to give up (shut up, in a sense, using an abbreviation of his own words). BTW, people can say P now and ~P at another time, and this causes very little mental stress. >>We can agree on someting. >>(As I said, HALT is the limit, I think we cannot even formally >>decide, mathematically, whether consistency is consistent.) > > > You cannot express the sentence above in a formal language. Which does not > imply its undecidability. Only proper propositions can be decidable or not. If the world is logical, as you claim, then our sentences cannot be illogical, thus our sentences must be proper propositions, thus decidable. > You better show a case where [mathematically] inconsistent program could be > usable. [Windows does not count! (:-))] Inconsistent with what? Empty arrays having A'First > A'Last are ubiquituous; I understand you find this inconsistent. >>>>We have >>>>lo, hi: arrays -> I, > If hi and lo are just arbitrary values I said, hi and lo are functions. I didn't say that they are arbitrary. > hi and lo are bounds, as such they have definite contracts. They cannot be > "just" values. Once you formulate the contract, it will be pretty easy to > show whether it is consistent = no any properly constructed array object > violates the contract. It is not rocket science, really... You have to know the contract of 'First etc. I see they can be surprising, but I don't see a violation of Ada's well working contracts in 'First > 'Last. >>Use subtypes. Computers are finite, so are types. > > > I don't know what a finite type is. You might mean the domain set of a > type. Then you are wrong, the sets of values of Ada's universal types > aren't finite. Ada's types in a real computer program are finite, no matter what. Any value in an Ada program is finite due to de facto capacity constraints. > You can have a type which values comprise an uncountable set > of any cardinality [I cannot tell for unreachable cardinals, though (:-))] I very much doubt that any executable program has ever succeeded in exstablishing a type representing an uncountable set, other than symbolically, or by turning it into a countable finite thing, by way of lazy evaluation. > It is not the same as to be able enumerate all these values in one program! For any infinite type, there needs to be an algorithm or a declaration capable of constructing the values in the type. For infinite types, the algorithms and declarations don't exist. > There is no any limitation on how bit patterns are mapped to the type > values. A limit on which items can be mapped to bit patterns is storage capacity. Storage capacity is a worldly item << infinity. > I can have 0000->Pi, 0001->e, 0010-><whatsoever>. I did answer this. >>>What I want is freedom. >> >>Then choose not use empty arrays, or test for 'length = 0, or >>build your own array abstraction, use use Ada.Containers.Vectors, >>.... or do not use Ada. > > > Ah, that's your definition of freedom... (:-)) I won't ask language designers to rebuild their language just because I prefer a certain, allegedly more consistent, design of arrays, preferred by some in some algorithms, not preferred by others. Is it so much better to introduce ubiquituous case distinctions ('Length = 0?) in every (sub)array algorithm just because there happens to be a mathematical property that may be applied to indexes, forcing A'First > A'Last to be a bad thing? > It sounds as if the whole language design would collapse if empty arrays > were constructed otherwise [properly.] Do you really believe in that? Sure a lot of algorithms will collapse if they have to adopt your consistency rules. If you dislike Ada's arrays, that's o.K.. If you claim to have found the only true rule stating what kind of arrays are consistent with the rule and what kind isn't, then this sounds like the RM has had inconsistent arrays for a number of years now. Shouldn't there be an article somewhere that points out the erratic definitions of array bounds in Ada 83, Ada 95, and the upcoming Ada 05? > Did I say that? If you insist on A'First <= A'Last, then it sounds like you want to restrict Ada's attributes. > The idiom you trying to push for has a clear application area. This area is > *narrower* than one of the array idiom. What is "_the_ array idiom"? The few array types in some languages that I know don't seem to have a problem with "The Last Ones Shall be First" > Then with "off"-values or without them, A'Last shall *not* be less than > A'First. Should this sentence start with "Thou shalst not do what everyone else does"? > Presently the case A'Last < A'First is used to indicate that there > is no bounds. That's wrong, in that it just indicates that A'Last < A'First yields an empty range. > It is a quite silly way to handle errors. Instead of an > immediate response you return nonsensical values What nonsensical values are returned in text like "3 .. 1"? result := default_value; for k in 3 .. 1 loop result := x(k); end loop; How could this be improved using if x'length = 0 then result := default_value; else for k in 3 .. 1 loop result := x(k); end loop; end if; |