On 10/07/07, Andrew Coppin
Stefan O'Rear wrote:
Another good example:
foo :: ∀ pred : Nat → Prop . (∀ n:Nat . pred n → pred (n + 1)) → pred 0 → ∀ n : Nat . pred n
x_x
Which you can read as "For all statements about natural numbers, if the statement applies to 0, and if it applies to a number it applies to the next number, then it applies to all numbers.". IE, mathematical induction.
...and to think the idea of mathematical symbols is to make things *clearer*...
As someone with a background in mathematics, I'd say that the idea of mathematical symbols is to make things more concise, and easier to manipulate mechanically. I'm not entirely certain that their intent is to make things clearer, though often they can make things more precise (which is a bit of a double edged sword when it comes to clarity). I quite often try to avoid symbols as much as possible, only switching to formulas when the argument I'm making is very mechanical or computational. After all, in most circumstances, the reader is going to have to translate the symbols back into concepts and images in their head, and usually natural language is a little farther along in that process, making things easier to read. - Cale