Re: Ada.Strings.Bounded

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

On Mon, 14 Apr 2008 08:50:21 -0700 (PDT), Eric Hughes wrote:

> On Apr 14, 3:07 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> If you are aiming at Liskov substitutability
>> principle,
> 
> But I'm not aiming for that.  It's related, to be sure, but it's not
> the same.  If you don't acknowledge that a universal type is a
> different creature than an ordinary type, then you would have to see
> only preexisting relationships.

I think it is wrong to consider N and universal_integer equivalent.

>>> So I can now outline what the relationship ought to be:
>>> -- The set of values of an implemented type is
>>>       a _subset_ of the terms of the universal type.
>>
>> Counterexample: NaN of Float.
> 
> I take from what you're saying that the ordinary way of bringing
> floating point arithmetic into a language is not an implementation of
> universal Real numbers.  That's true.

It is not a subset of R. Subseting is not a sufficient condition for a
successful modeling. Actually it is the opposite, a perfect subset cannot
be a good model. The best models of R aren't even close to subsets. For
example intervals with rational bounds.

>> The set of values of a derived type is neither subset or superset. It is a
>> different set.
> 
> If you insist, but this is not derivation.

It makes life a lot easier. Otherwise you will need to introduce encodings,
have to define the underlying bit patterns, and will never be able to
abstract implementations.
 
>>> -- The set of operators on an implemented type
>>>       _satisfy_ the axioms of the universal type.
>>
>> This cannot work because any implementation is necessarily a DFA.
> 
> ???

Programs are DFA (except hardware interrupts etc).

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