A
function is
decidable if there is a
Turing Machine that
computes the function in a
finite amount of
time (i.e., the Turing Machine
halts). Instead of talking about Turing Machines, though, let's use functions instead, because to me they're a little easier to
think about, but otherwise exactly the same. I'll use
ML syntax here.
In particular, we would like to find a function
fun H f x = true iff f:int->int halts on input x:int
But
consider a function
fun diag x = if (H diag x) then loop() else true
where
fun loop () = loop ()
So then
(H diag x = true) only if ((diag x) halts)
But
(diag x) halts exactly when
(H diag x) evaluates to
false, which is a
contradiction. Thus no such function H can
exist.
This is the halting problem, from which most of the theory of decidability branches out. So what can we do with the fact that H does not exist? Well, if we can show that given a "black box" function B, if we can use B to write H, then B must not exist. Here's an example:
Let's define
fun Z f = true iff f(0) halts, f:int->int
But then
fun H f x = Z (fn 0 => f x)
Here, if Z can
decide whether
(fn 0 => f x) halts on input 0, then that's really deciding whether
f x halts, which is the halting function. So Z cannot exist. Here are a few more examples:
fun Hsome f = true iff f x halts for some input x:int
but
fun Z f = Hsome (fn 0 => 0 | fn _ => loop ())
Here we've
reduced Z to Hsome. Since Z can't exist, neither can Hsome.
fun Hevery f = true iff f:int->int halts on every input x:int
but
fun Z f = Hevery(fn _ => f 0)
fun E (f, g) = true iff f(x) = g(x) for all x:int
but
fun H f x = E ((fn y => f x; y), (fn y => y))
and finally
fun Hsame (f, g) = true iff f and g halt on the same input
but
fun Hevery f = Hsame (f, fn _ => 0)
Please note that these functions Z, Hsame, etc.,
do exist for certain cases (i.e., for certain f's) and sometimes not
insignificant cases; all we've shown here is that they do not work in the
general case (for
every f).
There are many more functions that are not decidable and many more classes of decidability (i.e., recognizability), but that is beyond the scope of this node.