I am currently comparing the systems IMPS, PVS and Larch with respect to
their facilities to perform proofs in abstract algebra. The major concern of
this is to find out if the objects of concern, e.g. groups, rings, etc.,
may be expressed as single theories or modules, respectively. That is, the carrier
of a group is expressed as a type, the operations as functions over that
type. This representation is suggested by the systems descriptions.
It allows to instantiate the theory of e.g. groups to, say, a type of
integers together with its functions 0, +, and - . An instantiation like
that would then produce the results showed on an abstract level about groups
automatically for the type of integers after we show that the type integer
meets the group axioms.
But, it is not directly possible to talk _about_ groups in formulas though
this is absolutly common in mathematics. It is not possible in this "theory"
representation unless we redefine the whole theory again as a predicate.
My question is now: Are there any other theorem proving systems which offer
an explicit theory notion and allow to do the described change of viewpoint
in a more elegant way?
Florian
To Florian Kammueller<Florian.Kammueller@cl.cam.ac.uk
Subject: Q:Systems for Algebraic/Structural Reasoning
Copy to: qed@mcs.anl.gov., zucker@maccs.dcss.mcmaster.ca
Eindhoven, 11 March 1996.
Dear Florian,
In your email of 7 March you inquire about formalism
that can handle theories and complex notions, like the
notion "group".
This is something we felt the need for in the Automath
project in the middle seventies. The name invented for the
notion was "telescope". A telescope is a sequence of typed
abstactors, where in each abstractors the type
can depend on the variables introduced by the preceding
abstractors of the sequence. The name "telescope" was chosen
since the old-fashioned optical telescope used to be built
as a sequence of segments sliding into one another.
J. Zucker used telescopes on a large scale when writing
an introduction into analysis in his own version of
Automath. Unfortunately this work remained unimplemented
and unpublished because of the lack of finatial support in
those days. A short description can be found in Zucker's paper
J. Zucker,
Formalization of classical mathematics in AUTOMATH,
Colloque International de Logique, Clermont-Ferrand,
In: Colloques Internationaux du Centre National de la
Recherche Scientifique, 249, (July 1975) pp 135-145.
My own work on telescopes was published much later:
N.G. de Bruijn. Telescopic mappings in typed lambda calculus.
Information and Computation, vol 91, 189-204 (1991).
In order to see the subject of this paper one might think
of an operator that attaches a ring to every abelian group.
It is a kind of mapping from the telescope "abelian group"
to the telescope "ring". The paper shows that such mappings
can be treated by a calculus that copies the lambda
calculus on a higher level, again with both abstraction and
application, very similar to what we have with ordinary
functions. For the connection with Zucker see p. 192 of
this paper.
For extensive information on the Automath project, see:
Selected Papers on Automath,
edited by R.P. Nederpelt, J.H. Geuvers and R.C. de Vrijer,
Studies in Logic, vol. 133, North-Holland 1994.
Yours sincerely, N.G. de Bruijn
Eindhoven University of Technology,
Department of Mathematics and Computing Science,
PO Box 513, Eindhoven, The Netherlands.