high order relations in first order KIF

Tom Gruber <Gruber@HPP.Stanford.EDU>
Full-Name: Tom Gruber
Message-id: <2963039528-2260159@KSL-Mac-69>
Date: Tue, 23 Nov 93  02:32:08 PST
From: Tom Gruber <Gruber@HPP.Stanford.EDU>
To: interlingua@ISI.EDU
Cc: cg@cs.umn.edu, boley@dfki.uni-kl.de
Subject: high order relations in first order KIF
In-reply-to: Msg <9311111425.AA10829@rodin.wustl.edu> from fritz@rodin.wustl.edu (Fritz Lehmann) 
References: <9311050935.AA03585@rodin.wustl.edu>,

--- Fritz Lehmann <9311050935.AA03585@rodin.wustl.edu>

> 	KIF and Conceptual Graphs now make no provision for
> higher-order concepts with any semantics at all.  Gruber's
> Ontolingua makes a stab at it, as do Boley's DRLHs.  We
> need relations among relations, relations between
> relations and their own arguments, functions of functions,
> and so on, not just relations among individuals. 

---  Tomas Uribe <9311091953.AA10690@Xenon.Stanford.EDU>

> Um, Chapter 8 of the KIF reference manual describes how functions
> and relations can be defined... Given these definitions, one can
> proceed to quantify over them, and thus define functions of functions,
> relations over relations, and so on (i.e., the "individuals" over
> which the functions and relations range over are functions and
> relations themselves).

--- Fritz Lehmann <9311092334.AA02203@rodin.wustl.edu>

> 	I don't understand how, after first defining a
> relation with kappa-abstraction, one can then predicate
> the "mixed-order" relations between it and its own
> arguments (though it may be possible).  If this should be
> obvious from reading the manual, I missed it.  I described
> the practical value of this in previous messages to the
> interlingua and Conceptual Graphs lists.

> 	My motivation for this is that I am exploring
> automated knowledge base integration, which has practical
> commercial value.  This means starting with two knowledge
> bases with very different concept-systems and taxonomies
> ("ontologies") and discovering automatically the
> correspondences (identities, inclusions and overlaps)
> between concepts (and relations) in one and those in the
> other, and then using these correspondences for combining
> the two into an integrated knowledge base.  Another use of
> the correspondences is automatic translation from one
> knowledge system to the other.  When the two systems
> "first meet," they mutually explore the highest, genuinely
> ontological, levels of their concept-systems in order to
> find some common ground for communication.  

My colleagues and I have been building ontologies, in KIF, to
facilitate the sharing and exchange of knowledge among computational
agents (real live ones, like Mathematica and ODE-based simulation
tools for modeling satellites).  This work falls in the pragmatic side
of Pat Hayes' dichotomy: i.e., the purpose of the ontology is to
facilitate communication and not to prescribe the cognitive structures
of the agents.  From this pragmatists point of view, the essential and
unique benefits of using KIF instead of conventional software
engineering specifications (e.g., application programmer interfaces)

  1. EXPRESSIVE POWER -- we want to say things using expressions
(e.g., math models of device behavior) not just passing numbers and
strings to a function.  The agents need to commit to a common
interpretation of the expressions.

  2.  DECLARATIVE SEMANTICS is good for HUMAN communication of a
specification because it is independent of programs, cultures, natural
languages, and lexical context.  In addition, if the semantics is
compositional, one can write tools to help one deal with complex

Early on in the ARPA Knowledge Sharing Effort, when we began to build
software tools for writing and translating ontologies in KIF, we found
it useful (necessary, it seemed) to have some facility to describe
relations and functions as things in the universe of discourse.  AND
SO THEY ARE: the KIF specification includes an ontology in which
relations are sets of tuples, and functions are just relations whose
last argument is determined by the others.  For example, there is a
KIF relation called RELATION, which holds for sets of tuples, defined
as follows:

(<=> (RELATION ?r)               ; ?r is a relation IFF
     (and (set ?r)               ; ?r is a set
          (forall ?t
            (=> (member ?t ?r)   ; ?t is a member of the set ?r
                (list ?t)))))    ; ?t is a tuple

Since then, we have extended this fundamental ontological commitment
with a simple theory of classes and instances (aka the frame
ontology).  The frame ontology consists almost entirely of relations
that predicate over other relations, and no definition requires the use
of metalinguistic quoting.  For example, CLASS is equated with
unary-relation, and INSTANCE-OF (IS-A) is defined as a "mixed order"
relation between a unary relation and some other entity (possibly a
relation itself).

(<=> (INSTANCE-OF ?individual ?class)
     (and (class ?class)
          (holds ?class ?individual)))

The complete theory is available in four languages on the ftp server
  ksl.stanford.edu: /pub/knowledge-sharing/ontologies/frame-ontology.*

All of this is defined axiomatically on top of KIF, which I am told is
first order.  The difference between KIF's higher-order relations and
a second order semantics, I gather, hinges on just what is being
quantified over when one says "for all relations...".

