Subject:

Your machine isn't turing complete, so why are you mentioning the halting problem?

Date: Mon, 1 May 2023
Message-Id: https://www.5snb.club/posts/2023/your-machine-is-not-turing-complete/
Tags: #rant(3)

Sometimes I will be part of exchanges such as:

Me: It would be cool if you could prove the lack of stack overflows in code!

Someone: Proving that code will not stack overflow is the same as solving the halting problem though.

Which is very much true, if you demand no false positives. But rather pointless. It’s being overly pedantic as a way of (intentionally or otherwise) being dismissive about useful feature ideas.

For a system to be Turing Complete, it needs to be able to emulate a Turing Machine, which has a tape of infinite length. Your system does not have infinite RAM, therefore it’s not Turing Complete.

This is, of course, entirely besides the point, since we can do useful work on a system with limited RAM, we just can’t do all the possible work. Just like we can do useful analysis on some functions, we just can’t do that analysis for all functions. It’s okay to say “I don’t know for sure that this is okay, so I’m going to make it a compile error”.

There’s lots of analysis that falls into this category. Writing a type checker, or borrow checker, that rejects all bad code and accepts all good code is equal to solving the halting problem, but no one throws “But Halting Problem” at them. Because they’re allowed to say “I don’t know for sure that this is okay, so I’m going to halt compilation”.

fn main() {
    if program_halts() {
        let mut x = 42;
        std::mem::swap(&mut x, &mut x);
    }
}

Rust will say that this code is an error. Which might be wrong, if program_halts ends up being false always, that code is not UB if you were to force it to compile anyways.

Also, given a deterministic system with finite amounts of state, you’re able to tell for sure if it will halt or infinitely loop, assuming you have a machine with twice as much state. Just treat it as a graph cycle detection problem.

Some sample code displays that point:

#[derive(Clone, PartialEq, Eq)]
struct Machine {
    instruction_pointer: usize,
    ram: Vec<u8>,
    code: &'static [Instruction]
}

impl Machine {
    /// Executes a single step in the machine.
    ///
    /// Any steps done after the machine has halted are no-ops and safely ignored.
    fn step(&mut self);

    /// Returns true if the machine has halted.
    fn halted(&self) -> bool;
}

fn halts(machine: &Machine) -> bool {
    let mut tortoise = machine.clone();
    tortoise.step();

    let mut hare = machine.clone();
    hare.step();
    hare.step();

    loop {
        if hare.halted() {
            return true;
        }

        // If they're equal, then that means there is a cycle somewhere
        // Which means the machine will always be in that cycle, and will not halt.
        if hare == tortoise {
            return false;
        }

        tortoise.step();
        hare.step();
        hare.step();
    }
}

This is some fairly simple cycle detection code, if you just think of the machines as nodes in a linked list.

You can’t use this to find cycles in all Turing Machines, because those use infinite state to begin with. But for programs that access a finite amount of RAM, it definitely will work. Eventually.

You’re allowed to have false positives in analysis, which makes you not fall under the halting problem issue.

So stop mentioning the halting problem. That’s just namedropping some computer science problem, and is equal to telling a developer of a route planning application that they should not bother, because travelling salesman is NP-Hard.