Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!csd4.milw.wisc.edu!lll-winken!uunet!mcvax!hp4nl!philapd!ssp1!roelof
From: roelof@idca.tds.PHILIPS.nl (R. Vuurboom)
Newsgroups: comp.lang.misc
Subject: Re: Elegance (was Re: Language Tenets)
Summary: Elegance is not always understanding
Message-ID: <165@ssp1.idca.tds.philips.nl>
Date: 17 Jul 89 17:18:45 GMT
References: <57125@linus.UUCP> <1989Jun24.230056.27774@utzoo.uucp> <1207@quintus.UUCP> <1406@l.cc.purdue.edu> <2568@etive.ed.ac.uk>
Organization: Philips Telecommunication and Data Systems, The Netherlands
Lines: 44

In article <2568@etive.ed.ac.uk> nick@lfcs.ed.ac.uk (Nick Rothwell) writes:
>In article <1406@l.cc.purdue.edu>, cik@l.cc (Herman Rubin) writes:

>>There are times for elegance and times not to have elegance.  I will not
>>use an elegant definition if it obscures the concept.  I will not use a
>>short elegant proof, in general, if the understanding of the theorem is
>>compromised.
>
>Doesn't elegance imply clarity and understanding? 

Funnily enough, elegance does not always imply understanding. However the
catch here is that part of understanding a theorem is the ability to use 
not only the end result (the theorem statement itself) but the means to 
that end (the proof procedure). Sometimes in fact the proof procedure
itself is more important than the actual theorem statement.

There are several types of proof procedures. Some of which are:

	- existential		(...and therefor such an object must exist)
	- reductio ad absurdum  (suppose it isn't true and get a contradiction)
	- constructivistic	(...and this is the object)

Note that some existential proofs are reductio ad absurdums (suppose that
such an object does not exist).

Constructivistic proofs tend to go to the trouble (and detail) of creating
an actual object and, being more detailed, they tend (by definition) to be 
less abstract than existentials.

We're getting into an area of taste now but the higher the abstraction level 
(and hence shorter the proof) the more elegant (at least many think so).

Constructivistic proofs are especially important in computer science since
they can often be translated into computer algorithms while existentials
generally can't.

In this sense a less elegant (constructivistic) proof allows one sometimes 
to apply (and thus better "understand") a theorem where a more elegant 
(existential) proof would prevent this. 
-- 
Its a thin red line between boring and borish.

Roelof Vuurboom  SSP/V3   Philips TDS Apeldoorn, The Netherlands   +31 55 432226
domain: roelof@idca.tds.philips.nl             uucp:  ...!mcvax!philapd!roelof