From dahn@mathematik.hu-berlin.de Fri Aug 5 02:47:57 1994 Received: from compu735.mathematik.hu-berlin.de (compu735.mathematik.hu-berlin.de [141.20.54.12]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id CAA16306 for ; Fri, 5 Aug 1994 02:47:50 -0500 Received: from kummmer.mathematik.hu-berlin.de by compu735.mathematik.hu-berlin.de with SMTP (1.37.109.8/16.2/4.93/main) id AA16111; Fri, 5 Aug 1994 09:40:55 +0200 Received: from wega.mathematik.hu-berlin.de by mathematik.hu-berlin.de (4.1/SMI-4.1/JG) id AA27926; Fri, 5 Aug 94 09:47:54 +0200 Date: Fri, 5 Aug 94 09:47:54 +0200 From: dahn@mathematik.hu-berlin.de (Dahn) Message-Id: <9408050747.AA27926@mathematik.hu-berlin.de> To: owner-qed@mcs.anl.gov Subject: Re: Types Considered Harmful In a manuscript "Types Considered Harmful", recently distributed by the qed mailer, Leslie Lamport argues, that types are unnecessary and possibly harmful in proving mathematical theorems. As far as this I agree, BUT I should like to add some arguments that types can be useful for proving mathematics if applied with care. 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 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