Partially Solve the halting problem for brainf***

Question

To solve the Halting Problem you are given a description of a program, and must determine whether or not it will ever finish. You can never do this for all programs. Yet for programs like (in brainf***):

>

It obviously will halt, and for programs like:

+[]

It obviously will not. Your challenge is to "solve" the halting problem for as many programs as possible. These programs will not use . or ,, and will not have input or output. You will be given a description of the program and must output either "Halts", "Does not halt", or "Unknown". When your program outputs "Halts" or "Does not halt", you have solved the input program. Here are some requirements.

1. It must solve at least an infinite amount of programs.
2. For every program it solves, its solution must be correct.
3. You may only output 1 of the 3 above choices.
4. You may assume that the running computer has infinite time and memory, so XKCD 1266 would not work (the tape is unlimited).
5. No external resources.
6. You may not use a programming language that can actually solve the halting problem.

You may have a non-code-golfed side program that takes a string that is a program, and generates some sort of abstract syntax tree of it if you like. Note, that isn't really scoring per se, but how to determine if one program beats another.

1. If program A solves an infinite number of programs that B doesn't, but B only solves finite or no programs that A solves, A automatically wins.
2. Otherwise, the program with the fewest characters wins. Do not count white space or comments, so do not obfuscate your code.

Tip: Timers won't work. You see, for any time T and given machine, there is an N, such that all programs longer than that have to take more than T time. This means that a timer can only achieve the solution of a finite number of programs, and, as you can see above, solving a finite number of programs doesn't help.

Answer 1

Python, ungolfed spaghetti code

Oh dear.

def will_it_halt(instructions):
    tape_length = 1
    LOOP_BOUND = 1000
    registry = [0] * tape_length
    pos = 0

    jumpbacks = []
    reached_states = set()

    pos_instructions = 0
    while True:
        letter = instructions[pos_instructions]
        if letter == "+":
            registry[pos] = (registry[pos] + 1) % 256
        elif letter == "-":
            registry[pos] = (registry[pos] - 1) % 256
        elif letter == ">":
            pos += 1
            if pos >= tape_length:
                registry += [0]*tape_length
                tape_length = len(registry)
        elif letter == "<":
            pos -= 1
            if pos <= 0:
                registry = [0]*tape_length+registry
                tape_length = len(registry)
                pos += tape_length
        elif letter == "[":
            if registry[pos] == 0:
                nests = 1
                while nests:
                    pos_instructions += 1
                    if instructions[pos_instructions] == "[": nests += 1
                    elif instructions[pos_instructions] == "]": nests -= 1

                if jumpbacks == []:
                    reached_states.clear()

            else:
                jumpbacks.append(pos_instructions-1)

        elif letter == "]":
            stripped_registry = [str(x) for x in registry if x != 0]
            translated_pos = pos - (len(registry) - len(stripped_registry))
            state = (translated_pos, pos_instructions, ".".join(stripped_registry))
            if state in reached_states: return "Does not halt"
            elif len(reached_states) > LOOP_BOUND: return "Unknown"
            else:
                reached_states.add(state)
                pos_instructions = jumpbacks.pop()
        pos_instructions += 1
        if pos_instructions >= len(instructions): break
    return "Halts"

Pretty brute-forcey solution to the problem: just run the bf code. We assume the tape length is arbitrarily long and that individual cells wrap at 256. At the end of every loop, we store the state of the tape with a set. States are of the form (our position on the tape, our position on the instructions, what the tape looks like with leading 0's stripped).

If we store the same state twice, then we're somewhere in an infinite loop, so the program does not halt. If we store over 1,000 states, then cut losses and return unknown. Once we leave a loop we check to see if we aren't in any larger loops. If not, we're never seeing any of the previous states ever again (at the very least, the instruction position will always be different!) so we can clear the set of states.

This should accurately determine any BF program who's loops aren't longer than 1,000 iterations, as well as many programs that repeat a state before 1,000 iterations in a loop. Not all of them, though: something like "{1 million +'s here}[-]>+[+-]" eventually repeats a state, but the [-] loop passes 1,000 iterations first.

Some examples:

>+>->+>-

No loops, so it reaches the end and halts.

+[+]

Loop ends after 256 iterations, so it reaches the end and halts.

+[+-]

Eventually repeats the state (0,5,"1"), so it does not halt.

+[->+]

This doesn't repeat any states but the loop never ends, so it should print "unknown". But the program kind of cheats here. Instead of storing the position on the tape, it adds an offset between the original registry and the stripped one. If all a loop does is translate the tape by some spaces, then it will continue translating it indefinitely (like a life glider), so we can say it does not halt.

+[>+]

Doesn't translate, doesn't repeat any states, prints unknown.

+++++++++++[-]

This does halt, but it would print "unknown" if LOOP_BOUND was 10.

There's a couple of ways to make this smarter. You could obviously increase LOOP_BOUND to reduce the number of unknowns. You could have smarter handling of nested loops. You could probably do something fancy with BB numbers and the size of loops to better detect if something should halt, but I'm not good enough at CS nor at Python to be able to do that yet.

Answer 2

GolfScript (23 chars, infinite correct answers)

'[]'&!
# 0 if there are brackets, so Unknown
# 1 if there are no brackets, so no looping, so definitely halts
'UnknownHalts'7/=

Answer 3

Awk

A small extension in power from the two examples. If a program contains no loops at all, hence no decisions, it is still obviously determined to halt. Since we're assuming validity of the program, we also assume brackets are balanced and thus need only search for one or the other of the brackets.

BEGIN{RS=""}
!/\[/{print "Halts"; exit}
END{print "Unknown"}

For the second, it must check first if the loop runs at all, so we must simulate the straight-line code preceding the loop. Then, if the loop returns to the same cell (ie. number of >s is equal to the number of <s within the loop), and it performs no incs or decs at this cell (ie. for any position-balanced prefix of the balanced loop body, there are no instances of + or - before the next < or >, then the cell is unmodified). Implementing this part may take me more time. Ooh, wait, for the first part of checking if the loop runs at all, we can take this same idea and search the pre-loop program for balanced suffixes and insist that there be a + or - (unbalanced).

Answer 4

Haskell

Here is a really simple example answer. Feel free to include it in your answers (since you including multiple tests in an answer is a good idea.)

main=do
    p<-getLine
    if take 3 p == "+[]"
        then putStr "Does not halt"
        else putStr "Unknown"

It basically sees if there is a loop in the beginning. If that exact loop doesn't occur in the beginning, it just gives up. It doesn't even work for ++[]. It does solve an infinite number of programs though, and it is always correct when it solves it.