For pragmatic purposes such as those mentioned by Fritz Lehmann (e.g.,
comparing databases), I have never seen an example where one actually
needs to quantify over all the theoretically possible relations.  The
constraints of finite computation ensure that the set of relations of
interest will surely be describable in the finite vocabulary
(otherwise how could you even print out the answer?) and therefore
countable.  Of course this is understating the case: the set of named
relations in any implemented database (or concepts in a terminological
subsumption lattice) will be quite small.

So I was surprised to see such a tenacious plea for replacing the
semantic account for KIF (by which two moderately educated humans
might agree when A implies B) with something of Classical Higher
Order.   Just to convince myself, I worked out the first page of
examples on Lehmann's list.  I found them to be of two categories:
[Type K] you can easily represent the statement in KIF; or 
[Type X] you can't get two humans to agree on what the sentence means
by reading what was written in the email.  For a Type X example, 
I conjecture that elaboration of the specification (in declarative
text, no fair sending a program) either turns it into Type K or
demonstrates that the definition does not satisfy the pragmatic
objective of communicating meaning among humans.  

But let's see the evidence:

1. "Aristotle has all the virtues of a philosopher."

One man's virtue is another man's vice (type X).  If this example is
meant to suggest that property inheritance requires higher order
logic, it doesn't.  If (instance-of aristotle philosopher), then any
property P that is asserted of all philosophers applies to aristotle.
Taking classes to be unary relations, to assert a property of a class
is to write a rule of the form (=> (philosopher ?x) (p ?x)).  From the
definition of instance-of, it follows that (philosopher aristotle).
(p aristotle) holds by universal instantiation.

2. Patrick Winston's relation-between-relations semantic net
link [between the "left-of" and "right-of" relational links].

This depends what you want the relation-between-relations to mean.
Here's an example of a relation-between-relations that I assume can be
understood from its first-order definition:

  (<=> (INVERSE ?r1 ?r2)
       (and (binary-relation ?r1)
            (binary-relation ?r2)
       (<=> (holds ?r1 ?x ?y)
            (holds ?r2 ?y ?x))))

If you don't like HOLDS, you can do the same thing using sets of

3. The IS-A link in inheritance and subsumption hierarchies.
[as a relation or link, not a set of FO axioms]

IS-A is instance-of as defined above.

4. The relational IS-A/subsumption link in relational
hierarchies.  [some arguments may be permuted]

I don't undestand the "permuted" comment, but here is relational

(<=> (SUBRELATION-OF ?child-relation ?parent-relation)
     (and (instance-of ?child-relation relation)
          (instance-of ?parent-relation relation)
             (forall ?tuple
                (=> (member ?tuple ?child-relation)
                    (member ?tuple ?parent-relation)))))

5. The formal definition of individual identity or equality.
[As in "x = y  =def= Ax,y AP (P(x) iff P(y)).]

Equality is a primitive operator in KIF.  This is Type X again.  What
do you mean by "AP"?  If one takes equality as primitive, then by
substitution all the (<=> (P ?x) (P ?y)) axioms will be true.  What
else do you need in order to communicate the meaning of a knowledge
base full of P's and x's?

6. The assertion that, for a particular individual, all of a
certain kind of functions on that individual take a certain
kind of value.  [including recursively defined functions]

Here is the case for a specific function on a particular individual:

(<=> (VALUE-TYPE ?instance ?binary-relation ?type)
     (and (instance-of ?binary-relation binary-relation)
          (instance-of ?type class)
          (forall ?value
             (=> (holds ?binary-relation ?instance ?value)
                 (instance-of ?value ?type)))))

Using that, we can generalize to "all of a certain kind of functions":

(=> (certain-kind-of-function ?f)
    (value-type particular-individual ?f certain-kind-of-value))

7. The ability to refer to and predicate the relations which
exist between a given relation and its own arguments.  For
R(a,b), this yields R'(a,R); R''(b,R,R'); and infinitely more.

The following defines the function mapping a relation to the class of
all objects that are one of its arguments in one of its tuples.

(<=> (RELATION-UNIVERSE ?relation ?type-class)
     (and (relation ?relation)
          (class ?type-class)
          (forall (?x)
            (<=> (exists ?tuple
                     (and (member ?tuple ?relation)
                          (item ?x ?tuple)))
                     (instance-of ?x ?type-class)))))

With this vocabulary you can a define you favorite specialization of
"relations which exist between a given relation and its own
arguments".   So, if I follow the notation above, R'(a,R) would be

(<=> (r-prime ?x ?r)
     (instance-of ?x (relation-universe ?r)))
or perhaps order matters:
(<=> (r-prime ?x ?r)
     (exists ?y (holds ?r ?x ?y)))
and that is a special case of the frame-ontology's EXACT-DOMAIN.

8. Semantic "case relation" taxonomy links.

Type X.  If you can explain what this means using only email and no
references to literature I don't have time to read, I will write the
axioms in KIF.  If you mean "referring to the nth argument of a
relation tuple", that is trivial (see NTH-DOMAIN).

10. The inclusion ordering in cylindric algebras.

In the engineering math ontologies, we've axiomatized textbook
abstract algebra using the same sorts of second-order notation
described above.  Say exactly what you mean, and I'll say it in KIF.