Higher-order KIF and Conceptual Graphs

Date: Fri, 03 Dec 1993 10:02:16 -0400 (EDT)
From: FWLIV@delphi.com
Subject: Higher-order KIF and Conceptual Graphs
To: interlingua@ISI.EDU, boley@dfki.uni-kl.de
Message-id: <01H61EPH75PE92000I@delphi.com>
X-Vms-To: INTERNET"interlingua@isi.edu,cg@cs.un mn.edu,boley@dfki.uni-kl.de"
Mime-Version: 1.0
Content-Transfer-Encoding: 7BIT

Dear Tom Gruber:                        Gruber@HPP.Stanford.edu

	No-one disputes that KIF has function and relation objects. 
The "logic order" issue is about the semantics of quantification
over them --- whether it's based on "weakly" (actually First-
Order) vs. "strongly" higher-order logic.  The former allows
quantification only over a specified set (based on a currently
available vocabulary) of relation-symbols, whereas the latter
can genuinely quantify over all relations irrespective of the
particular currently available vocabulary.  I listed all
examples mentioned in this stream, expressly including some
"weakly" (i.e. KIF if it's FO) definable, and some not.  In your
last message to these email lists you worked out the first page
of my examples, but these were not the proved cases requiring
strongly higher-order semantics, which were mostly on the last

	Although you are at the core of the Knowledge Sharing
Effort, and probably KIF's main user, you mention "KIF, which I
am told is first order."  The rest of us are in much the same
position, having constructs like "(relation ?r) ... (forall ?r
(r? x?))" which looks higher-order but which we are "told is
first order".  Your examples in KIF with "forall ?r"s and the
implict foralls in KIF rules with "=> ?r ..." do nothing to
address the issue of what relations these quantifications
actually cover.

	I'll curtail my tenaciousness on this; Pat Hayes and others
and I have covered the issue at length, an issue I doubt many on
these email lists had known about before, and we cited
references.  There are certainly: A. higher-order concepts of
practical importance for knowledge-bases and AI, and B. concepts
which are only strongly-higher-order definable.  Where A and B
overlap, there is a problem for KIF.  For Conceptual Graphs,
John Sowa has already addressed the overlap a bit: he has now
departed from FOL by (wisely, I think) including natural numbers
as primitives along with a "cardinality" function from a set to
a number.   Using these he defined "connected" and "finite"
(which are not First-Order-definable).  A type lattice on
differentia graphs with CG "actors" would require a further
departure.  I'm grateful to Sowa for recommending Gordon &
Melham's "HOL" book, which as far as I can tell does things
right.  (It includes beta-reduction and if there's "First-Order-
ism" hidden in there, I haven't found it yet.)  One could do
knowledge interchange using the implemented, fully formalized,
typed, higher-order, ML-based "HOL" language itself.

	Still, Tom, your long message deserves response.  Those who
find this (foundational rather than notational) discussion
pointless, stop reading now -- and use your kill file!

>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.

	Yes.  Pat's description of our big difference was correct (if
applied to knowledge interchange rather than Krep in general), and
I look to interchange-language semantics for unambiguous
communication rather than for determining the whole of "meaning"
for an agent.  In most domains every description is only an
approximation.  There will indeed be predicates like Pat's "VERY-
BIG" example.  In practical knowledge interchange there will
always be part of the language (in fact most) which gets its
meaning from outside the formalism.  This is far short of Pat's
vision of "grounding" all meaning with a complete formal

>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...".

	Yes, assuming KIF's "higher-order" relations are actually
First-Order.  Not only "for all relations..." but also "there
exists a relation..." is affected.

>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.

	There's more to Krep than comparing databases.  In particular,
very different ontologies need to be integrated; one may be a
straightforward finite database and the other a highly abstract
domain.  A CAD database may need to exploit and interact with an
abstract axiomatization of geometry and perhaps a graph-theory
concept system.  The latter have infinite "spaces" of predicates and
relations, some of which are undefinable in First-Order (called
"strongly higher-order" in my updated list of examples with
references).  An integrator will need to quantify over them all, to
correctly define things like identity of triangle objects, etc. (see

> ...the
>semantic account for KIF (by which two moderately educated humans
>might agree when A implies B)...

	When the relatively uneducated (the users) rely on the
moderately educated (the AI people) to correctly implement
concepts well understood only by the very highly educated (the
relevant mathematicians), like higher-order model-theoretic
semantics, caution is advisable.  This applies especially in order
to correctly "agree when A implies B".

>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.

	This is wrong because the sentence nowhere states that
Aristotle is a philosopher (he may lack their vices), so
inheritance is not involved.  Your phrase "any property P" is
higher-order and a "(forall ?p)" has to be added if your KIF
implication "=>" is to apply to more than just the one predicate
"p".  My formalization was "AP( (Virtue(P) & Ax(Philosopher(x) ->
P(x))) -> P(Aristotle) )".  Granted, this is easily expressible in
KIF with a "(forall ?p)" but the question of what predicates
"forall ?p" actually covers remains unresolved.

>>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

	Yes, this does it.  Of course variables like ?r1 and ?r2
which appear in a KIF implication without a preceding quantifier
are deemed to be universally quantified (page 22 of KIF 3.0
Manual), so there are implicit "forall"s and again the issue (of
what is quantified over) is unresolved.

>>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.

	I use IS-A for AKO (subtype) as opposed to instance-of.  Both
are easily expressed in KIF, subject to my comments on examples 1
and 2.

>>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)))))

	Again, "?child-relation" and "?parent-relation" are implicitly
quantified over, so the logic-order question remains.  [The 
"permuted" deals with relational symmetries.  Tuples are sequences
in which every argument position is distinguishable, so an n-adic
relation with some symmetries among its (indistinguishable)
arguments will be repeated in the relation as multiple tuples with
the positions of symmetric (but somehow distinguished or named)
arguments permuted.  Assuming this, your definition handles it.]

>>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?

	Of course if equality is truly primitive it needn't be
defined at all.  But you mention "by substitution" (of "all" P's
of course); the ability to substitute is exactly what this
definition (Leibniz's) implies.  "AP" means (forall ?p).  You
kindly didn't point out my egregious error of including the "Ax,y"
(which effectively limits the universe to one kind of object!); it
belongs to the left of the whole definition.  I corrected this in
the updated list of examples.

	This equality business is serious in Krep practice.  It is by
no means obvious when two objects in an ontology are "the same
object".  This often needs to be formalized.  In purest unlabeled
graph theory, for example, two graphs are the same if they're
isomorphic; in fact TWO such graphs cannot be isomorphic -- they
are the same graph.  Some geometry systems identify congruent
triangles (even if reflected), yet a CAD system has to distinguish
them as separate objects.  In manufacturing, "a part" may or may
not be one physical object in the world; it may be only one object
with respect to the device it's part of, but have many
counterparts in identical devices (the ontology may well not have
"available vocabulary" to distinguish it from these others, in a
FO system).  This issue is closely related to my examples 25 and

>>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))

	Again, both ?binary-relation and ?f are implicitly
universally quantified here.  If KIF is only First-Order, then
these fail to cover all of the desired functions (unless certain-
kind-of-function happens to mean "first-order-definable-function"
or a subset of that!).

>>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.

	The last definition seems to do it for a fixed-arity dyadic
relation ?r.  Perhaps you could handle poly-arity relations too. 
I mentioned this and several related cases in connection with C.
S. Peirce's "hypostatic abstraction" of relations into individuals
after Mike Genesereth had remarked that no such relation as r'
exists.  The connection of these examples to logic-order is a
little different from the other examples.  Having r-prime itself
as a relation now recursively creates an infinite number of
relations as soon as one ?r is asserted.   Consider that (kappa
(?z ?r) (r-prime ?z ?r)) applies to itself, etc.  I suggested that
the totality of such relations might be unreachable by First-Order
quantification on relations; Chris Menzel replied that
quantification with (First-Order) Henkin semantics would cover
them.  I'm not sure.  I guess it could reach the members of any
particular one, but I don't know that it can cover the recursive
closure of all of them.  Anyone have a good reference?

>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).

	I won't go into deep-case theory, which involves the
intension.  It's not NTH-DOMAIN but rather the "type" of the role
as opposed to the type of the participant. A particular set of r-
prime relations (as above) shares with others certain features in
common.  This induces a relational hierarchy combining the methods
of examples 4 and 7..  Thus a participant in a relation has a
meaningful "role" in the relation, which role has qualities in
common with similar roles in other distinct relations.  By this
you can generate AGENT, VICTIM, SPATIAL-PARTICIPANT and similar
semantic "thematic" roles used in linguistics and semantic
networks.  KIF could do the extensional part of this using your
methods in 4 and 7.

>>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.

	Relations in KIF are based on sets.  Cylindric Algebras in
general (unlike some other abstract algebras) are not representable
as systems of sets if they include triadic relations.  (Only so-
called Regular Locally Finite Cylindric Set Algebras are.)  This was
proved by the mathematician Lyndon and Henkin, Monk, Tarski and
others for various classes of unrepresentable Cylindric Algebras. 
So I surmise that KIF would not be able to express them with correct
semantics.  (Brink & Schmidt's article in my "Semantic Networks"
collection showed that KL-ONE-type systems are notational variations
of well-known members of this general family of algebras.)

>  Say exactly what you mean, and I'll say it in KIF.

	A generous offer.  Things like "x is finite", "x is a
natural number" "x is connected" and all the only-strongly-
higher-order-definable things can be said in KIF, but I don't
see how the formal semantics will be correct if KIF is First-
Order.  You can say it in KIF, but it won't be exactly what I
mean.  Fortunately I'm unwilling to say exactly what I mean, if
it means I have to formalize in higher-order logic the 58
examples I listed.  I think I've done enough on email to alert
the KIF and CG communities to the logic-order issue.

                         Yours truly, Fritz Lehmann
4282 Sandburg, Irvine, CA 92715 USA    714-733-0566