Re: [Haskell-cafe] Very freaky

Cale Gibbard wrote:

On 10/07/07, Andrew Coppin wrote:

...

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.

I always have some beef with the common perception expressed in some of the above. I suppose I can speak concretely by listing again the three different presentations appearing above and comparing them. (A) ∀ pred : Nat → Prop . pred 0 → (∀ n:Nat . pred n → pred (n + 1)) → ∀ n : Nat . pred n (B) 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. (C) Mathematical induction I have re-formatted (A) and (B) to be fair, i.e., they both receive nice formatting, and both formatting are more or less equivalent, dispelling such myths as "formal logic is unorganized" or "English is unorganized". I have formatted them to be equally well-organized. (C) is the clearest to those people who have already learned it and haven't lost it. I grant you that if you talk to a carefully selected audience, you just say (C) and leave it at that. But if you need to explain (C), saying (C) again just won't do. Most people claim (B) is clearer than (A) when it comes to explaining (C). One unfair factor at work is that most people have spent 10 years learning English; if they have also spent 10 years learning symbols, we would have a fairer comparison. Someone who know C but not Haskell is bound to say that C is clearer than Haskell; we who know both languages know better. (B) is less clear than (A) on several counts, and they are all caused by well-known unclarity problems in most natural languages such as English. "if it applies to a number it applies to the next number" is unclear about whether "a number" is quantified by ∀ or ∃. It could be fixed but I think I know why the author didn't and most people wouldn't. If we actually try to insert "every" or "all" somewhere there, the whole of (B) sounds strange. Part of the strangeness is due to the lack of scope delimiters: Later in (B) there is another "all numbers" coming up, and two "all numbers" too close to each other is confusing. You need scope delimiters to separate them. English provides just a handful of pronouns: I, we, you, he, she, it, they, this, that, these, those. The amount is further decimated when you make mathematical statements (pure or applied). Any statement that needs to refer to multiple subjects must run into juggle trouble. In (B), fortunately 95% of the time is spent around one single predicate, so you can just get by with "it". You can't pull the same trick if you are to explain something else that brings up two predicates and three numbers. To this end, an unlimited supply of variables is a great invention from formal logic. (I am already using this invention by designating certain objects as (A), (B), (C) and thereby referring to them as such. There is no more tractible way.) Of course with the use of variables comes again the issue of scope delimiters. Actually even pronouns can be helped by scope delimiters. English badly lacks and needs scope delimiters. Quantifiers need them, variables need them, and here is one more: nested conditionals such as (B): if if X then Y then Z X implies Y implies Z are unparsible. Perhaps you can insert a few commas (as in (B)) or alternate between the "if then" form and the "implies" form to help just this case: if X implies Y then Z but it doesn't scale. It also proves to be fragile as we insert actual X, Y, Z: if it applies to a number implies it applies to the next number then it applies to all numbers Now, (B) is actually parsible, but that's only because I formatted it thoughtfully. Formatting is a form of scope delimiting, and that solves the problem. But formatting is tricky, as we have all learned from Haskell indentation rules. It is best to combine explicit delimiters such as parentheses with aesthetic formatting. Both the textually inclined and the visually inclined can parse it with ease, and (A) shows it. Actually, I formatted (A) first, since that's more obvious to format; then I copied its formatting to (B). You may counter me with this part: (A') ∀ n : Nat . pred n (B') pred applies to all numbers Surely the introduction of the variable n in (A') is an extra burden, and (B') streamlines it away? Yes, but (A') is not the best expression possible in formal logic anyway. Following the formal logic of HOL (hol.sf.net) and many others, ∀ is just another polymorphic operator: ∀ :: (a -> Prop) -> Prop and furthermore (A') is just syntactic sugar for ∀ (λn : Nat . pred n) which is (A*) ∀ pred Now it is streamlined: It only mentions the two essences of (B'): about pred, and being universally true. No unnecessary variable. If you also want it to say something about Nat, just throw in some types. Cale may counter that I have only been addressing precision, not "clarity" as he defined by ease of reading and inducing images in heads. Besides replying him with "if it doesn't have to be correct, I can write one that's even easier to read" (with apology to Gerald Weinberg), let me play along that definition just a bit. What image should I form in my head, if "a number" may be universal or existential and I don't know which to image, if "it" juggles between three subjects and I don't know which to image at which instance, and if the whole thing lacks scoping so much that it is not even parsible? As I write in another post: "I think of formal logic as clarifying thought and semantics, cleaning up the mess caused by idiosyncracies in natural languages (both syntax and semantics) such as English. But not many people realize they are in a mess needing cleanup." There are two ways to clean up anything. Take governments for example. If a government is corrupted, you could help it and fix it up, or you could start a revolution and remove it. Natural languages are also corrupted when it comes to clarity of thought, reasoning, and semantics. I take the extremist approach of siding with the revolutionaries, and that is starting over with a brand new language divorcing natural words, i.e., formal logic. I do not invest hope in fixing up natural languages because of these sentiments: natural languages are too fragile to fix, natural words are too overloaded to be safe to reuse, and if you fix it up it will look just like formal logic with bloat. It is also a benefit, not a drawback, to learn a different language and broaden one's mind; it is a drawback, not a benefit, to avoid a different language and narrow one's mind. It is also a benefit, not a drawback, to keep natural languages around for its strength: poems, puns, visions, sweeping generalizations; but do let's use a different language for a different task: a logical one for a logical task. Textually-inclined people feel at home with formal logic. Visually-inclined people are disadvantaged, but they are just as disadvantaged with textual natural languages. What they need are visual languages. Formal logic enjoys a more well-defined grammar and is a better basis than natural languages for developing visual languages. It only took humankind a millennium to see that clarity of arithmetic is achieved by forgetting natural language "intuition" and adopting formal language "manipulation", and then the science and engineering of physical hardware took off. It will only take you another millennium to see that clarity of semantics is achieved by forgetting natural language "intuition" and adopting formal language "manipulation", and then the science and engineering of logical software will take off. Already, it has started: http://www.abo.fi/~backrj/index.php?page=Teaching%20mathematics%20in%20high%...