Hacker News new | past | comments | ask | show | jobs | submit login

Whether or not you can map everything in the higher order language to the nat -> nat one is what's at issue, not the reverse.

For an analogy, you can map all the natural numbers to real numbers. This proves just about nothing. That you cannot map all the reals to the naturals proves something very important.

It would be truly bizarre if a useful programming language could express something that computation on bits could not.




> Whether or not you can map everything in the higher order language to the nat -> nat one is what's at issue

If you can't map higher-order constructs to Gödel codes (effectively, numerical representations of syntax), you can't always map them to `nat -> nat`. That's precisely my point.

And, if you could map higher-order constructs to Gödel codes, the higher-order abstractions would be lost - all you need to do to break the abstraction is inspect the syntax. Just like, if you have reflection, type abstraction is lost - all you need to do to break the abstraction is use typecase.


You would only not be able to map higher order functions to Gödel codes if it is not the case that for some n, f(n) outputs but does not determine m. I'm far from the most knowledgeable programmer in the world... but I do know that such a function could not be implemented by a computer.

As long as f(n) outputs a unique m, you can number f, n, and m. And as long as a programming language is Turing complete, you can do that. Interpreting any sort of abstraction is beside the point (even the "Gödel sentence" that you could ultimately find needn't be interpreted... which I suppose in this case would be a "Gödel operation").

Insofar as a program can be compiled and implemented in machine code, all the functions of that program's programming language can be mapped 1 to 1 to nat -> nat operations. This is just what's at issue here.

To cut through it a bit, you write

> The Church-Turing thesis says absolutely nothing about abstraction barriers your language might enforce, e.g., what you get if your language has parametric polymorphism

If a language has parametric polymorphism, is it therefore not Turing complete? Because if the language with parametric polymorphism is Turing complete, then the Church-Turing thesis absolutely has something to say about that language.


> Insofar as a program can be compiled and implemented in machine code, all the functions of that program's programming language can be mapped 1 to 1 to nat -> nat operations.

That mapping is a property of the implementation, not of the language. A user of the source language can't rely on the existence of this mapping - it would be literally impossible to run programs, say, using paper and pencil.

> If a language has parametric polymorphism, is it therefore not Turing complete?

Whut?

> Because if the language with parametric polymorphism is Turing complete, then the Church-Turing thesis absolutely has something to say about that language.

It says something about the functions of type `nat -> nat` that I can compute in the language. But a language with parametric polymorphism has lots of other types besides `nat -> nat`.




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: