Re: Higher-order KIF & CGs
fritz@rodin.wustl.edu (Fritz Lehmann)
Reply-To: cg@cs.umn.edu
Date: Mon, 1 Nov 93 01:16:17 CST
From: fritz@rodin.wustl.edu (Fritz Lehmann)
Message-id: <9311010716.AA28631@rodin.wustl.edu>
To: phayes@cs.uiuc.edu
Subject: Re: Higher-order KIF & CGs
Cc: boley@dfki.uni-kl.de, cg@cs.umn.edu, interlingua@isi.edu
Dear Pat Hayes:
Discussing logic-order for KIF may be moot -- I don't know to
what degree KIF is open to change. On one hand the initiators of
KIF have pretty much settled on a first-order logic in LISP syntax.
On the other hand the very few attempted "users" of KIF have
squawked about its shortcomings and there have been no public
responses (on this INTERLINGUA email list at least) nor announced
corrective modifications in the language. Some Conceptual Graphs
people (like Guy Mineau) have extended CGs to higher-order a la
Gruber's Ontolingua, but I believe they have been limited to Sowa's
(apparently uninterpreted) reifying of predicates/relations into
individuals.
You've raised pure mathematical concerns about using higher-
order logic as a basis for an interlingua. I am concerned with
practical, finite transmission of knowledge and concept-systems
between real-world knowledge bases. This means that although human
readablitiy may be a low priority, feasibility of expression
("machine elegance") is a high priority. That's what higher-order
logic is good at. The fact that some construct may be reducible to
a first-order semantics using, say, an equivalent countable number
of first-order sentences (running over some available vocabulary)
may be of interest to the mathematical logician but if this requires
a corresponding effort in pure KIF then KIF fails. If every mention
of 100 senators required (as in first-order logic) 4,950 explicit
inequality statements between senators, that too would be a failure.
So if there is some ingenious but far-fetched reduction to FOL, then
_serious_ "syntactic sugar" is essential in the basic language
definition. If not, then we need the real higher-order model-
theoretic semantics. I wonder how broadly the epithet "sugar" may
be construed. If one "sugar" sentence substitutes for an infinite
(or indefinite or even intractably high) number of pure KIF/CG base
sentences, I don't think I'll call it "sugar" any more. That's
protein. Certainly such constructs need to be included in the "base
model" of any useful interlingua.
>> Thanks for describing to me the reduction of
>>equality-definition to First-Order via a finite schema
>>made of "Relation-symbol X Argument-place" instances,
>>depending on a finite vocabulary of available
>>relation-symbols. This seems like an unappealing
>>kludge which nonetheless works for some systems.
>Well it might not be very attractive, but it always works, and its the
>'standard' way to axiomatise equality in first order. Of course one can
>always summarise it in a schema (Leibnitz law) to make it look neater, but
>that still doesnt take one even to second-order order logic, since this
>schema is always equivalent to a finite set of its instances.
Pat, I don't know that it would "always work" for KIF since
KIF 3.0 allows an indefinite number of argument-places for a single
relation. A relation need not have fixed "rank" or "arity" so
"Relation X Argument-place" is not defined. Incidentally, I commend
KIF for this excellent poly-arity feature which is a big improvement
over Relational and Universal Algebra. It was adapted from LISP
constructions like (AND X Y Z W Q) where the number of conjoined
arguments is indefinite. Its usefulness is not restricted to
commutative/symmetric operators/relations: consider (CYCLE X Y Z W
Q) where the arguments are arrows drawn on a map. Also I think this
means that my earlier suggestion for the model-theory, that the
domain be "closed under direct product," needs to be modified to
"closed under disjoint unions of direct products."
>Heres why beta-reduction is so different.
> [explanation omitted]
>The equality schema is a
>convenient way of writing an essentially first-order intuition, but
>lambda-conversion is fundamentally beyond first-order quantification
>machinery.
Good. If beta-reduction of a lambda sentence has use in the
practical world, then this is just another reason for using a true
higher-order Krep language. I won't accede to your "essentially
first-order" above for equality since, in your schema-method, a
happenstance feature of _our_ syntax (finite vocabulary) determines
a real feature of the _world's_ semantics (identity of differently
qualified individuals). I'd rather say that individual
equality/identity is essentially higher-order, but representable by
a first-order schema kludge in systems with fixed finite
vocabularies and arities. [A class identity like the identity in
geometry of "equiangular triangles" and "equilateral triangles" has
nothing to do with our finite vocabularies.]
>>an infinite zoo of these
>>relation-symbols springs up.
>> . . .Forms are: a; b;
>>R(a,b); R'(a,R); R''(b,R,R'); etc.
>While I agree that it often seems natural
>to use R' and even sometimes R'', can you find a singe plausible excuse for
>R''', let alone R'..(50)..', say? I'm bothered by the way that letting
>recursion loose creates so many wildly implausible schemes when we really
>only wanted three, or maybe two, of them. Maybe recursion was a little too
>strong a tool to use?
I haven't considered 50 levels, but I've thought about: when
is it fruitless to consider more levels? R''' is indeed used: in
category theory, one R''' is to R as the role of an object in a
morphism is to a natural transformation. This reminds me of a maxim
of mine: the smarter you are, the higher the order of your logic.
Category theorists pride themselves on proofs using natural
transformations as opposed to getting the same result using
functors, or, worse, (ugh) sets of actual morphisms. I don't know
whether they've ascended beyond natural transformations of functors
of morphisms of objects, but I suspect so. The limit in the
comprehensible number of levels appears to be a matter of
unfortunate human mental limitation (which can be overcome -- with
difficulty!) rather than a fundamental barrier. In precisely the
same vein, Banach said "Good mathematicians see analogies between
theorems or theories. The very best ones see analogies between
analogies."
Similarly, I vaguely recall that Ontek, Inc.'s manufacturing
ontology system (a competitor of CYC created with the advice of
Peter Simons and other ontological philosophers) uses 4th-order
predicates. Perhaps they would not like to be stuck with a merely
first-order communication language.
>... once one has all the relation and
>function-substitution instances, further instantiation (eg over the
>relevant Herbrand universe) is just ordinary first-order.
>(I know that such 1PC theories of the integers, say, have nonstandard
>models. My attitude is: tough, thats the way life is! If one had
>uncomputable resources available, one could eliminate these nonstandard
>models. But one doesnt.)
That's real dedication to first-order-ism -- like a dog which
loves its leash. I don't know if even Martin Davis, who always
lobbies for first-order-ism, would go so far. If real-world users
were told that KIF or Conceptual Graphs required them to have
mysterious nonstandard numbers "outside" the real number line,
they'd rebel. (They may not appreciate that the reals are just
"dust" with plenty of room for nonstandard infinitesimals!) In
truth, for interlingua purposes, we should take numbers as
indefinable primitives: no Peano, no Princ.Math., no Goedel, no
nuttin. I don't see what "uncomputable resources" has to do with
purely formal semantics -- I gather from your whole discussion that
model-theoretic semantics is provided for an interlingua only to be
clear about what is meant in the abstract, without any assumption
that we actually have to be able to compute every underlying
Tarskian structure. We are not necessarily talking about
_computation_ at all, just a communiction language with formal
model-theoretic semantics. We can eliminate nonstandard numbers by
(n-order) fiat.
>My intuition is that while first-order quantification can be conceptualised
>as shorthand for an infinite, or unbounded, conjunction, and has a certain
>simplicity that it inherits from this intuition, higher-order
>quantification unfortunately cant be thought of in this comfortable way.
>This isnt obvious, and indeed was discovered this century, but its true.
>The ordinary intuitions about quantification just don't extend past first
>order. Thats why I am always suspicious that when someone tells me they
>want higher-order quantifiers, they really mean first-order with
>higher-order sugar on them. Im all in favor of the sugar, of course, for
>languages that people have to use (contrast KIF), provided one doesnt
>forget what one is really eating.
Not just "people ...(contrast KIF)." Machines need "sugar"
too, given your broad (logician's) definition of sugar -- see my
comment above re "machine elegance".
You allude nebulously to the pitfalls of true higher-order
logic, but I suspect these turn out to be either A. loss of
completeness and compactness, which are practically dispensable, or
B. genuine but in fact desirable changes in semantics. You say:
>Well, decideablity yes; but higher-order, taken seriously, takes us way
>beyond that: completeness is impossible. Bear in mind what that really
>means: that the set of truths is *uncomputable*. To claim that an
>implemented system is based on a semantics relative to which computability
>is provably impossible, seems to me to be just wishful thinking.
I repeat my original comments to the INTERLINGUA list:
"The usual objections to higher-order logic are that it is
undecidable, uncompact, lacks the 0-1 property, etc. These are
extraneous theoretical matters . . . They have no practical
importance for transmission of descriptions of real-world entities.
. . . We need to transmit finite taxonomies and descriptions of
real-world things and laws and relations, in large but finite
domains, ideally with the full (logical) expressiveness of very
careful and precise natural language. . . . It's not enough to say
"I like my logic to have formal completeness" -- demonstrate the
practical penalty of incompleteness (in real world AI communication
among our finite computers) or what ever else ails you about n-order
logic."
No-one has yet made the case that formal completeness has any
practical importance for communicating knowledge systems. Give us
REAL EXAMPLES of trouble caused by incompleteness. Incompleteness
arises for example from the ability of a language to predicate a
number which "corresponds" to the sentence doing the predicating.
Or to a Turing Machine unknowingly describing itself. Skipping
technicalities -- only a tiny proportion of the sentences in an
undecidable language (or programs in a Turing Machine) are
interpretable as self-referential and hence undecidable. [I don't
necessarily mean this asymptotically.] The shortest undecidable
sentence (program) is normally extremely long. It seems unlikely
ever to be encountered in AI or Knowledge-base communication, unless
by design. Can you clarify in plain, practical terms why
completeness is really important for communicating Krep systems?
(If you really think so.) You say "the set of truths is
*uncomputable*" Yes, but so what?
>> At present, KIF and CGs are unable even to
>>express -- with semantics -- Peirce's (or
>>Leibniz's) basic sentence: "Given any two things,
>>there is some character which one posseses and the
>>other does not."
>Well, they can say this, but only if one provides a theory of what
>'characters' are. And that seems quite a reasonable requirement. Claiming
>that you can say this in higher-order means that you are assuming that the
>logic has this notion somehow built into it. Even that seems reasonable
>until one knows about higher-order incompleteness and so forth, at which
>point I tend to balk, and ask where the confidence comes from that one
>really has captured this uncapturable semantics?
I think it's perfectly clear what "character" means here; it
means predicate. It asserts the existence of some predicate of an
individual, so it's second-order. Current KIF/CG can't say it (with
meaningful formal semantics). The sentence is in fact central to
descriptions of relational databases. Your dire warning of "higher-
order incompleteness and so forth" seems again like a shibboleth.
This just one of umpteen potentially useful higher-order examples
one could think of. Here's another: "All monotonic functions of 42
have positive values." Not very exotic -- but can anyone express it
correctly in KIF? Or in Conceptual Graphs based on Sowa's existing
phi-operator?
>Nonmon can be first order, thats orthogonal. The reason for taking
>nonmon seriously is that there is ample evidence that people want to use
>it, and it really *can't* be reduced to monotonic first-order logic.
Yes it's orthogonal. (Digressing hopelessly, I know of no
evidence whatsoever that "people want to use" nonmonotonic logics.
They want to deal with conflicting information; since when do they
demand new logics? Admittedly there are plenty of people around who
want to _invent_ new logics. Things that belong in the deep
theory/ontology are crammed into these "logics". But I don't want
to talk about this can of worms here. One can at a time.)
At first you seemed to say, as I do, that being merely first-
order might be a drawback of KIF or CGs. Later you've been citing
the familiar comforts of first-order from a mathematical logician's
point of view. Theoretical underpinnings should be basically sound,
but our knowledge-sharing purposes demand that practically useful
expressiveness comes before those theoretical concerns and
preferences of mathematical logicians which in practice turn out to
be irrelevant.
Yours truly, Fritz Lehmann
4282 Sandburg, Irvine, CA 92715 714-733-0566 fritz@rodin.wustl.edu
=====================================================================