Leslie Lamport closes his paper with the statement
"Mathematicians have gotten along quite well for two thousand years without
types, and they still can today."
In fact, just the opposite is true: Mathematicians are so much used to a well
typed language that they will emphatically reject any ill-typed expression:
Paul Halmos mentions in his book "How to Write Mathematics" the nightmare of
any mathematician - a sequence n_{\epsilon} that tend to zero if \epsilon
tends to infinity!
Virtually each text book in mathematics has statements like : We denote
natural numbers by m,n,... real numbers by x,y,... functions by f,g,.. Of
course - as Lamport argues - these conventions are not necessary. Instead of
stating that the order of the reals is Archimedean as
"For all x there is some n such that x < n"
one may write
"For all sets a if a is in the set of real numbers then there is a set b such
that b is in the set of natural numbers and the ordered pair <a,b> is in the
set representing the natural order on the set of real numbers"
This would be perfectly correct. But giving it to an automated theorem prover
would have just the same effect that Leslie Lamport observed as harmful when
building types into the language: The prover might be occupied by checking
that some sets are members of others.
In mathematics the typed language helps the reader to find a proof. E.g. when
asked to prove that for all x (1 =< x^{2} + 1) - a statement that involves
only variables and constants of type real - the reader will try to use only
axioms and lemmata about real numbers to find a proof; he will not consider
properties of arbitrary sets or the definition of the reals as a set. Such a
restriction is of even greater importance for an automated theorem proving
system. Such a restriction of the knowledge base will enormously restrict the
space to be searched for a proof. In fact, in this example, it may be decided
to search for a proof from an untyped first order theory like the theory of
ordered ring. So types in a language can sometimes even help to eliminate
types for the provers.
But note: This effect has been obtained by considering types in the proof
strategy - not during the search for a proof which will not be affected by
types. A concious strategic decision has been made! This decision maybe wrong
in some cases. E. g. trying to prove that the order of the reals is
Archimedean will fail if the definition of the reals as a set is not taken
into account. Using type information for eliminating types maybe wrong, but in
many cases it's useful and that's, why mathematicians have gotten along quite
well for two thousand years with types, and they still do today.
Bernd, Ingo Dahn
dahn@mathematik.hu-berlin.de
Replied: Sun, 31 Oct 1993 11:03:27 -0600
Replied: "Piotr Rudnicki <piotr@cs.ualberta.ca> boyer"