Formal-ity and the Church-Turing thesis

[rusi]

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.

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.
It is hard science however for all the models that anyone has so far come up with.

Now there are caveats to this which I wont go into for now.

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.

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?
If the TM were finite it would be a DFA
If the Intel-machine (and like) were infinite they would need to exist in a different universe.

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