Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Posted-Date: Thu, 26 Aug 93 07:14:06 PDT
Message-Id: <199308261414.AA00558@aerospace.aero.org>
Date: Thu, 26 Aug 93 07:14:06 PDT
From: cal@aero.org
To: info-hol@dworshak.cs.uidaho.edu
Subject: Computing in a Theorem Prover is Silly


I have been following this mailing list and others for some time, watching how
difficult it is to do simple proofs with most automatic theorem provers.  It
seems to me that part of the reason is that, while there is a large body of
standard notation in mathematics, there is no standard notation for
manipulation of expressions in these other notations, and that is one of the
main computing steps of a theorem prover.  I was moved to comment on the
proposals about adding numerals to HOL because therein lies a very dangerous
area with which I am familiar.

One of the failings of almost all computer systems is their inability to
combine disparate programming paradigms.  This shows up in the context of
automatic theorem provers by trying to do computation with the logical
framework (in the worst cases, using the Peano axioms directly to multiply
integers in a rule-based system!).  Of course, in some cases computation is
exactly the subject of the logical analysis, not part of the logical analysis,
and then you need to deal with it directly, without having to worry about such
difficulties as dealing with overflows and round-off in a logical framework.

A more general difficulty with adding new capabilities (of any kind) to most
computer systems is that there is no support within the system for diversity,
so the very most clever implementors either map the desired features or
functionality onto a set of not-quite-appropriate pieces within the system, or
they add on a new set of pieces that are somewhat inconsistent in spirit, if
not in operation, with the rest (the not-very-clever implementors of some
systems I have seen have done amazing things in this regard, but that is not
the problem here).

Anyway, this note is primarily a warning about the long-term future of HOL.
Either drop the idea of adding a new kind of thing in the system, and do
number stuff the old way (which I personally don't like very much, because
taking "less than one minute" to multiply two four digit numbers on a Sun SS10
appalls me, since I assume that less than one minute amounts to almost one
minute, and I can do it that fast by hand), or start to design a completely
new architecture that provides the infrastructure necessary to combine very
different computational resources and make effective use of them.

Otherwise, you run the risk of evolving HOL into a dinosaur, since using any
fixed architecture for more and more diverse kinds of functions will
eventually run up against a fundamental complexity limit that depends on the
scope and flexibility of that architecture, and unless the architecture itself
has been designed for extensibility in certain ways, that limit will be
reached much sooner than you want.

I welcome further discussion (flames to /dev/null, please).

Christopher Landauer

P.S. Credibility check (and a little bit of advertising 8-)) : my research
area is model integration in heterogeneous computer system environments, and
we have been working to determine the architecture and software infrastructure
necessary to support integration among disparate computational resources.  We
have no definitive answer yet, but have published widely on the kinds of
features required.  The approach we have been developing for the last four
years applies to computer systems in many application areas, as the references
below show (all of the papers cited below and almost all of our other papers
are available as postscript files through E-mail, or on paper through
SnailMail).  My somewhat intemperate comments on the QED mailing list
(qed@mcs.anl.gov) reflect these opinions also, and even include some
description of the kinds of features I think are required for large theorem
provers.

For example, see [1] below for our view of the basic problem and the
principles of our approach, [2] for a discussion of how our approach might
apply to very large simulation programs, [3] for a fairly recent description
of the architecture we believe is necessary, and [4] for a discussion of how
our approach might apply to computer systems that support complex system
engineering problems.

[1] Kirstie L. Bellman, ``An Approach to Integrating and Creating Flexible
Software Environments Supporting the Design of Complex Systems'', pp.
1101-1105 in Proceedings of WSC '91: The 1991 Winter Simulation Conference,
8-11 December 1991, Phoenix, Arizona (1991); revised version in Proceedings of
the Artificial Intelligence in Logistics Meeting, 8-10 March 1993,
Williamsburg, Va., American Defense Preparedness Association (1993)

[2] Christopher Landauer, Kirstie Bellman, ``Integrated Simulation
Environments'' (invited paper), Proceedings of DARPA Variable Resolution
Modeling Conference, 5-6 May 1992, Herndon, Virginia, Conference Proceedings
CF-103-DARPA, published by RAND (March 1993); shortened version in Proceedings
of the Artificial Intelligence in Logistics Meeting, 8-10 March 1993,
Williamsburg, Va., American Defense Preparedness Association (1993)

[3] Christopher Landauer, Kirstie L. Bellman, ``The Role of Self-Referential
Logics in a Software Architecture Using Wrappings'', Proceedings of ISS '93:
the 3rd Irvine Software Symposium, 30 April 1993, U.C. Irvine, California
(1993)

[4] Christopher Landauer, Kirstie L. Bellman, April Gillam, ``Software
Infrastructure for System Engineering Support'', Proceedings AAAI '93 Workshop
on Artificial Intelligence for Software Engineering, 12 July 1993, Washington,
D.C. (1993)