Re: SUO: type equivalence
----- Original Message -----
From: "David Whitten" <whitten@lynx.eaze.net>
To: <standard-upper-ontology@ieee.org>
Sent: Thursday, November 02, 2000 12:17 PM
Subject: Re: SUO: type equivalence
>
> Robert E. Kent said:
> > I am currently contemplating quotients of "logical languages" via type
> > equivalence, and would be interested to know what has been done on this
> > subject. The central axiom would seem to be that relational type
> > equivalence implies the type equivalence of its signature. To wit: (
> > where == means type equivalence)
> > if rho_1 == rho_2 then arity(rho_1) = arity(rho_2) and
> > sign(rho_1)(x) == sign(rho_2)(x) for all x in arity(rho_i), i = 1, 2.
> > This of course can easily be framed in KIF. Are there other obvious
> > axioms?
>
> I would like to know what you think a signature is.
The signature of a relation type is a constraint on the types of entities
that may be used as relational arguments. I believe that this is the same
notion as the signature in CGs
[http://www.bestweb.net/~sowa/cg/cgdpansw.htm#Header_28], and that it is
stronger than the nth-domain constraint
[http://ltsc.ieee.org/logs/suo/msg01047.html]. I use "variables" to index
the arguments, thus abstracting from position. Possibly, you could use
the nth-argument-name in the SUO starter ontology as such a variable.
> In my starter structural ontology, the distinction is made between
> the instance-of and the subclass-of relations on an argument to a
> relation.
> This means that if you know the argument to a relation is
> an instance of CLASS, you must further specify which class it is a
> subclass of. I would also argue that you need to deal with
> inter-argument dependencies as well as only intra-argument definitions.
In order to make clear the underling mathematics, my definition of "logical
language" does not use constraints other than type declarations. These come
in later when defining an abstract ontology. As I mentioned in my discussion
of languages as mathenatuical objects
[http://ltsc.ieee.org/logs/suo/msg01864.html], this definition of "logical
language" is very close to Chris Menzel's description
[http://ltsc.ieee.org/logs/suo/msg01792.html] of "sorted languages/logics."
I want to define morphisms of "logical languages" in order to define
language constructors -- operators on building block languages.
> A separate issue is specifying how propositions that use the relation
> are constrained. For some relations, it doesn't make sense to have two
> propositions that are true at the same time.
> As an (admittedly flawed) example, if you had a 'COLOUR' relation
> which related automobiles to a single member of the set
{RED,YELLOW,BLUE},
> it would be a useful part of the signature/definition of the COLOR
> relation to say that if you have (COLOUR AUTO-9876 RED) that you
> cannot have (COLOUR AUTO-9876 BLUE) as well.
I had some brief discussion of monadic entity type constraints in my message
[http://ltsc.ieee.org/logs/suo/msg01789.html] that introduced my definition
of "logical language". On entity types we may place (monadic) sequent-style
constraints of the form a1, ..., am |- b1, ..., bn, which include subtype
(entailment) constraints a |- b, necessity constraints |- b , covering
constraints (exhaustive cases) |- b1, b2 , disjointness constraints
(incompatibility types) a1, a2 |- , and incoherent types a |- . But these
were simple global constraints on entity types, not geared toward single
relations.
> These are some of the structural relations that I am trying to define
> for version 3 of the Starter Structural Ontology.
>
> David (whitten@lynx.eaze.net) (713) 791-1414 ext 6116
>