Re: Re: Language vs. Library why it matters
- To: mathgroup at smc.vnet.net
- Subject: [mg61645] Re: [mg61563] Re: Language vs. Library why it matters
- From: Andrzej Kozlowski <akoz at mimuw.edu.pl>
- Date: Mon, 24 Oct 2005 21:07:02 -0400 (EDT)
- Sender: owner-wri-mathgroup at wolfram.com
On 22 Oct 2005, at 13:36, Richard J. Fateman wrote:
> Bill Rowe wrote:
>
>
>
>
>>
>>
>> My intent was merely to make the point Godel's results must apply
>> to Mathematica since they clearly apply to mathematics and
>> Mathematica
>> by design is intended to encompass mathematics.
>>
>>
>>
>
> Not so. Mathematica does not prove theorems, generally. Some
> mathsource
> programs may construct some proofs in some limited context, but those
> don't contradict Godel's result.
>
>
Of course they don't contradict it (how can they) but certainly they
are affected by it or rather by them. Mathematica not only computes,
it also uses mathematical concepts. Some of these concepts are
"infinitistic". I have myself partially implemented some algorithms
related to Matveev's complexity, which measures the "complexity" of a
4-manifold, and a manifold is not a "finitistic" concept. And
essentially anything infinitistic is subject to Godel's theorems. In
fact, concepts very closely related to Godel's work have actually
been implemented in Mathematica: for example Chaitin's Omega. In this
sense Bill is correct, any algorithmic mathematics can in principle
be implemented in Mathematica and will have to be subject to Godel's
theorems.
>
> Mathematica running on your computer is not, actually, as
> powerful as the simplest Turing machine. The "Halting Problem"
> for Mathematica on your computer is solvable. You have a finite
> machine with a finite number of states. It is possible in principle
> to tell if a program is in a loop or if it will halt. The testing
> procedure may take a very long time to run, but the testing procedure
> is also finite.
>
>
Yes, but bringing up the whole issue of finite state machines is just
a red herring. Actually, Godel's proof does not require the existence
of any infinite sets; it only requires the induction principle: for
every integer n there is an integer n+1. In the case of computers
this is equivalent to the principle that you can always construct a
larger computer. Even if the halting problem on any particular
computer is solvable, the halting problem for all possible computers
is not. And Mathematica can certainly be modified to run not just on
64 bit computers but on any kind of computer.
On the other hand if you introduce the objection that there is a
limit to the largest computer that can be constructed e.g. the number
of atoms in the universe - (I recall this very feeble argument has
been used by some computer scientist arguing against Roger Penrose's
"Shadows of the Mind") then you have to accept that algorithms also
are limited by their running time. There are many possible limits:
the maximum lifetime of the hardware, the maximum lifetime of any
human being, the maximum expected length of existence of any human
civilisation, the expected time before the lights go out in our solar
system, etc. The algorithm that solves the halting problem for the
computer made of all the atoms in the universe is likely to easily
exceed all of these.
So all the staff about finite state machines has virtually no
relevance to this discussion .
>
> If you want to explore decidability, Frege, Whitehead/Russell, Godel,
> Turing, ... that's fine, but don't confuse it with defects in
> computer algebra system design.
>
>
>
I am still rather amazed that my ironic and jocular remark generated
all this stuff. Of course I have always realised that people differ
hugely in their sense of humour: something that one person may see as
the pinnacle of wit to another will sound merely pathetic. There
was, however, a certain serious aspect to my bringing up Godel but it
appears to have been completely missed so I guess I should state it
explicitly.
I was of course referring to the analogy or similarity that exists
between the situation of a practical mathematician and of a practical
user of Mathematica. Godel's second theorem can be rather roughly
described as stating that we cannot prove the consistency of any
system of axioms that would be rich enough to serve as a basis for
the kind of work that most mathematicians do. However, if you ask an
average mathematicians what is this set of axioms mathematics is
supposed to be based on he will probably just stare at you with
incomprehension and disbelief. Very few mathematicians use any kind
of axioms and I doubt that one in ten could explain what the Zermelo-
Fraenkel axiom system is, or give an exact statement of either of the
two celebrated theorems of Godel. Most when faced with some
inconsistency in their mathematical work (a pretty common situation)
will first attribute it to some faulty reasoning on their part. If
everything seems fine at that level, they may start questioning some
of the results considered as established that they have been using.
Occasionally some of these are discovered to be incorrect in spite of
having been accepted previously. That is the only kind of
"inconsistencies in mathematics" that come up in the real world. When
they are discovered to be such they are simply eliminated and are no
longer considered part of "mathematics" - this is why I doubted that
an "inconsistency in mathematics" has any meaning (after it is
discovered it ceases to be regarded as part of mathematics; was it
really a part of it before?). Of course it is in theory possible to
imagine that this process of looking for the source of an
"inconsistency" might eventually lead one to question some of the
"axioms", but this is so unlikely that nobody normally needs to
concern himself with it at all.
So what does this have to do with Mathematica? Well, I think it does
have something to do with it, but it is an analogy rather than any
strict relationship.
Because of Godel's work a mathematician has to live with the
theoretical possibility that what he is doing essentially nonsense
because of some fundamental flaw at the level of "axioms of
mathematics". But the overwhelming majority of mathematicians (quite
rightly) could not care less: they go on solving problems using the
tools they are familiar with and relying on their skill and
intuition, not axioms and rigorous deduction from first principles.
In some way a Mathematica programmer is in a similar situation.
While I do not agree that there is nay indeterminism in Mathematica
except bugs that will be corrected (as in all software) and and
"features" like TimeConstrained, without which life would be even
worse for those with slower machines, there is indeed one aspect of
Mathematica, where there is a mall degree of unpredictability (rather
than indeterminism). This aspect lies at the heart of Mathematica and
distinguishes it (in my opinion very favourably) form other systems.
I am referring to pattern matching and transformation rules based on
pattern matching. In my opinion for a mathematician this is by far
the most natural way to program. As Steven Hatton correctly observed,
Mathematica re-write rules work exactly the way the human
mathematician works. By contrast tail recursion as used in Scheme is
very unnatural for a mathematician: it requires deliberate
readjustment of the normal way of thinking. (In fact there are pretty
good reasons to believe that exposure to too much Lisp diminishes
ones ability to understand more complex mathematics, which is one
reason why I would object to teaching Lisp as a programming language
to math students.)
So, while pattern matching and transformation rules are, for
mathematicians, the best aspect of Mathematica, they are also the
principal source of "unpredictability". To see the reason for this,
just consider how many ways there are in Mathematica of writing a
pattern. Remember that you have to take into account the effect of
Attributes of functions such as Orderless or Flat, and the effect of
HoldPattern, Verbatim etc. Then you also have to take into account
the fact that, for reasons of performance, Mathematica's pattern
matching is, in a sense, "incomplete". In a complicated expression
involving functions with Orderless and Flat attributes, the pattern
matcher will not look for patterns at all possible levels.
Remembering all that, try to ask yourself the question: what would
one mean by a complete documentation of Mathematica's pattern matching?
Presumably, it would have to be a set of sentences ("axioms") from
which the user would be able to determine exactly which pattern will
match which expression, no matter how complex either of them is.
Could a complete documentation of this kind possible be
significantly shorter than just listing all possible (finite)
patterns and expressions that they match? I don't know, but in any
case it seems likely that this list of "axioms of pattern matching"
would have to be pretty long. I am sure a lot longer than I would be
likely to read and remember. Would having such a documentation be of
any more use to you when using pattern matching in programming than
the axioms of set theory are to somebody working on the topology of 4
manifolds? I doubt it. I have been programming for quite a few years
in Mathematica, and have occasionally come across behaviour that
surprised me and did not work the way I expected. Maxim Rytin has
posted a few of such examples. In those rare situations when
something like that comes up in practice I behave exactly as I do
when I come across a similar problem in mathematics. I do not run for
my copy of Kleene or some other text on the foundations of
mathematics but simply change my approach relying on my intuition and
experience. I do not see how having a hugely complicated
documentation of something whose principal appeal is its naturalness
and simplicity (I mean pattern matching) would be of any help.
I think I have now written more than I ever wanted to write on this
topic.
Andrzej Kozlowski