Re: Questions on possreps

From: David BL <davidbl_at_iinet.net.au>
Date: Tue, 14 Jun 2011 23:50:42 -0700 (PDT)
Message-ID: <e297997c-260d-4555-8324-9ef67697c8e3_at_k15g2000pri.googlegroups.com>


On Jun 15, 1:39 am, Hugh Darwen <hughdar..._at_gmail.com> wrote:

> I deliberately omitted any reference to the IM. It seems from your
> response and Keith Duggar's that there is more interest in the IM in
> particular than in the general type model into which the IM is
> supposed to be incorporated. As Erwin has already noted, the IM makes
> certain modifications to the base model.
>
> Anyway, to address this observation for now (I might come back to
> other points at a later date):
>
> Your points are correct but nevertheless if T2 is a subtype of T1,
> then an invocation of a selector for T1 can denote a value of type
> T2. It wouldn't be a selector for T1 if that were not the case.
> Similarly, every invocation of a selector for T2 denotes a value of
> type T1. Thus the problem that selectors are intended to solve
> remains solved.
>
> I should perhaps make it clear that although Tutorial D includes
> explicit syntax for defining types via possrep declarations, TTM
> itself does not prescribe syntax. A type that is defined solely in
> terms of operator signatures conforms to our model if those operators
> include at least one that satisfies the requirements for being a
> selector (pace the IM as already noted) and counterparts of our THE_
> operators that in Tutorial D are implicitly spawned by possrep
> definitions. A language that somehow enforces these requirements on
> every type definition (pace the IM) conforms to our model.

Thanks, I believe that helps me understand the pertinent differences between our approaches.

Consider this example of two operators used to allow any natural number to be represented (where I'm assuming that the number 0 is a natural number, but not to be confused with the nullary operator 0 that denotes that number, and s is the successor operator):

    Natural <--- 0;
    Natural <--- s(Natural);

I note that under TTM, s is not a selector for type Natural, because there is no invocation of s that denotes the number 0. However, s would be a selector for type Counting (the positive integers). Indeed, one can instead define operators as follows:

    Natural <--- 0;
    Counting <--- s(Natural);
    Natural <--- p(Counting);

where p denotes the predecessor operator. I note that with these signatures the s and p operators are bijective, and indeed meet the TTM requirement for being selectors on their respective declared return types. Furthermore, there is a symmetry in the way each operator represents the THE_component operator of the other operator. That is not surprising of course because the THE_ operators represent the inverse of the associated selector (i.e. they get back the values of the possrep components that were put there by the selector). As it stands however, it seems there is a missing ingredient which is to specify the subtype relationship:

    Counting isa Natural;

I say this is missing from the perspective of thinking of these operator signatures as analogous to production rules of a formal grammar. I want expressions like s(s(s(0))) to be legal. With that analogy, type names are like non-terminal symbols, and brackets, commas and operators (which I think are formalised already as symbols - but I'm not completely clear on that) are the terminal symbols. Type symbols and operator symbols are disjoint. I see the subtype declaration "Counting isa Natural" as adding a production to the grammar in the obvious way. Indeed, an elegant syntax would instead be:

    Natural <--- Counting;

As far as I can see, this way of thinking about inheritance aligns perfectly with the subtype as subset-of-values approach to type inheritance in the D&D IM.

At the moment, I regard this example as an illustration of the fact that the "possible representation" concept adds some hoops to jump through. I wonder whether these hoops should be there in the first place.

For another, and in my opinion much more important illustration of why I'm uncomfortable with the restrictions imposed by the possible representations concept (applied at the logical level of discourse), I refer you to the sections titled "Union types" and "Elegant and orthogonal operators" of my first post on the thread "An alternative to possreps". More specifically to my claim that operators on uncountable types can be very elegant compared to the "imperfect" versions that try to account for the finite nature of computers by imposing what appear tantamount to possible *physical* representation restrictions on the (abstract) types themselves. Received on Wed Jun 15 2011 - 08:50:42 CEST

Original text of this message