Re: SUO: Classification Ontology
All,
A very useful generic classification in the KIF Classification Ontology
represents the *powerset construction*. Here, as usual, sets are represented
as unary KIF predicates with membership determined by predication. Let '?p'
be an arbitrary predicate (set). Let '(power ?p)' represent the powerset
classification of '?p'.
(UnaryFunction power)
(forall (?p ?c)
(=> (= (power ?p) ?c)
(and (UnaryRelation ?p) (Classification ?c))))
The components of the classification '(power ?p)' are defined as follows.
An instance of the classification '(power ?p)' is a member of the "set"
'?p'; that is, an instance that '?p' predicates to true.
(forall (?p ?i)
(<=> ((inst (power ?p)) ?i)
(?p ?i)))
A type of the classification '(power ?p)' is a unary KIF predicate '?q' that
is contained in '?p' (see the 'subRelation' KIF relation in the Bootstrap
Ontology [http://grouper.ieee.org/groups/ltsc/logs/ontology/msg00471.html]).
(forall (?p ?q)
(<=> ((typ (power ?p)) ?q)
(subRelation ?q ?p)))
The incidence relation of the classification '(power ?p)' represents
(sub)set membership.
(forall (?p ?i ?q)
(<=> ((|= (Power ?p)) ?i ?q)
(and (subRelation q p) (q i))))
__________
It is a standard fact in Information Flow that from any classification '?c'
there is a *canonical extent infomorphism* to the power classification of
the instance set. This canonical infomorphism 'eta_c : c -->
power(inst(c))', denoted 'eta' since it is the unit of a functorial
adjunction, has the following KIF definition (here we use KIF
classifications in functional form).
(UnaryFunction eta)
(forall (?c ?f)
(=> (= (eta ?c) ?f)
(and (Classification ?c) (Infomorphism ?f))))
The source classification is the given classification.
(forall (?c) (= (src (eta ?c)) ?c))
The target classification is the power classification on the instance set.
(forall (?c) (= (tgt (eta ?c)) (power (inst ?c))))
The instance function is the identity function on instances.
(forall (?c ?i) (= (instFn (eta ?c) ?i) ?i))
The type function is the extent function on types.
(forall (?c ?t) (= (typFn (eta ?c) ?t) (ext ?c ?t)))
Robert E. Kent
rekent@ontologos.org
----- Original Message -----
From: "Robert E. Kent" <rekent@ontologos.org>
To: "Michael Uschold" <mfu@redwood.rt.cs.boeing.com>
Cc: "SUO" <standard-upper-ontology@ieee.org>
Sent: Friday, January 19, 2001 4:09 PM
Subject: Re: SUO: Classification Ontology
> Hi Mike,
>
> I agree. I have ongoing work on the Information Flow Framework (IFF). What
I
> sent was an extraction from the appendix of an unpublished paper of mine
on
> a "Classification Metatheory." I will try to send a more completely
> annotated document later. As a stopgap let me send the basic part of this
> appendix -- the part without the colimit representation. Although this
also
> is a bit terse, perhaps it will suffice in the meantime.
>
> Robert E. Kent
> rekent@ontologos.org
>
>
> ----- Original Message -----
> From: "Michael Uschold" <mfu@redwood.rt.cs.boeing.com>
> To: <rekent@ontologos.org>; <standard-upper-ontology@ieee.org>
> Sent: Thursday, January 18, 2001 5:24 PM
> Subject: Re: SUO: Classification Ontology
>
>
> >
> > Robert,
> >
> > It would be helpful to augment Kif-ese with English documentation
> > indicating what is going on. In my opinion, this is more important
> > than the KIF - in communicating.
> >
> > Mike
>