[Haskell-cafe] Haskell is a declarative language? Let's see how easy it is to declare types of things.
Albert Y. C. Lai
trebla at vex.net
Thu Apr 4 05:46:37 CEST 2013
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
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
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
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?
More information about the Haskell-Cafe