Comment by SilasX | Hacker News Reader

Comment by SilasX | Hacker News Reader

Parent Full thread

Sorry if I'm missing something fundamental, but (1) shouldn't matter if there's some mapping between a) those types and b) functions of type `nat -> nat`. AIUI, the CTT is equivalent to saying that anything that can be computed at all (regardless of type signature) can be done via the `nat -> nat` functions representable on some TM. IOW, whatever transformation it is that the other-typed function makes (edit: or whatever input-output mapping), it is isomorphic to one on `nat -> nat`.

Since computers regularly implement exactly such a mapping, it doesn't sound like a problem.

>Curiously enough, programming in the real world is seldom about evaluating functions of type `nat -> nat`.

How is it not about that? Everything you do is converted down to CPU ops that just implement (something expressible as) functions on natural numbers (technically, fixed-with binary numbers). The whole job of programming can be described as "converting a problem to a format suitable for a fast `nat->nat`-implementing machine"; it's just that several of the layers of the conversion are hidden from you.

> (1) shouldn't matter if there's some mapping between those types and functions of type `nat -> nat`.

That's the thing. In some languages, this mapping doesn't always exist.

> AIUI, the CTT is equivalent to saying that anything that can be computed at all (regardless of type signature) can be done via the `nat -> nat` functions representable on some TM.

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 (and no means to circumvent it, e.g., reflection).

These abstraction barriers might seem just like limitations that buy you nothing, but that's not the case. For example, if your language has abstract types (not the same thing as abstract classes), then you can be sure that any internal invariant violations can be traced to the module where the abstract type is defined. Have fun getting a static guarantee of this kind in C or Java.

> How is it not about that? Everything you do is converted down to CPU ops that just implement (something expressible as) functions on natural numbers (technically, fixed-with binary numbers).

Compilation translates programs in a source language into semantically equivalent programs in the target language. Compilation doesn't guarantee that every target language program is expressible in the source language - in fact, this is often not the case.

>That's the thing. In some languages, this mapping doesn't always exist.

