[Haskell-cafe] Haskell is a declarative language? Let's see how easy it is to declare types of things.

[Albert Y. C. Lai]

On 13-04-03 07:39 PM, Alexander Solla wrote:
> There's your problem.  Mathematicians do this specifically because it is
> helpful.  If anything, explicit quantifiers and their interpretations
> are more complicated.  People seem to naturally get how scoping works in
> mathematics until they have to figure out free and bound variables.

Quantifiers are complicated, but I don't see how explicit is more so 
than implicit. If anything, it should be the other way round, since 
correctly interpreting the implicit case incurs the extra step of first 
correctly guessing how to explicate. (If it doesn't have to be correct, 
I know how to do it 100 times simpler, to paraphrase Gerald Weinberg.)

I have just seen recently

   prove or disprove:
   for all e>0, there exists d>0,
     if 0<b<a<d, then (a-b)/sqrt(b) < e

I grant you that clearly the implicit quantifiers for a and b are "for 
all". The unclear part is where to put them. There are essentially 4 
choices: "for all a" may be outside or inside "there exists d", 
similarly "for all b".

Even when mathematicians care to explicate quantifiers, they pay lip 
service by the like of

   every x satisfies P(x,y) for some y

leaving you to wonder between "for all x, there exists y" and "there 
exists y, for all x".

How does one resolve this kind of ambiguities? It seems to me the reader 
is expected to go through this algorithm:

1. for each candidate C of disambiguation:
      launch your theorem prover to find a proof or disproof of C
      remember whether it's a proof or disproof
      remember the complexity of the proof or disproof

2. guess whether the author intends the statement to be true or false

3. discard candidates whose truth values disagree with the author's 
intended truth value (e.g., if C is disproved, but the author intends a 
true statement, discard C)

4. among the remaining candidates, pick the one with the highest 
complexity of proof/disproof, for the author clearly intends the most 
"interesting" candidate

5. insist that "this is the obvious choice". important! it is important 
to insist "obvious" so that people believe it and disbelieve what I'm saying

In other words, "to parse one statement, first prove or disprove four 
statements".

The people you have observed must be the top 1% of math classes, those 
students who qualify for math grad school. I am sure they are born to 
excel at this guessing game. What I have observed are instead "the rest 
of" the students and how naturally miserably they get scoping wrong 
until they figure out free variables and bound variables. I am referring 
to this simple highschool scenerio (now also a simple college scenerio):

Define f(x) = x^2
Define g(x) = 3*x

Before I continue, recall that they have no clue about free vs bound 
variables. Without that clue, they already have to figure out scoping, 
and they naturally decide... x has global scope! (It does not help that 
teachers and books also send out that message, intended or unintended.)

To compute f(0), set global x=0, f(x) = x^2 = 0^2.
To compute f(1), set global x=1, f(x) = x^2 = 1^2.

So far so good, and no problem on g(0) and g(1) either. Now ask this 
question:

f(g(x)) = ?

At this point, "the rest of" the students (i.e., not the top 1%) bifurcate:

Group A say: g(x) varies, therefore don't set global x to anything.
f(g(x)) = f(varying thing) = f(x) = x^2

Group B say: to compute f(g(x)), set global x=g(x)=3*x. so x=3*x. wtf?