roelof@idca.tds.PHILIPS.nl (R. Vuurboom) (07/18/89)
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
marc@hpfcdc.HP.COM (Marc `Bo Who?' Sabatella) (07/25/89)
>In the POP-2 language and its derivatives, multi-result functions are handled >in a very straight forward manner: >... >If you think of "f(x,y)" as "push x, push y, call f", and "-> x" as "pop x", >then the underlying [stack] mechanism and its usages should be self evident. It is even more straightforward in Forth, where values are pushed by simply computing them, and implicitly popped by calling a word that requires an argument. Since parameters are not named, however, you get a lot of the "dup swap drip drop" that contributes to Forth's being considered a Write Only language. It seems POP-2 may have found one way around this.