Re: Partial OSA

[Michal.Walicki@ii.uib.no (Michal Walicki)]

>Don,
>
>You wrote:
>
>> Could you please briefly explain why
>>
>> > the only way to have Nat as a subsort of Int is to specify naturals
>> > and integers in the same module (similarly for rationals Rat, etc.)
>>
>> I don't see this, myself.  (I'm not sure that I know what you mean by
>> "module", but I assume that it is synonymous with "specification".)
>> What's wrong with
>>
>>   INT = ... specification of Int ...
>>
>>   NAT = enrich INT by ... specification of Nat as subsort of Int ...
>
>Ah, I hadn't imagined anyone wanting to do it that way round; thanks.
>So I'd overstated my claim.  It should now be more like:
>
>  The only ways that I can see to have Nat as a subsort of Int are
>  (i) to specify naturals and integers in the same specification body,
>  or (ii - thanks, Don) to first specify integers and then extend with
>  the specification of naturals as a subsort.  If one ever wants
>  integers to be a subsort of rationals, however, one has to start with
>  Rat as the primary sort instead.  Moreover, (ii) wouldn't cater for
>  using naturals without integers around - although one could provide
>  an alternative version of NAT as well, I suppose.
>

Since in the case of enrich, things with the same names are identified,
what's wrong with

        NAT = ... spec of Nat ...

        INT = enrich NAT by ... spec of Int with
                succ: Int -> Int ... other Int stuff
                and Nat as subsort of Int (e.g. by a single explicit definition)

(Perhaps, one gets some new proof obligations, e.g., that the profiles of
'new' and 'old' succ are compatible, or that the predicate definiting 'new'
Nat is satisfied by all and only 'old' Nat's.)

I do not know if there was any conclusion of the discussion on sharing, but
depending on what happens with parameterized specifications, dot notation
and sharing, wouldn't the following one make sense:

        NAT = ....

        INT(NAT) = ... spec of Int with type schema ...
                Int : sort = [\ NAT.zero : -> NAT.Nat
                                NAT.succ : Int -> Int
                                pred   : Int -> Int
                                ... some axioms ...  \]

If this kind of specification is possible it should implicitly include the
sort Nat as a subsort of Int.


        Michal