Noncomputability of computable function application

Stream: new members

[Matt Diamond]

I recently came up with a proof of the statement ¬Computable₂ fun (f : NatComputable) (n : ℕ) => f n, where NatComputable is defined as { f : ℕ → ℕ // Computable f }. However, I don't completely understand why this is true. (My proof was a proof by contradiction in the style of Lawvere's theorem, but "assuming the opposite allows you to prove False" isn't a very satisfying explanation.)

I would think that applying a computable function would itself be a computable function. However, this is clearly not the case. Could anyone help me gain a deeper understanding of why function application isn't computable?

[Eric Rodriguez]

Does Computable give you an explicit algorithm for it, or just gives you a guarantee that such an algorithm exists?

[Matt Diamond]

well it's a Prop so I don't think you can extract the algorithm, but if you look at docs#Nat.Partrec you can see that the type itself is explicit

[Matt Diamond]

Computable is just Partrec with total functions, and Partrec is just a wrapper around Nat.Partrec with encoding/decoding

[Mario Carneiro]

You don't want to extract the algorithm, it's hilariously terrible

[Eric Rodriguez]

I guess that's the issue, you can't have a universal algorithm for computing a function just because you know in theory that it is computable

[Mario Carneiro]

but you could, in principle

[Matt Diamond]

I'm not sure what algorithm we're talking about extracting since I'm asking about a proof that function application isn't computable

[Mario Carneiro]

I'm not sure I would describe it as function application, it's more like a universal turing machine

[Mario Carneiro]

I don't know what would be the most intuitive "explanation" for your theorem; for example that function grows faster than any computable function so it can't be computable

[Matt Diamond]

that's a good point

[Mario Carneiro]

How is NatComputable primcoded?

[Mario Carneiro]

I think this theorem might be trivial, NatComputable doesn't look like it would have any sensible Primcodable instance

[Matt Diamond]

I proved that it was Countable and Infinite and then chose a Denumerable instance using Choice

[Mario Carneiro]

oof

[Matt Diamond]

haha yeah, I know

[Matt Diamond]

and then I relied on the fact that Denumerable.ofNat is "computable" to create a fixed point around Nat.succ

[Matt Diamond]

it was definitely hacky

[Mario Carneiro]

It might be interesting to prove that every Primcodable NatComputable instance is pathological in some way

[Mario Carneiro]

You should probably be able to prove your theorem generic over the Primcodable NatComputable instance

[Matt Diamond]

not sure what you mean by "generic"

[Mario Carneiro]

Take that instance as an argument to the theorem instead of proving it about one particular choice

[Mario Carneiro]

Note that with your definition, I'm not even sure you can evaluate app 0 0, so it's not going to be computable in a very literal sense

[Matt Diamond]

yeah, I realize the whole thing is noncomputable in a sense

[Mario Carneiro]

Mario Carneiro said:

It might be interesting to prove that every Primcodable NatComputable instance is pathological in some way

I suppose your theorem is essentially proving this (especially if you generalize over the instance instead of using the one you found using choice): there is no "nice" instance you can pick which makes function application computable

[Matt Diamond]

right

[Mario Carneiro]

that is possibly another way to answer your question about why the theorem should be true: there are ways to enumerate turing machines, but (1) you don't know when you have enumerated the same machine twice and (2) you don't know if it halts. Using choice to solve both issues results in an enumeration which has unknowably scrambled things and now you can't evaluate it

[Matt Diamond]

ah, true