Formal-ity and the Church-Turing thesis

[Mark Janssen]

> On Tuesday, October 8, 2013 5:54:10 AM UTC+5:30, zipher wrote:
>> Now, one can easily argue that I've gone too far to say "no one has
>> understood it" (obviously), so it's very little tongue-in-cheek, but
>> really, when one tries to pretend that one model of computation can be
>> substituted for another (arguing *for* the Church-Turing thesis), they
>> are getting into troubling territory (it is only a thesis,
>> remember)....
>
> The CT thesis is scientific and provable in one sense and vague/philosophical in another.
> The Science: Turing computability and lambda-computability are equivalent.
> The proofs just consist of writing interpreters for one in terms of the other.

Ah, good, a fellow theoretician.  Now it's nice that you use language
that makes it seem quite clear, but understand that there's a hidden,
subconscious, *cultural* encoding to your *statement*.  The use of the
term "equivalent", for example.  Equivalent for the programmer, or for
the machine?  (etc., et cetera), and further:  "writing interpreters
for one in terms of the other", but again, this will change depending
on your pragmatic requirements.  To the theorist, you've accomplished
something, but then that is a self-serving kind of accomplishment.  To
the programmer, operating under different requirements, you haven't
accomplished anything.  I don't have an infinite stack to implement
lambda calculus, but I can treat my computer's memory as a TM and
*practically* infinite and only rarely hit against the limits of
physicality.  This is just being "respectful"... ;^)

(For the purposes of discussion, if I make a word in CamelCase, I am
referring to a page on the WikiWikiWeb with the same name:
http://c2.com/cgi/wiki?WikiWikiWeb.)

> The philosophy: *ALL* computational models are turing equivalent (and therefore lambda-equivalent) or weaker.
> The Idea (note not proof) is that for equivalence one can write pair-interpreters like above. For the 'weaker' case, (eg DFA and TMs) one proves that TMs can interpret DFAs and disproves the possibility of the other direction.
>
> This must remain an idea (aka thesis) and not a proof because one cannot conceive of all possible computational models.

Why not?  I can "conceive" of all possible integer numbers even if I
never "pictured" them.  Is there not an inductive way to conceive of
and define computation?  I mean, I observe that the field seems to
define several ModelsOfComputation.  Intuitively I see two primary
domains

> It is hard science however for all the models that anyone has so far come up with.

And what of "interactive computation"?

> As for:
>
>> I challenge you to get down to the machine code in scheme and formally
>> describe how it's doing both.
>
> I can only say how ironic it sounds to someone who is familiar with the history of our field:
> Turing was not a computer scientist (the term did not exist then) but a mathematician.  And his major contribution was to create a form of argument so much more rigorous than what erstwhile mathematicians were used to that he was justified in calling that math as a machine.

Hmm, I'm wondering if my use of the word "formally" is confusing you.
In mathematics, this word has a subtly differing meaning, I think,
than in computer science.  Turing was "justified in calling that math
as a machine" because he was using a definition (the translation table
+ finite dictionary) such that it remained perfectly deterministic.

And here, again, one can easily gets mixed up using the same lexicon
across two different domains:  that of math and that of CS.  I advise
you to look at the dialog at ConfusedComputerScience.

> The irony is that today's generation assumes that 'some-machine' implies its something like 'Intel-machine'.
> To get out of this confusion ask yourself: Is it finite or infinite?

But this only gets us out of the confusion for the mathematicians.
For the programmer and perhaps even the computer scientist (the one's
coming from physics), it is something different.

> If the TM were finite it would be a DFA

But this is not a useful formalism.  Any particular Program implements
a DFA, even as it runs on a TM.  The issue of whether than TM is
finite or not can be dismissed because a simple calculation can
usually suffice, or at least establish a range "usefulness" so as not
to "run out of memory".

> If the Intel-machine (and like) were infinite they would need to exist in a different universe.

Ha, yeah.  Let us dismiss with that.

> And so when you understand that TMs are just a kind of mathematical rewrite system (as is λ calculus as are context free grammars as is school arithmetic etc etc) you will not find the equivalence so surprising

It's not that it's surprising, it's that it's *practically* a problem.
 The translation between one PL and another which assumes a different
model of computation can get intractible.

Maybe that makes sense....

MarkJ
Tacoma, Washington