The mapping exists, just not necessarily within the language; the CTT is orthogonal to practical difficulties of massaging the data into a usable input format. (e.g. how to convert a binary tree in to the TM's format and vice versa)

>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 ...

Those all speak to the issue of how difficult it is (for e.g. a human) to implement the function, not whether language/computation model can compute it at all.

>Compilation translates programs in a source language into semantically equivalent programs in the target language. Compilation doesn't guarantee that every target language program is expressible in the source language - in fact, this is often not the case.

If you have a computation for which no TM (or asm, C, etc program) exists that computes it, let us know! That would be real progress on the CTT towards a negative answer and a Fields Medal for whoever found it!

> The mapping exists, just not necessarily within the language

In practice, people write their programs in a programming language. Some languages (e.g., C, Java, Lisp) only provide leaky abstractions, so programmers always have access to the internal representation of everything, to the detriment of modularity. But there are languages (e.g., Standard ML) that aren't hobbled in this way.

> Those all speak to the issue of how difficult it is (for e.g. a human) to implement the function, not whether language/computation model can compute it at all.

No. In Standard ML, writing a function that inspects the representation of an abstract type isn't “difficult” - it's literally impossible. If you want to do it, you have to use a different language. The type system enforces the separation of concerns, so that you don't have to rely on your discipline alone.

> If you have a computation for which no TM (or asm, C, etc program) exists that computes it, let us know!

Re-read my sentence. I was talking about the converse: There exist programming languages that don't allow you to do everything the target machine can do.

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`.

>In practice, people write their programs in a programming language. Some languages (e.g., C, Java, Lisp) only provide leaky abstractions, so programmers always have access to the internal representation of everything, to the detriment of modularity. But there are languages (e.g., Standard ML) that aren't hobbled in this way. ... writing a function that inspects the representation of an abstract type isn't “difficult” - it's literally impossible.

Alright, at that point it becomes an issue of "what kinds of things count as computations" for the purposes of the CTT. You're right that some languages simply lack certain capabilities, but that's an issue of access, not computation per se. You can get the same result in pure math:

"C is incapable of computing the zlobnorg of a matrix."

'Ridiculous! I'm sure I can write a program that does it! So, what exactly is a zlobnorg?'

"Sorry, only the matrix itself can answer that."

If you're going to go that route, then yeah the CTT is false -- likewise, TMs can't see inside black holes, so they can't "compute" that either.

But the "computations" referred to in the CTT are assumed to meet certain criteria, e.g. that there's some API exposed for accessing the relevant information, and the output is a "pure function" of that input (or at least makes any external state changes accessible, etc). But then once you've done so, all the Turing-complete languages can access said information information and compute the correct result.

Now, if your point is that the day-to-day work of a programmer is a lot more than writing pure functions: I whole-heartedly agree and have said the same thing myself. I cringe at the whole "Maxwell's equations of programming". Of course you have to care about external state and access privileges and race conditions and whether the API is usable, etc -- things that the CT notion of "computation" doesn't deal with. But, for the same reason, that's also orthogonal to the CTT.

> You're right that some languages simply lack certain capabilities, but that's an issue of access, not computation per se.

Types determine what computations make sense.

> If you're going to go that route, then yeah the CTT is false -- likewise, TMs can't see inside black holes, so they can't "compute" that either.

Careful! I never said the CTT is false. I only said it guarantees nothing about functions whose type is anything other than `nat -> nat` (up to isomorphism).

> But the "computations" referred to in the CTT are assumed to meet certain criteria, e.g. that there's some API exposed for accessing the relevant information (...) Of course you have to care about external state and access privileges and race conditions and whether the API is usable, etc

These are properties of programs, not functions. Two syntactically different programs may compute the same function, so you can't conflate programs with functions (and hope to make sense).

>Types determine what computations make sense.

Types determine what the developer has certified as making sense. There can (and as far as we know, always does) exist an isomorphism between the higher-typed function that the developer has implemented and the TM-computable nat->nat.

So, a TM can "make sense" of the higher-order function, even when it only has the nat->nat type.

>Careful! I never said the CTT is false. I only said it guarantees nothing about functions whose type is anything other than `nat -> nat` (up to isomorphism).

And and I was saying that the CTT is equivalent to saying that there is an isomorphism between a TM-computable nat->nat and any function that can be computed at all.

>These are properties of programs, not functions. Two syntactically different programs may compute the same function, so you can't conflate programs with functions (and hope to make sense).

Fair enough -- I should have said "function" there but the point stands: you can't refute by CTT by defining Turing-complete language that lacks some critical access and say, "well, that's a function I guess it can't compute!"

> Types determine what the developer has certified as making sense.

Types determine what computations make sense, even before any program is written at all.

> There can (and as far as we know, always does) exist an isomorphism between the higher-typed function that the developer has implemented and the TM-computable nat->nat.

Are you sure you're talking about isomorphisms in the mathematical sense? https://ncatlab.org/nlab/show/isomorphism I'm talking about a pair of morphisms:

    forward :: Foo -> Bar
    backward :: Bar -> Foo

Such that they compose to identities:

    backward . forward = id :: Foo -> Foo
    forward . backward = id :: Bar -> Bar

I'm pretty sure there's no isomorphism between `nat -> nat` and `forall a. a -> a`. Just to give one example.

> And and I was saying that the CTT is equivalent to saying that there is an isomorphism between a TM-computable nat->nat and any function that can be computed at all.

What category are you working on?

> you can't refute by CTT by defining Turing-complete language that lacks some critical access and say, "well, that's a function I guess it can't compute!"

I'm not refuting the Church-Turing thesis! Why would I want to? I even believe it's true... in some models. (Yes, truth is relative to models of a theory. Unlike provability.) I'm only saying that the CTT only claims what it claims. You're making extra conclusions that don't follow from the CTT's statement.

You genuinely don't know how to write a TM that implements the identity function, or is there some technicality that it fails? If the latter, I'm not sure how it's relevant to my phrasing of the CTT.

>Types determine what computations make sense, even before any program is written at all.

>What category are you working on?

I have no idea what point you're trying to make with either of these comments.

>I'm not refuting the Church-Turing thesis! Why would I want to? I even believe it's true... in some models. ...

Regardless, my point is that the limitations you're bringing up seem to be very trivial and understate the extent to which it does apply. You're still wrong if you think the CTT is "true, but false if applied to matrix functions. No way could a computer handle that. They only know binaries numbers, not the matrix type. I mean, come on, I gave them a different name and everything!"

> You genuinely don't know how to write a TM that implements the identity function, or is there some technicality that it fails?

The inhabitants of the type `forall a. a -> a` (which, by the way, in an effectful, Turing-complete language, has more inhabitants than just the identity function) aren't in one-to-one correspondence with the inhabitants of the type `nat -> nat`. I asked for an isomorphism of types, you have to give me an isomorphism of types. Or maybe you don't know what “isomorphism” means in mathematics?

>> What category are you working on?

> I have no idea what point you're trying to make

Okay, you don't know what “isomorphism” means in mathematics.

> You're still wrong if you think the CTT is "true, but false if applied to matrix functions.

The CTT isn't “false if applied to matrix functions”. The CTT says nothing about functions at a type not isomorphic to `nat -> nat`. It would be like saying “SilasX is all wrong about frogs!”, when you never said anything about frogs (at least, in this discussion).

> No way could a computer handle that. They only know binaries numbers, not the matrix type. I mean, come on, I gave them a different name and everything!"

I write my programs in high-level programming languages, not machine language, though. The whole point to high-level programming languages is to reason in terms of their abstractions, not their possible implementations.

Reply on news.ycombinator.com