[Haskell-cafe] Very freaky
Albert Y. C. Lai
trebla at vex.net
Thu Jul 12 21:57:05 EDT 2007
Cale Gibbard wrote:
> On 10/07/07, Andrew Coppin <andrewcoppin at btinternet.com> 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
>> > 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
> 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
I suppose I can speak concretely by listing again the three different
presentations appearing above and comparing them.
(A) ∀ pred : Nat → Prop .
→ (∀ 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
(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
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
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)
(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
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
More information about the Haskell-Cafe