I agree with nearly all the points that Barry Smith
has made in favor of using the word "type" as the
official term in the documentation of the ontology.
I have some clarifications and quibbles, but I don't
want to obscure the main point in this note. (01)
When I said that I would be willing to accept "class"
as a synonym, I intended that word to be used only by
those users who are writing something in OWL and need
to add comments in English that relate directly to that
formalism. (02)
But as I said in other notes, the formal statement of
the ontology should be in a formalism that is more
general than OWL, such as Common Logic, which allows
any OWL statement to be automatically translated to
a logically equivalent statement in CL. For any
documentation that relates to the official ontology,
I would recommend the word "type". (03)
I also agree with Barry that the official formalism for
the ontology should clearly distinguish types. In order
to support as many versions of FOL as possible, including
ones that allow quantifiers to range over relations
(such as OWL), CL has a typeless semantics for the core.
However, Appendix A of the draft CL standard defines a
typed language, extended CLIF (Common Logic Interchange
Format), and Appendix B defines another typed language,
extended CGIF (Conceptual Graph Interchange Format): (04)
http://cl.tamu.edu/docs/cl/32N1377T-FCD24707.pdf (05)
Both CLIF and CGIF (in either the core or extended versions)
allow any sentence s in either one to be translated to a
logically equivalent sentence in the other. The typed
version of FOL called Z (which is already an ISO standard)
can be translated to the extended versions of either CLIF
or CGIF. That translation would preserve all the typing,
in the sense that any Z sentence s translated to either
CLIF or CGIF and back to Z would be a typed sentence that
is logically equivalent to the original. (The result might
not be identical to the original s because there may be
some minor shuffling around of subcomponents -- e.g., a
component such as (p & q) might come back as (q & p).) (06)
Since Z is typed and it's already an ISO standard, some
people have asked why we should not use Z as the official
language for ontology. There are several reasons: (07)
1. The Semantic Web languages RDF(S), OWL, and SWRL cannot
be translated to Z, but they can be translated to CL. (08)
2. Z was designed by mathematicians for mathematicians, and
most nonmathematicians hate the notation with a passion. (09)
3. Since syntax arouses passionate arguments pro and con,
the semantics of CL is defined in an abstract syntax
that does not favor any concrete notation. To illustrate
neutrality, Appendices A and B define two notations
that are very different in appearance, but identical in
semantics. These and any other notations that have been
formally defined by a translation to CL semantics can
qualify as "dialects" of CL. Z could be such a dialect. (010)
4. Other important features of CL, which are essential for
supporting the Semantic Web, include support for Unicode
and the ability to permit any URI to be used as a name.
Although Unicode is supported, CL semantics does not depend
on the encoding, and neither CLIF nor CGIF require any
symbols beyond the first 127 (i.e., ASCII). That is not
true of Z, whose official notation goes far beyond the
symbols that are supported in most fonts (although Z does
provide a way to spell out the symbols that are beyond ASCII). (011)
5. CL also supports some important extensions beyond the
usual versions of FOL, such as quantifying over relations.
The CL semantics supports such extensions while preserving
an FOL style of model theory because the quantifiers in
any theory expressed in CL are restricted to a specified
domain (for example, the domain of anything named by a URI). (012)
6. The draft CL standard allows dialects that use a very wide
range of syntax, including notations that look like natural
languages. As an example, I wrote a grammar for Common
Logic Controlled English (CLCE), which can be translated to
or from a typed version of CL, such as extended CLIF or CGIF: (013)
http://www.jfsowa.com/clce/specs.htm (014)
I stopped working on this version in 2004, when we were trying
to finish the specification of CL itself, but the grammar is
still compatible with the current version. I am not proposing
CLCE exactly as presented in this document, but I believe that
a highly readable formal language can be developed along the
lines of CLCE and related languages such as ACE: (015)
http://www.jfsowa.com/logic/ace.htm (016)
I would propose such languages as a more readable *supplement*
to a more traditional dialect of CL. In any question about
semantics, the traditional notation would take precedence. (017)
In previous discussions, I stated one definition of type, and
Barry stated another. The the pros and cons of either one are
moot points, since the semantics of "type" will be determined
by whatever version of logic is adopted. If CL is the logic,
then types would be represented by monadic relations in CL,
which would be represented as restrictions on the quantifiers
in typed dialects of CL. An instance of a type would be anything
in a given model for which the corresponding relation is true. (018)
John Sowa (019)
_________________________________________________________________
Message Archives: http://colab.cim3.net/forum/ontac-forum/
To Post: mailto:ontac-forum@xxxxxxxxxxxxxx
Subscribe/Unsubscribe/Config:
http://colab.cim3.net/mailman/listinfo/ontac-forum/
Shared Files: http://colab.cim3.net/file/work/SICoP/ontac/
Community Wiki:
http://colab.cim3.net/cgi-bin/wiki.pl?SICoP/OntologyTaxonomyCoordinatingWG (020)
|