Re: SUO: Re: Bootstrap Ontology
----- Original Message -----
From: "pat hayes" <phayes@ai.uwf.edu>
To: "Robert E. Kent" <rekent@ontologos.org>
Sent: Saturday, January 27, 2001 6:21 PM
Subject: Re: SUO: Re: Bootstrap Ontology
> >All, especially KIF experts,
> >
> >The Boot Ontology needs a Cartesian product unary predicate
> >'(productRelation ?p1 ?p2)' for any two given unary predicates '?p1' and
> >'?p2'. What follows is a candidate definition of this. Please check to
see
> >if this is correct.
>
> It is impossible to tell, since it uses undefined terminology
> ('double', notably. I assume that this is a predicate which
> characterises the set (?) of pairs, with 'first' and 'second' as the
> selector functions?)
Yes. This is some of the list terminology defined on the following page:
Knowledge Interchange Format
draft proposed American National Standard (dpANS)
NCITS.T2/98-004
[http://meta2.stanford.edu/kif/dpans.html#Lists]
Here is the definition.
(defrelation double (?l) :=
(exists (?x ?y) (= ?l (listof ?x ?y))))
(deffunction first (?l) :=
(if (= (listof ?x @items) ?l) ?x)
(deffunction last (?l) :=
(cond ((null ?l) bottom)
((null (rest ?l)) (first ?l))
(true (last (rest ?l)))))
> >__________
> >
> >The Cartesian product unary predicate is define as follows.
> >
> >(BinaryFunction productRelation)
> >
> >(forall (?p1 ?p2 ?p)
> > (=> (= (productRelation ?p1 ?p2) ?p)
> > (and (UnaryRelation ?p1) (UnaryRelation ?p2) (UnaryRelation ?p))))
>
> I presume this is intended to be something like a sort restriction?
Yes.
> If so, it doesnt really work in KIF.
Can you go into any more detail? I am very much interested in this kind of
restriction of KIF.
>SUO-KIF will have an explicit
> sorting extension; details available shortly, but you can get the
> flavor from the way your example would look:
>
> (SortOf productRelation ((UnaryRelation UnaryRelation) UnaryRelation) )
>
> ie the sort of 'productRelation' is a binary function from
> UnaryRelation x UnaryRelation to UnaryRelation. (The language will
> also permit more complex Boolean combinations to allow things like
> sort overloading and multiple inheritance.)
OK. Seems rather elaborate. Would this stuff be better placed in some
"mathematically-oriented" ontologies? I would prefer that an absolute
minimum be placed in core KIF and a core KIF ontology. What that minimum is,
is another question.
Again, can we not have some very basic sort-like ontologies where semantical
typing is defined? I will soon offer a KIF "ontology" for basic
category-theoretic notions where a kind of semantical typing is defined.
> SUO-KIF will also, by the way, allow terms (including variables) to
> occur in function and relation position, which means that your other
> axioms can be written more compactly without the explicit equalities
> in the antecedents:
>
> >(forall (?p1 ?p2 ?i ?i1)
> > (=> (= ((projectionFunction1 ?p1 ?p2) ?i) ?i1)
> > (and ((productRelation ?p1 ?p2) ?i) (?p1 ?i1))))
OK, but I think that I am already using this idea here. For example,
'((projectionFunction1 ?p1 ?p2) ?i)' uses the term '(projectionFunction1 ?p1
?p2)' in a unary relation position. And '(?p1 ?i1)' uses the variable '?p1'
in a unary relation position.
> (forall (?p1 ?p2 ?i)
> (?p1 ((projectionFunction1 ?p1 ?p2) ?i) )
This gets half of the typing, but the other half asserts that '?i' is of the
product type '(productRelation ?p1 ?p2)'.
In summary, I believe that a core (or bootstrap) KIF ontology is necessary.
But, there is still some question about what to put in this ontology. Right
now I am oriented towards placing in this the foundation assumptions
(restricted comprehension principle) made by Saunders Mac Lane on pages
21--24 in the text "Categories for the Working Mathematician": existience of
a universe (the set of all KIF objects), and formation of doubletons, pairs,
Cartesian product, power set, union, etc.
> ---------------------------------------------------------------------
> IHMC (850)434 8903 home
> 40 South Alcaniz St. (850)202 4416 office
> Pensacola, FL 32501 (850)202 4440 fax
> phayes@ai.uwf.edu
> http://www.coginst.uwf.edu/~phayes
>
Robert E. Kent
rekent@ontologos.org