On Wed, 25 May 1994, you wrote:
> John,
>
> I would like to see the details of your Prolog-based meta theory.
I don't have a ready-made answer that would satisfy you, Bob. That is
because the projects for which we've used metatheory have had goals
different from QED, and we've concentrated on developing the aspects
we've needed. Let me explain.
Here we've had no difficulty taking conventional (ZFC) set theory as a
mathematical foundation. Our need for metatheory has been to do with
the formalisation of mathematics in a straightforward way (axiom schemes,
side conditions and so on) through to rapid prototyping of tools support.
Since logic is applied mathematics (my source for this was Abraham
Robinson, 1969) we have had no difficulty *in principle* with
taking set theory as the formalisation of the metatheory also. When
applying that principle in practice however, we've made the following
design decisions:
* We've noticed that ur-elements (essentially, `atoms' in Lisp or
Prolog parlance) are a considerable practical convenience in
many applications of set theory. A version of set theory
including them is easily justified by modelling in conventional
set theory. Hence we're working in set theory with ur-elements.
* To make the meta level as unobtrusive as possible at the user
interfaces of our tools, we've subsetted set theory for use as
a metatheory: no quantifiers, only a small fragment of the set-
theoretical universe (essentially finite, labelled, ordered trees).
This also simplifies tools support considerably. Obviously one
could then say we're no longer working in set theory. The point
is, the validation strategy is interpretation in set theory.
* To make the metatheory more immediately useful, we've introduced
as primitives into the metatheory, some application-specific
notations and recursive definition mechanisms which would ordinarily
be defined in set theory. For example some of the objects which
the metatheory is intended to reason about are designated as
object language variables. There's a predicate to recognise
them and a type of meta level variable which ranges over them.
However, I've saved the main point till last. A formal theory should
formalise both syntax and proof, but another useful notion of theory is:
a set of sentences from some formal syntax. In our theorem prover work
the object theories are formal and the meta level syntax is formal.
However, since the meta level is based on set theory and is currently being
used to write executable specifications rather than proofs, we have not
needed so far to formalise the meta level proof concept.
Well, that's a first approximation to the truth. To the extent that
reasoning in the metatheory is implemented by our extended Prolog (Qu-Prolog),
which is our theorem prover implementation language, there is a proof concept.
It has some nice ideas I think - e.g. there is support for evaluating
during unification the meta level operation of substitution for object
variables - but I don't claim Qu-Prolog proof concept meets the needs of
QED. A PhD student is working on a formal metatheory, but he's not done yet.
Bottom lines.
* I doubt I'm far from your position on metatheory. I need to know
more about FSO, but it sounds promising.
* I'm not pushing an alternative. Prolog, resolution, unification
etc. are techniques which can be used to support using a theory -
they don't solve the problem of choosing a theory.
* Although this does not meet your request Bob, anyone who wants
to see recent evidence of our work on Prolog-style support for
an executable meta level vocabulary, and an interactive theorem-
prover application, can ftp details of Qu-Prolog 3.2 and Ergo 4.0
from ftp.cs.uq.oz.au. Relevant files are:
/pub/SVRC/software.9p.tar.Z
/pub/SVRC/software.ergo.tar.Z
/pub/SVRC/techreports/tr93-18.ps.Z
The tech report is the Qu-Prolog 3.2 user manual, which considers
only differences from Sicstus Prolog. The Ergo file includes its
own user manual, both in report form and as on-line support. Both
pieces of software have been used nontrivially: Qu-Prolog to
implement Ergo, Ergo to support e.g. verification of MIPS 3000
assembly code. As both are currently under further development
the released versions are not supported. Anyone who has technical
questions about this software would best query Peter Robinson
(pjr@cs.uq.oz.au).
John