Functional languages like ocaml are based on lambda calculus. Therefore users of ocaml might be interested to read theoretical papers about lambda calculus.
I have written a little paper which shows that there are functions which are non-computable in lambda calculus. Since lambda calculus can express all computable functions this is equivalent of saying that there are uncomputable functions. Interested readers can find the paper here.
This is phrased a bit unclearly. It is not hard to interpret “there are non-computable functions in lambda calculus” as “there exists a function that is not computable but can be expressed in lambda calculus”, which is false. Instead it would be clearer to write that since lambda calculus and Turing machines can express the same class of (number-theoretic) functions, then lambda calculus cannot express the non-computable functions.
Sorry for the sloppiness of this sentence. The sentence there are non-computable functions in lambda calculus is really misleading. It is better to say that there are functions which are not computable in lambda calculus. And since lambda calculus can express all computable functions this is equivalent of saying there are uncomputable functions. I have corrected the misleading sentence above.
There is a very simple counting argument that proves that not all functions are computable in the lambda calculus, or any programming language for that matter:
There are uncountably many functions.
There are only countable many lambda calculus terms.
Hence there exist functions without a corresponding lambda calculus term.
This is Cantor’s famous diagonal argument. It is taught in every theory of computation class.
So I’m curious what the contribution of your paper is?
@smolkaj: Very elegant highlevel argument. However it doesn’t give you an answer to the question Which functions are not computable?. It has been one of the great achievements of Turing, Church and Gödel to prove that there are undecidable propositions (or uncomputable functions) by giving explicit functions which cannot be computed. The most famous example is Turing’s halting problem.
The paper I have written does not have any new contribution. If it had, I would have sent it for publication to some scientific magazines. It is just a compilation of facts which have been known for a long time. I hope that I can make some of the facts more accessible with my writings.
Indeed the proof doesn’t construct you such a function. But using the proof @smolkaj mentions you can already pin down that there must be functions from ℕ → ℕ that are not computable. Basically programs are finite strings of a finite alphabet Σ, the cardinality of this set is |Σ*| = |ℕ| < |2ℕ| = |ℕ → ℕ|. So there must be a function from ℕ → ℕ to which you can’t associate a program.
I find models of computations rather ad-hoc an unsatisfying and what I really like in this proof is that there is none involved. It frames the problem in a purely descriptive fashion: you already don’t have enough finite strings (programs) to describe all the functions from ℕ → ℕ.
@dbuenzli and @smolkaj: Thank you for the interesting discussion. It might be interesting to look into the topic deeper. The elegance of the proof with cardinality of sets is very convincing. What does it prove really?
In this proof functions are treated as subsets of the cartesian product of the domain and the codomain with the restriction that the elements of the codomain are unique for each element of the domain. If we take the natural numbers as domain and codomain N -> N, then a function as a set consists of possibly infinite but countable many elements. The set of all functions is the set of all subsets of N x N which according to Cantors diagonal argument has a higher cardinality than the set N x N. Therefore the set of functions is not countable and the set of computable functions is the set of algorithms which has to be countable as Daniel outlined very well.
Therefore all functions as defined above cannot be computable.
Since Cantor lived before Hilbert, David Hilbert certainly has known this proof. But despite of this knowledge he challenged the mathematical community with the problem to solve the decision problem i.e. to find a general method to decide propositions. What is a decision procedure? It is a computable function which maps a proposition (which can be encoded as a natural number) to the set {0, 1}. What David Hilbert gave as a challenge was a specification of a function.
If we narrow down the space of functions to the space of functions with a specification we get a again a possibly infinite but countable set. A specification has to be written in some language over an alphabet. I.e. the set of functions of type N -> N with specification is certainly countable. In that case Cantors diagonal argument with cardinality no longer applies.
If we restrict ourselves to functions with specifications the topic from my point of view is much more interesting. Now we can pose questions like:
Compare the following statements:
If find the first statement much weaker than the second and the third. However to prove statements as the second and third we need more machinery than Cantors diagonal argument with cardinality.
Regards
Helmut
Thank you, Helmut, for elaborating.