[Haskell-cafe] Very freaky

[Albert Y. C. Lai]

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
>> >
>>
>> 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%20school.html