[sc34wg3] Comments on Tau model

[Robert Barta]

On Mon, Jul 26, 2004 at 09:46:15AM +0200, Lars Marius Garshol wrote:
> 
> --- HIGH-LEVEL COMMENTS
> 
> I guess my key question for the author of this model is why he chose
> the particular structure he did. As far as I can tell, almost any
> underlying structure would have served the purpose, since it is the
> operations that do the job.

Lars,

Yes, it's the operations which count. But: Whenever you choose a
'particular structure' then you - in the same step - implicitely
choose the operations which come with it.

So, for example, if you say "A blabla is a set", so you not only
have defined the structure, but also operations (set operations)
for A.

With the above, the choice of the structure is then a matter of
convenience. In one extreme you could squeeze everything in strings of
symbols (like for Turing-Machines), in the other extreme you build
tuples and tuples of tuples to hard-code the structure you want.

In the case of a string expressing subexpressions and properties
can be rather inconvient. If you have chosen many different tuple
structures, then the formalism has to cover many cases.

It is in this tension field that choosing the 'right' structure
is more of an art than that of ultimate truth. The version you
see is probably 5 or 6.

> To put it another way, couldn't the exact same set of operations
> have been used on a quad model? Or on some third model?

I would not know why you could not do that. Maybe the description
is a bit different in complexity.

> The structure of Tau assertions is, it seems, different from both the
> structure of TMRM assertions and TMDM associations.

Yes.

> As far as I can
> tell, there is no groupings of players of the same role (role type in
> TMDM), ....

Yes.

> nor does there appear to be any support for assertion types.

Yes.

> Or is that supposed to be indicated with some undefined role type?

No, as every assertion is a thing by itself which can be referenced
in any other assertion the 'type of an assertion a' is expressed by
another assertion which happens to have the right roles (class, instance).

So there is no special treatment for "association types".

> --- DETAIL
> 
>   "Literals may be numbers of quoted strings"
> 
> Why just two types? In fact, why are the types specified at all? As
> far as I can see they aren't used anywhere.

That is true for the part you see. We have envisaged uses where
numbers could come in very handy. Not sure how this pans out, though.

> What is the predefined identifier "id" used for?

[1] It simply gives an assertion a label. It is used to cross-reference
between assertions.

>   "The sets of assertions is denoted by /A/."
> 
> This should be "set of all", right?

Of course.

>   "Assertions are by default anonymous, but we can name them a
>   predefined role id."
> 
> What does this mean?

It is a restatement of [1].

>   "That way assertions are only equal if they have identical members."
> 
> Surely that applies anyway?

Yes. This sentence has evolved over time and did not get better. It
was meant as explanation and became misleading.

> In 1.3 there are actually two merging rules. If a map is a set of
> assertions there is an implicit merging of equal assertions. The same
> happens when maps are composed using set union.

Yes, but these are no 'particular merging rules', just, say, 'generic
ones', based on the simple identity of things.

> In 1.4 the two basic operations are defined. Interestingly, since all
> is defined in terms of roles in assertions, this is very similar to
> the FM I proposed, if the model I used is changed to use the structure
> I used for associations for *all* statements.

Ye....es. I think it this is a consequence of getting rid of topics,
moving everything into assertions/quadruples/...  Since you only have
now assertions, you only have to worry about these.

> Regarding 2, are you sure that instances/subclassing belongs in the
> core model? In my view this is more suitable for user-space
> vocabulary.

No, I am not sure, whether it belongs here.

But: 1) These both assertions types are so inherent in our ontological
        thinking that they would have a right to be first-class citizens.

 [2] 2) As you pointed out already there is a need to express an
        assertion type and as you point out below the basic operations
        DO NOT make use of this assertion type.

        Now, in practical cases I would like to say

           lars -> player / plays-squash-somewhere

           ^^^^    ^^^^^^   ^^^^^^^^^^^^^^^^^^^^^^

           thing   role     association type

        and not just

           lars -> player

        To define such convenient operations I need to have
        /instance-of/ inside the formalism.

> /A^n/ is presumably the same as /A x A^n-1/ (ie, /A/s cartesian
> product with itself n times)?

Yes.

> 2.2 uses the terms "concept" and "object", but as far as I can tell
> this is the first occurrence of these two terms.

Yes, the first sentence in 2.2 is meant for motivating the following.
In a purely formal document, I would have drop it.

> In 2.2 there are no assertion types. Traversal of the assertions is
> done purely in terms of role types, and no assertion type is tested
> for.

Yes, see [2].

> Also, the operations in 2.2 would produce results for assertions of
> the form (using LTM syntax for simplicity):
> 
>   whatever(a : superclass, b : subclass, c : superclass, d : subclass)
> 
> Surely there is a missing set of constraints here?

They would maybe produce something like

 [ a, b, c, d ], ... [ .......]
 ^^^^^^^^^^^^^^      ^^^^^^^^^^
 first result        last result

where a, b, c, d are assertions.

> In "is-a<sub>m</sub><sup>0</sup>", what is the 0 doing there? Is it
> because you're following 0 subclass steps? Isn't it better just to
> lose that 0?

It is there to clearly distinguish between the "b is a _direct_
instance of c" and "b is an indirect instance of c".

The first one is tricky, it is the latter we mostly are interested
in. Using is-a<sub>m</sub> only would indicate more to me that it
would be the latter.

> In 2.3 the list of operations provided is, interestingly, very
> nearly the same as the one I sketch in my FM proposal. Yours is of
> course much more detailed, but it's interesting that the operations
> seem to be the same.

I wonder how the exists and forall things look like in FM. In the case
of Tau the semantics are extremely trivial to express. For example
'exists' ($m is a map):

    $m [ p ]
  = $m [ p = p ]
  = all assertions in m where there is one evaluation value of p which is the same as p
  = all assertions where there is at least one evaluation value

And 'forall' is just complementary to that.

\rho