Externally, in the metalanguage, you can count syntactically distinct terms, and, of course, the collection of terms that have type `nat -> nat` is countable.
Internally, in the lambda calculus itself, or a model of it, there are two caveats, however:
(0) Nothing guarantees that all internal inhabitants of a type are denotable by external pieces of syntax. For example, most real numbers are undefinable. (There are only countably many formulas over a finite alphabet, but uncountably many real numbers, ergo, most real numbers can't be “pinned down” using a formula. That doesn't prevent them from existing. The situation is exactly the same with a type like `nat -> nat`.)
(1) The right internal notion of equality isn't syntactic equality (which doesn't even make sense, for the reason stated above), but extensional equality.
If all of this sounds too strange, read more about model theory, Gödel's completeness theorem, and the Löwenheim-Skolem theorems.
Yes but the real number that cannot be pinned down using a formula can also not be pinned down using a computation, and we are talking of models of computation.
> Yes but the real number that cannot be pinned down using a formula can also not be pinned down using a computation,
Undefinable real numbers exist, whether you can compute them or not.
> and we are talking of models of computation.
A theory of computation that rejects the existence of things that can't be computed is like a logic that rejects the existence of FALSE because it can't be proved. Where does the busy beaver function sit in your conceptual model?
> Undefinable real numbers exist, whether you can compute them or not.
I agree with you, but as you probably know this is a deep ontological question. The meaning of something "existing" has been debated for many centuries, especially for cases such as this.
> A theory of computation that rejects the existence of things that can't be computed is like a logic that rejects the existence of FALSE because it can't be proved. Where does the busy beaver function sit in your conceptual model?
There is a difference between rejecting and classifying. I am not proposing a new computational model. Turing's model classifies the busy beaver function as non-computable. Correct?
I thought we were discussing Church-Turing. This assumes Turing Machines, and what they can compute. Of course you can break everything by assuming an imaginary machine that can compute functions that are not computable by Turing Machines...
> Turing's model classifies the busy beaver function as non-computable. Correct?
Yep.
> I thought we were discussing Church-Turing. This assumes Turing Machines, and what they can compute. Of course you can break everything by assuming an imaginary machine that can compute functions that are not computable by Turing Machines...
Turing never redefined the concept of “countable”, which belongs in set theory. If you had asked him what the cardinality is of the set of functions from the naturals to the naturals, he would've answered you “uncountable, of course”.
It is not necessarily representable. By diagonalization, in fact, nat -> nat can be shown to be uncountably infinite. Intuitively, an example nat -> nat function that is uncomputable is ~Ld, the function that, given a natural index i into the diagonal of the table of Turing machines and their accepted strings, returns the opposite of whether machine i accepts string i. The output is then clearly equal to no Turing machine, since it differs in at least one position. In order to encode this function, an oracle is required. As such, nat -> nat uncountability can be shown to be central to proving Turing recognizability.
Ok, that's a good point, but it is also true that functions requiring an oracle cannot also be represented in any Turing-complete programming language, right?
This seems trivial to prove: any function representable in any given programming language maps to a finite string of characters, and finite strings of characters maps to natural numbers.
