Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
In 2007, it has been proven that high-order unification is decidable on the pattern matching case. If that is true, what is stopping someone to write an equation like:
(F [1,3,2], F [4,1,3,2], F[3,1]) = ([1,2,3], [1,2,3,4], [1,3])
If the unification works, wouldn't it probably find an F which implements a sorting algorithm - essentially generalizing the programming by example technique and, to an extent, replacing a programmer's job?
It's incredibly unlikely that a complete sorting algorithm that works for ANY input would be deduced from just 3 inputs.
In particular, there's a problem: sorting is a problem that matches an infinite set of inputs to an infinite set of outputs. You've only given a finite set of inputs, so there's an infinite number of problems which could be described by those input/output pairs.
For example, what if we want to sort numbers lexographically (i.e. dictionary order) instead of numerically? So 1, 11, 112, 1123, all come before 2. But, your example also describes lexographically sorting the given inputs. How does the algorithm know which one?
In short, it can't figure out that you want a sorting algorithm, because you haven't told it you want a sorting algorithm.
For that, you need a specification of some sort. The problem of "Given an arbitrary specification, find an algorithm that meets that specification" is undecidable.
So, there will never be a computer program which, 100% of the time, generates a correct algorithm solving any problem you give it.
It's possible that with machine learning, we can automatically derive some algorithms, but there will always either be a risk that those algorithms are incorrect, or there will be a risk that our procedure will say "I couldn't find a solution."
This is an unavoidable fact of mathematics.
