Re: Decidability
Brandon,
Your note contains many interrelated comments.
I completely agree with some of them, but I
would add qualifications to the others.
BB>... I would say that decidability is not something
> that should be sought at all cost. In fact it seems
> likely that any language sufficient to represent
> anything like the richness of human thought must be
> undecidable.
I agree. But I would add that the words "decidable"
and "undecidable" are inappropriate as modifiers of
a language. It is better to use them to characterize
problems.
As I said in my first note on this topic, all major
programming languages (C, Ada, Java, C++, C#, Perl,
Python, PHP, LISP, Prolog, etc.) allow programs to
be expressed whose termination is undecidable. But
nobody has ever said that property is a defect.
BB> However for processing and computation, decidability
> is undoubtedly of utmost importance -- much more
> important than the lower complexity boundaries,
> I would say.
Decidability of what? The language? A particular
problem? I certainly agree that there is no point in
letting a program run forever on a problem that will
never terminate. But what if you have a problem whose
termination is unknown? Perhaps you might want to let
the program run over the weekend to see what happens.
BB> The main problem is of course that if I am really dealing
> with a truly undecidable problem (such as computing
> entailment) in some language), I cannot even write an
> algorithm to do this. If I have a semi-decidable language,
> the situation is very slightly better because at least
> I have a test for positive cases -- but it's not much
> better, because the complexity of this test is not
> bounded by any function (so neither time nor memory
> requirement are bounded).
What are you saying? Do you mean that nobody should ever
try to prove a theorem before proving that it's provable?
Look at the _Principia Mathematica_. Whitehead and Russell
proved a lot of theorems without knowing anything about the
issues of undecidability, and it turns out that all their
theorems can be proved in a few seconds with modern theorem
provers. (Of course, there are probably many others that
they couldn't prove, but they never put them in their book.)
Look at the TPTP web site with thousands of problems for
theorem provers. Many of those problems are expressed
in full first-order logic, but they're provable. Why
should people give up before they try them?
I completely agree with the following:
BB> However, in many cases the complexity class does not
> directly affect the practical scalability. This is because
> complexity classes deal in worst cases. These typically
> arise quite rarely compared to the average case. Thus it
> may well be that a cubic algorithm works pretty well in
> almost all cases (and hence could be perfectly acceptable
> to web users who seem remarkably tolerant to systems that
> don't always work).
I would add that what's available on the web is so incomplete
and so rife with errors that users have much more serious
problems to worry about than the completeness or decidability
of their proof procedures.
BB> Thus the halting problem is solvable for "pure" Prolog
> programs (but not if one uses the various messy stuff
> that makes real programming possible).
No. You can simulate a Turing machine in pure Prolog, for
which the TM "tape" is expressed as a Prolog list. Then
you can give it a tape that expresses an undecidable
program. If you can't prove that the TM will halt, then
you can't prove that the Prolog simulation of it will halt.
BB> So the clever Prolog programmer does not tame the
> undecidable but rather steers around the exponential.
The Prolog programmer, like a programmer who uses any other
language, steers around both exponential and undecidable
problems. They've been doing that for over 50 years. Now
web programmers have to steer around polynomial problems.
And on the topic of Horn-clause logic, I would like to
recommend the following note I sent to these lists four
years ago. Note the discussion of how Bill Andersen and
his colleagues dealt with 5532 axioms taken from Cyc, of
which 84% of them could be expressed in hte Horn-clause
subset. I highly recommend that approach.
John Sowa
____________________________________________________________
Enrico,
I think we agree about the nature of completeness and its importance
for many kinds of reasoning. The differences in our points of view
seem to result from different assumptions about the relationships
between the ontology, the reasoning methods, and the kinds of problems
to be solved.
In your note, you seem to assume that there is one and only one
kind of reasoning method that can be used with a given ontology:
EF>Well, if you are a serious computer scientist, you should warn the
>military agency that they can not use the same ontology to achieve
>both tasks. You have to tell them that it is impossible to use your
>(incomplete) logic-based system to solve a problem and its dual
>at the same time.
This is a very different assumption from the Cyc philosophy that Fritz
Lehmann was discussing. Cyc has one very large ontology with many
different reasoning methods that can be used with it to solve different
kinds of problems. You seem to assume a different ontology for each
kind of reasoning method.
Since I'm not exactly sure what position either you or Fritz is
advocating, let me explain the position that I would recommend
for a large number of different kinds of problems:
1. Start with a large ontology stated in a very expressive version
of logic, which includes at a minimum all of first-order logic.
I would add metalevel and higher-order extensions for reasoning
about the first-order axioms, selecting which ones to use for a
given problem, and even revising the axioms in some cases.
2. At this point, I believe that Fritz and I would agree, but you are
probably waving your hands to protest that the reasoning methods
that would apply to such a logic would have to be intractable,
incomplete, undecidable, etc. I think that both Fritz and I would
agree with you. The difference is that Fritz says that he doesn't
care, but I care more than he does. My position is somewhere
between you and Fritz. I sympathize with your concerns, but I
believe that there are ways of dealing with them in a way that is
logically sound and with suitable guarantees to the users (the
military authorities in your example).
3. The point I want to emphasize is that intractability is not a
property of the logic, but a property of the problems you are
trying to solve. An NP-complete problem will be NP-complete
in any logic you use. Restricting the logic will not solve the
problem -- it will just make it impossible to state the problem.
Similarly, a polynomial-time problem is going to take polynomial
time in any logic. If you can solve it in polynomial time with
description logics or Horn-clause logics, a full FOL theorem
prover, such as Otter, will also solve it in polynomial time
(I will admit that a more restricted theorem prover may be able
to solve some problems faster, but Otter has a variety of methods
that it can choose for different problems. Even though it always
uses full FOL to state the problem, it can automatically choose
a more restricted method when it is suitable.)
4. There are many problems that require the full expressive power of
FOL but can be solved in polynomial time. An example is answering
an SQL query in terms of a relational database. The SQL query
language has the expressive power of FOL, but any SQL query
can be evaluated against a relational DB in polynomial time with
an exponent that is less than or equal to the maximum number of
quantifiers in the query. The world economy depends on such
problems being solved billions of times a day.
5. One approach that I highly recommend started with the Cyc KB,
which is probably the largest axiomatized KB ever developed.
The developers (Petersen, Andersen, and Engel, see ref. below)
used the full Cyc system to develop an application, but they
wanted to run it as a standalone application without using the
full power of Cyc. They developed tools that were able to extract
the 5,532 axioms they needed from the half million axioms of the
total Cyc system. Of those axioms, 4667 could be translated to
Horn-clause form, which they used as part of a deductive database
system. There were 875 axioms outside the Horn-clause subset;
instead of throwing them away, they used those axioms as database
constraints, which could be evaluated against their relational DB
in polynomial time (a constraint is simply a query whose answer is
required to be "yes"). See the full paper for more info.
6. Such examples illustrate my recommendation: use a large ontology
with axioms stated in a highly expressive logic and develop
automated tools that can extract different subsets of that ontology
that can be used for different kinds of problems with different
methods of reasoning. For those problems that can be solved with
description logics or Horn-clause logics, the automated tools can
extract the appropriate subset and translate it to the proper form.
But the same tools may be used to extract other subsets for other
purposes.
Bottom line: I don't believe in a one-size-fits-all version of logic.
Different problems may require different methods of reasoning with
logics of different expressive powers. But many different versions
of logic can be related to one another as subsets of a more expressive
logic, from which they can be extracted with the aid of appropriate
tools.
I also take exception to the following point:
EF>And for this, I don't mean two DIFFERENT tasks, but essentially
>the same task viewed from the positive and the negative point of view.
I don't regard the positive and negative views as "essentially the
same task." One of them may be well defined and bounded while the
other is open-ended and impossible to characterize. The set of all
cows is finite, but the set of all non-cows is completely undefined.
Following is the reference for point #5 above:
Peterson, Brian J., William A. Andersen, & Joshua Engel (1998)
"Knowledge bus: generating application-focused databases from large
ontologies", in Proc. 5th KRDB Workshop, Seattle, WA. Available from
http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-10/paper2.ps
John Sowa