SUO: Re: Re: motion for the IFF Foundation Ontology version 1.0
All,
The original motion for the IFF Foundation Ontology version 1.0 was
apparently received by everyone, but does not seem to have entered the
archive. It contained a reasonably important note at the end, which I resend
now for archival purposes. That note appears at the end of this message
after the double line. Thanks.
Robert E. Kent
rekent@ontologos.org
----- Original Message -----
From: "Robert E. Kent" <rekent@ontologos.org>
To: "SUO" <standard-upper-ontology@ieee.org>
Sent: Thursday, July 26, 2001 1:54 PM
Subject: SUO: Re: motion for the IFF Foundation Ontology version 1.0
> ----- Original Message -----
> From: "Robert E. Kent" <rekent@ontologos.org>
> To: "SUO" <standard-upper-ontology@ieee.org>
> Sent: Thursday, July 26, 2001 1:45 PM
> Subject: SUO: motion for the IFF Foundation Ontology version 1.0
>
>
> >
> > All,
> >
> > I move that this group commence work on the IFF Foundation Ontology
> version
> > 1.0 [submitted on July 20, 2001] posted at
> > [http://suo.ieee.org/IFF-Foundation-Ontology.pdf] (670 KB, 111 pages),
> with
>
> That was the link yesterday, but it looks like the address has been
changed
> now to [http://suo.ieee.org/Kent-IFF.pdf]. Anyway, it is one of the expert
> contributions listed on the page [http://suo.ieee.org/suopapers.htm].
>
> Robert E. Kent
> rekent@ontologos.org
>
==================================================
I am releasing the IFF Foundation Ontology in steps called versions. Please
correlate the following comments with Figure 1 on page 1 of the version 1.0
document entitled "IFF Foundation Ontology Architecture (with
dependencies)."
o The IFF Foundation Ontology version 0.0 [submitted on June 20, 2001]
contained terminology and axioms for the conglomerate namespace and the core
namespace for classes and functions. Currently there are 11 terms introduced
in the conglomerate namespace and about 130 terms introduced in the core
namespace. Terms were placed in these namespaces on the basis of need
-- this need coming from ongoing work in either the Category Theory Ontology
in the upper metalevel or the Model Theory Ontology in the lower metalevel
(see dependencies in Figure 1). Of those 130 terms, 100 are concerned with
finite limits, especially pullbacks. I expect that the core namespace will
eventually grow to contain several hundred terms. The terms of the core
namespace are partitioned into the following sub-namespaces (with inclusion
indicated by the dot notation): the top-level core namespace (SET)
containing terminology for classes, (SET.FTN) for functions, (SET.LIM) for
finite limits including the terminal class, (SET.LIM.PRD) for binary
products, (SET.LIM.EQU) for equalizers, (SET.LIM.SEQU) for subequalizers
(amongst other things, subequalizers are needed to define partial orders and
equivalence relations), (SET.LIM.PBK) for pullbacks, and (SET.TOP) for topos
structure. In the other dependency direction, the needs of the IFF
Foundation Ontology are minimal -- it only requires the following terms from
the Basic KIF Ontology (KIF)
[http://grouper.ieee.org/groups/suo/email/msg04183.html]: 'KIF$class',
'KIF$relation', 'KIF$subclass', 'KIF$functional', 'KIF$signature', '[-]',
'pair', '1', and '2'.
o The IFF Foundation Ontology version 1.0 [submitted on July 20, 2001 --
the version under consideration now] contains terminology and axioms for (1)
the core namespace: classes and functions, and (2) the IFF Category Theory
(sub)Ontology. So version 1.0 has added the IFF Category Theory Ontology to
version 0.0. I think the SUO community will find this addition to the IFF
Foundation Ontology to be quite interesting; particularly since it makes
heavy use of the core namespace of set-theoretic classes and
functions, and also since it will be needed to represent the Kestrel
Institute's Specware system (in the plans), which, as you know, is based on
category theory -- here we will need to add a namespace for sheaves. There
are currently about 170 terms in the Category Theory Ontology. When the
base-line terminology for category theory is complete, there may be over 250
terms. I expect that eventually the Category Theory Ontology will grow to
contain thousands of terms. The terms of the IFF Category Theory Ontology
are partitioned into the following sub-namespaces (again with inclusion
indicated by the dot notation): (GPH) for large (directed) graphs, (GPH.MOR)
for graph morphisms, (CAT) for categories, (FUNC) for functors, (NAT) for
natural transformations, (ADJ) for adjunctions, (MND) for monads and monad
morphisms (handles equational presentations and data structures such as
stacks, trees, s-expressions and lists), (MND.ALG) for algebras and
freeness, (COL) for colimits in categories, both finite and general, with
initial objects, (COL.PRD) for binary coproducts, (COL.COEQU) for
coequalizers, and (COL.PSH) for pushouts.
o The IFF Foundation Ontology version 2.0 [to be submitted later] will
contain terminology and axioms for (1) the core namespace of classes and
functions, (2) the IFF Category Theory (sub)Ontology, and (3) the IFF Model
Theory (sub)Ontology. The IFF Model Theory Ontology will contain namespaces
for sets, small relations, small classifications, spans and hypergraphs,
models, and 1st-order interpretations. It is planned that later versions of
the IFF Foundation Ontology [versions 3.0 etc.] will incorporate namespaces
for limits, Kan extensions, classifications, concept lattices, topoi and
fibrations.
Robert E. Kent
rekent@ontologos.org