Re: An alternative to possreps

From: David BL <davidbl_at_iinet.net.au>
Date: Sat, 18 Jun 2011 00:54:58 -0700 (PDT)
Message-ID: <18da2bfd-3237-439c-ac67-9cea39b82282_at_h30g2000prf.googlegroups.com>


On Jun 17, 8:15 pm, Hugh Darwen <hughdar..._at_gmail.com> wrote:

> TTM is not at all concerned with syntax. It uses the terms "selector"
> and "possrep" to define concepts on which to base the semantics of
> certain operators that it proposes to be required in connection with
> every type. A selector for type T is a bijective function (assuming a
> canonical form for its domain), mapping possrep values to values of
> type T and vice versa. It is the inverse mapping that allows our
> "THE_" operators to be defined for each possrep component.

[snip]

> Thus, I would agree that David's proposal is a possible replacement
> for Tutorial D's way of defining scalar types, but it doesn't yet do
> the job of guaranteeing those required semantics.

Towards that aim, I rather like the idea of extending the syntax of my proposed DDL slightly by allowing for bidirectional arrow symbols on the operator signature declarations. This is to declare the fact that the operator is bijective (a "selector"). This is on the domain which is the cartesian product on the declared types of the arguments, or a restricted comprehension on the same, (designated with a boolean expression over the names of the arguments coming after the keyword 'on'). For example:

  type Rational;

  Rational <-->
    rational(

        Integer numerator,
        Integer denominator)
    on  denominator > 0 and
        coprime(numerator,denominator);

This selector declaration implicitly declares the component-wise operators on its inverse:

  Integer <--- numerator(Rational);
  Integer <--- denominator(Rational);

There are some close similarities to Tutorial D, but some useful syntactic differences (e.g. subtype declarations are orthogonal, and it is easy to see how additional selectors can be independently declared on pre-existing or third party types).

The following is the definition of literal given in TTM:

  "A literal is an expression denoting a selector   operator invocation (see RM Prescriptions 4, 9,   and 10) in which every argument expression is a   literal in turn."

Elsewhere, TTM refers to the fact that a literal denotes a value, and this is the usual terminology for a formal semantics. I'm not certain, but my impression is that the word 'denoting' in the above definition of literal actually relates to providing latitude to the language (i.e. consistent with Hugh saying "TTM is not at all concerned with syntax"). It is permissible for a literal expression to use operators that are not selectors, but only to the extent that there is a defined sense in which that expression is regarded as a convenient alternative syntax of an expression only using selectors.

For the time being I'll restrict myself to operators that are selectors. I want to investigate what it means to employ nullary operators like 0 (not to be confused with the number which it denotes). Can a nullary operator be a selector? Indeed it can, but only if both the domain and codomain are the empty set. What is needed is a subtype of Natural, with the subtype-by-constraint condition equal to 'false'. Let's call this empty subtype EmptyNatural. This suggests the following:   Counting isa Natural;
  EmptyNatural isa Natural;

  EmptyNatural <--> 0;
  Counting <--> successor(Natural predecessor);

In general the inverse of a unary selector operator without an 'on' constraint is also a unary selector operator without an 'on' constraint. Therefore it is assumed the following selector is implicitly declared:

  Natural <--> predecessor(Counting successor);

So, in a slightly tricky fashion, we have managed to meet the requirement that each type has at least one selector as per TTM.

Given that there is a defined sense in which nullary operators can be regarded as selectors, it would now be appropriate to relax that restriction on all nullary operators. So the end result is simply:

  Counting isa Natural;
  Natural <--- 0;
  Counting <--> successor(Natural predecessor); Received on Sat Jun 18 2011 - 09:54:58 CEST

Original text of this message