Higher-order logic, tractability, and firstname.lastname@example.org
Date: Tue, 7 Jan 92 16:37:48 EST
To: email@example.com, firstname.lastname@example.org, email@example.com
Cc: firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com
Subject: Higher-order logic, tractability, and requirements
I want to endorse David McAllester's recommendations for getting
higher-order logic into KIF:
> Sounds interesting. Have you considered whether the subsets of
> higher order logic allow truly increased expressive power? For
> example, do they allow a definition of transitive closure? The Kl-ONE
> primitives I am aware of do not really extend the expressive power
> beyond that of first order logic. Why not simply allow
> arbitrary quantification over functions and predicates?
There are many reasons for using higher-order logic. One is just
to express things in a simpler way. For example, it is shorter and
easier to say subtype(DOG,ANIMAL) than to say
(Ax)(dog(x) -> animal(x)).
That is the KL-ONE and E-R style of second-order logic, where there
are no quantifiers at all. The quantifiers come in when you start
to describe how KL-ONE works. Then you have rules like the following:
(Ax)(Ay)(Az)((subtype(x,y) & subtype(y,z)) -> subtype(x,z)).
Here you have second-order rules that quantify over types. However,
these rules are the same for every application, so most KL-ONE-like
systems compile them (or write them) in procedural code for better
performance. But if we want to discuss the difference between
inheritance in KL-ONE and NIAM, we would like to compare axiomatized
theories of how the procedures in each of the systems work. We would
also need that kind of axiomatization if we want to write an interpreter
for such a system in another language or if we want to write the rules
for translating one system into another.
Those are special cases where the system developers implement all
the axioms that require higher-order quantification, and the knowledge
engineers who write applications use only second-order statements
without quantifiers. However, one can easily imagine more exciting
applications where the kn. engineers would have to write quantified
higher-order statements as well. That brings in the question of
tractability, as David mentioned in another note:
> This brings us back to the expressibility/tractability issue. Can I
> interpret your statement as saying that full higher order is avoided
> because of tractability issues? What position does (should)
> knowledge sharing standards take on the expressibility/tractability
> issue? I would think that the interlingua should be maximally expressive
> so that any data base can at least be expressed in the interlingua.
> For example, the interlingua should allow one to exactly express the
> Reimann hypothesis (suppose someone has a data base of mathematical
> Allowing the expression of arbitrary mathematics gets a little tricky,
> but a simple higher order logic would handle all of "ordinary" mathematics
> (including the Reimann hypothesis).
The question of tractability in the abstract is meaningless. You always
have to ask "for what purpose?" Consider, for example, first-order
1. If you want to do arbitrary theorem proving, almost any interesting
question is NP complete, taking exponential amounts of time.
2. But if all you want to do is to ask whether a given formula is
true about a given model, that can be answered in polynomial time
with maximum exponent equal to the number of quantifiers.
3. And if you have a database with indexes on the critical fields,
you can evaluate existential quantifiers in sublinear time.
4. But if all you want to do is to translate a formula from one
notation to another, the time is measured in milliseconds or less,
independent of the number of quantifiers or modal operators.
For the knowledge sharing effort, all of these purposes (and many
others) may be relevant for one application or another. All of
them should be supported.
This brings us to the point about requirements, which have been
mentioned from time to time, but have never been discussed in
detail. We can't really say what kinds of features must be
supported by the knowledge sharing effort until we have a clearly
defined set of requirements.
There is also a question of how many languages we need. Is it possible
to do everything with a single KIF? Must we have several languages,
such as KIF, KQML, KRSS, etc.? How are those languages related?
Can any of them be subsets or supersets of one another? What about
the Cyc distinction between an epistemic level (EL) vs. a heuristic
level (HL)? Do we use the same or different languages for the
different levels? Or do we use the same syntactic forms, but with
a changed vocabulary?
What about different notations, such as traditional predicate calculus,
LISP-like, conceptual graph-like, SQL-like, or even English-like?
Must every semantic feature be representable in every notation?
Without a clear-cut list of requirements, we may be arguing for or
against different features for totally unrelated reasons.