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.