Typed KIF

Tom Gruber <Gruber@sumex-aim.stanford.edu>
Message-id: <2903799733-3280429@KSL-Mac-69>
Date: Tue, 7 Jan 92  11:02:13 PST
From: Tom Gruber <Gruber@sumex-aim.stanford.edu>
To: interlingua@isi.edu
Subject: Typed KIF
In-reply-to: Msg of Tue, 07 Jan 92 09:06:34 PST from Robert MacGregor <macgreg@isi.edu>
> In general, the KIF current philosophy seems to be to make
> it easy to translate INTO KIF, at the expense of making
> it harder to translate OUT of KIF.  Inventing a stricter,
> and thus friendlier version of KIF, plus developing
> a (single) translator from full KIF into the restricted
> KIF, would reduce the effort required for a KR system
> to build a KIF interchange facility.

For about a year now we have been maintaining a translator from KIF
definitions into LOOM, Epikit, and a canonical KIF.  It's called
Ontolingua, and it was developed specifically to support ontologies
(sets of definitions).  The first things we did to to make translation
practical was (1) introduce second order relations for classes/types
and relation definitions.  (2) identify a subset of KIF that was
guaranteed translatable (issuing warnings at translation time if it
can't translate a form).  We have worked closely with Genesereth and
Fikes, and the effort has been a forcing function for some of the
design of KIF.  For example, the latest draft of KIF (in preparation)
will contain an axiomatization that unifies relations, functions, and
sets -- which will provide much of the foundation we had to invent for
defining ontologies.

Now that the issue of introducing types into the KIF has come up, I'd
like to raise three questions for this committee.  Each has to do with
the tradeoff between expressiveness and ease of translation.  The
answers are relevant to the activities of the SRKB working group.
We are concerned with defining shared ontologies, and need to
establish requirements for "shareable definitions" of relations, 
classes, functions, sets, and distinguished constants.

  1.  Types vs. second-order ontology.  Would it suffice to define a set of
second order relations for describing classes, relations, and
functions (e.g., subclass-of, instance-of, etc.).  Or, is it better to
include types as part of the interchange language?

  2. Class and relation hierarchies without definitions?  Does a
description of a class or relation that comprises only necessary
constraints have to be a definition?  In other words, if one put the
discussion of analytic truth and definitions in the context of
defining portable ontologies, what distinctions would matter?

  3. Polymorphism.  Can/should a definition of a relation or
function constant depend on the types of its arguments?  For example, 

  (defunction plus ($op1 $op2)
     (if (and (numberp $op1) (numberp $op2))
         (+ $op1 $op2)
         (if (and (setp $op1) (setp $op2))
             (union $op1 $op2))))

similarly for relations

 (defrelation greaterp ($arg1 $arg2)
    (=> (and (numberp $arg1) (numberp $arg2))
        (> $arg1 $arg2))
    (=> (and (setp $arg1) (setp $arg2))
        (> (cardinality $arg1) (cardinality $arg2))))

  3b. Would it be possible to define greaterp several times using
      defprimrelation, each with a different type to dispatch on?

Tom Gruber