Re: a multilingual approach

guttman@linus.mitre.org
Message-id: <9304141125.AA10713@circe.mitre.org>
To: qed@mcs.anl.gov
Cc: guttman@linus.mitre.org, farmer@linus.mitre.org, jt@linus.mitre.org
Subject: Re: a multilingual approach 
In-reply-to: Your message of "Tue, 13 Apr 93 17:10:38 EDT."
             <9304132110.AA10474@circe.mitre.org> 
X-Postal-Address: MITRE, Mail Stop A156 \\ 202 Burlington Rd. \\ Bedford, MA 01730
X-Telephone-Number: 617 271 2654; Fax 617 271 3816
Date: Wed, 14 Apr 93 07:25:50 -0400
From: guttman@linus.mitre.org
Sender: qed-owner
Precedence: bulk

In my last message I mentioned IMPS and the "little theories" version
of the axiomatic method, but without explaining what I meant.  

IMPS, an Interactive Mathematical Proof System, is an interactive
theorem prover intended for proofs in mathematics and software
assurance.  It uses a simple type theory with partial functions (such
as division, undefined for 0 denominator) and subtypes (the integers
are a subtype of the reals, for instance).  We have used IMPS to prove
a substantial collection of theorems including foundations of
analysis, some group theory, and various other areas.  IMPS is
described in a paper forthcoming in the Journal of Automated
Reasoning.  I would also be happy to send copies if you are
interested.  

One of the distinctive characteristics of IMPS is its support for the
"little theories" version of the axiomatic theory.  This contrasts
with the "big theory" version.

In the big theory version, the mathematician formalizes all of his
work within a single powerful theory, such as ZF set theory.  Each
model of this big theory must be large enough to contain
representations of all the objects that will be of interest to the
mathematician.

In the little theories version, different results are proved in
different theories, which may have relatively sparse vocabulary and
small models.  Mathematics done in different little theories may be
related by *theory interpretations*.  A theory interpretation is a
syntactic translation from the language of one theory to the language
of another, with the proviso that *theorems* of the source theory get
mapped to theorems of the target theory.  (To ensure that a
translation is an interpretation, it's enough to prove that the
*axioms* of the source theory map to theorems of the target, together
with a few other obligations that may depend on the logic.)  

To re-use a theorem of one theory, one constructs an interpretation
and then gets the image of the source theorem as a theorem of the
target theory without further proof.  For instance, to re-use a
theorem about metric spaces in a context concerning the reals, one
constructs an interpretation from the metric space theory to the
reals.  This formalizes the idea that the reals "may be regarded as a
metric space" in such-and-such a way.  

As a more interesting example, consider the Knaster fixed point
theorem (which was recently formalized in Imps by Javier Thayer).
First we define monotonicity in the context of a theory of a partial
order written "prec" over objects in a universe uu:

(def-constant monotone
  "lambda(f:[uu,uu], forall(x,y:uu, x prec y implies f(x) prec f(y)))"
  (theory partial-order))

Then the fixed point theorem is stated and proved in the theory
(extending partial-order) complete-partial-order:


(def-theorem knaster-fixed-point-theorem
  "forall(f:[uu,uu], 
           forsome(bot,top:uu, forall(x:uu, bot prec x and x prec top))
            and
           monotone(f)
            implies
           forsome(z:uu, f(z)=z))"
  (theory complete-partial-order)
  (usages transportable-macete)
  (proof ( ... )))

Many useful consequences follow from interpreting uu and prec to be,
for instance, sets and inclusion (such as the Schroeder-Bernstein
theorem), or the reals and <= (for a different kind of intermediate
value theorem), or real functions.

The little theories approach is discussed in a paper called "Little
Theories", CADE-11, 567-580, written with my colleagues Bill Farmer
and Javier Thayer.  

	Josh