Fun with the halting problem.

Lets start by proving the following result.

Result 1

There is no program bool isDeadCode(Code j, Code c) that can check whether a program j contains dead code c.

What we mean by dead code is the following:

...
helloWorld();
if (true) { Console.WriteLine("Hey there") }
return;
Console.WriteLine("I will never be reached. I am dead code");
...

Anyhow, back to the proof...

Suppose there does exist a program bool isCodeDead(Code j, Code c) that can check whether a program j contains dead code c.

In other words. Something like this:

bool isCodeDead(Code j, Code c)
{
    ... // some magic here that tells if  c is dead in j
}

Now let k/0 be an arbitirary program for which we want to know whether it halts or not. We start by getting rid of all occurrences of c in k, producing k'. We can be sure that c isn' t dead code in k' because c is absent in k'.

Now lets consider the following pseudocode:

proc g:
    k'
    c

It should be clear that c will only be reached when k' halts. Since we assumed that we have a program bool isCodeDead(Code j, Code c) that checks whether a program contains dead code, we can tell whether g has dead code. But that also means we can tell whether k' halts. That leads to a contradiction because the halting problem tells us we cannot tell whether an arbitirary program halts or not.

Thus now we know our assumption was wrong and that the original result must hold by reductio ad absurdum. $\blacksquare$

Now lets use this result to proof an interesting Corollary.

Corollary 1

There is no program List<Code> markDeadCode(Code c) that can mark dead code in an arbitrary program.

The following proof is very similar to the previous one. Lets asume the contrary, that there is a program List<Code> markDeadCode(Code c) that can mark dead code in an arbitrary program.

The source code of such a program would be as follows:

// returns a list of codes that are dead in c.
List<Code> markDeadCode(Code c)
{
    ... // extreme Coding skills that can mark dead code 
}

Now we can write the following program:

bool isCodeDead(Code j, Code c)
{
    List<Code> deadCodes = markDeadCode(j);
    foreach (Code deadCode in deadCodes)
    {
        if (deadCode == c)
        {
            return true;
        }
    }
    return false;
}

Wait hold on a second!? Hadn't we proven in Result 1 that no program bool isCodeDead(Code j, Code c) could ever exist? Exactly. we have found a contradiction, and thus there is no way a program List<Code> markDeadCode(Code c) could ever exist by reductio ad absurdum.

$\blacksquare$

I found these proofs rather beautiful and wanted to share them with you :-)