6 ms·

A few years ago I had an idea to try and solve halting problem for as many Brainfuck problems as possible, using a few simple heuristics. (To make things easier

A few years ago I had an idea to try and solve halting problem for as many Brainfuck problems as possible, using a few simple heuristics. (To make things easier I picked a dialect with 1 byte cells that weren't allowed to over- or underflow.) I managed to solve all BF programs up to length 12. The longest running but stopping short program that I've found was this: >+[>++>+++[-<]>>], it stopped after 9212 steps. https://github.com/eterevsky/beaver https://github.com/eterevsky/beaver

tromp 3y ago
> I managed to solve all BF programs up to length 12. With 8 possible instructions, that is equivalent to all programs up to 12 * log 8 = 36 bits. Curiously, that exactly matches how far we were able to analyze the behaviour of a functional busy beaver [1]. > it stopped after 9212 steps. The largest output of a 36 bit lambda term is a whopping 578960446186580977117854925043439539266349923328202820197287920039565648199686 bits long though... [1] https://oeis.org/A333479 https://oeis.org/A333479
- smohare 3y ago
  [dead]
saghm 3y ago
From what I recall, the "undecidable" part of the halting problem isn't determining that something halts, but determining that it _doesn't_ halt (i.e. the halting problem is verifiable, as opposed to the inverse "non-halting" problem, which isn't verifiable, which is always the case for the inverse of a verifiable problem).\ I've never properly learned brainfuck, so the answer to this might be trivial without needing to write a solver, but what's the shortest non-halting program you found?
- shoo 3y ago
  The shortest non-halting brainfuck program will have exactly three instructions. Here is one them: `+[]` here is another one: `-[]`. Brainfuck's state consists of an array of integers, an index into that array, a program counter, and some bookkeeping required to track which "[" corresponds to which "]". Let's assume the array a[:] is zeroed and the index i is set to 0 before the program begins executing. Then `+` increments the cell in the array a at index i, i.e. `a[i] += 1`; `[` begins a while loop, equivalent to `while a[i] != 0 {`; and `]` ends the while loop: `}` . So the program `+[]` is equivalent to something like a := (allocate a length N array of bytes, set to zero) i := 0 a[i] += 1 while a[i] != 0 { } which will not terminate. Why is this the shortest? `]` is the only instruction that might decrease the program counter, otherwise the program counter always increases by one or more. Therefore, a non-halting brainfuck program must include at least one `]`. Brainfuck programs are syntactically incorrect unless there is exactly one `]` occurring somewhere in the program after each `[`. So the shortest non-halting brainfuck program must have at least two instructions. There is only one syntactically valid brainfuck program with two instructions that might not halt: `[]`. But this will halt, assuming that the array `a` is initialised to zero before execution begins. So the shortest non-halting brainfuck program contains three instructions.
  - LegionMammal978 3y ago
    To add to this, there is also the `,[]` program, which reads a single input byte, halts iff it is zero, and loops infinitely otherwise.
    - shoo 3y ago
      Fair point! Arguably the program `,` might not halt if a user never provides a byte of input to read! I've never seen a brainfuck machine with a read timeout.
  - smohare 3y ago
    [dead]
- lmm 3y ago
  > I've never properly learned brainfuck, so the answer to this might be trivial without needing to write a solver, but what's the shortest non-halting program you found? It's a pretty trivial question in any language, it tends to just be while(true); or similar in that language.
  - nixpulvis 3y ago
    What is it in the lambda calculus?
    - lmm 3y ago
      (Lx.xx)(Lx.xx) is the most famous/well-known one.
      - tromp 3y ago
        And as it turns out, the smallest one too. For combinatory logic with the usual {S,K} basis, it's S S K (S (S S K).
    - burnished 3y ago
      What does 'lambda calculus' mean? I read that lambda refers to binding to variables - so is 'calculus' really just a way to refer to calculating generally? I suppose I only know the word contextually from the math class that shares the name.
      - sam_bristow 3y ago
        "Lambda calculus is a notation for describing mathematical functions and programs. It is a mathematical system for studying the interaction of functional abstraction and functional application. It captures some of the essential, common features of a wide variety of programming languages." - https://www.cs.cornell.edu/courses/cs3110/2008fa/recitations/rec26.html https://www.cs.cornell.edu/courses/cs3110/2008fa/recitations...
        3y ago
- deleted 3y ago
  [deleted]
- rstuart4133 3y ago
  Actually, it's possible to determine if any machine with a finite (bounded) number of states (ie, finite memory) halts given a finite (bounded) input. You just enumerate all the states. If for some input there is a sequence of states that loops without consuming input, it's infinite, otherwise not. In practice it may not there may not be enough resources to build something to enumerate all the states on all inputs, but we are talking theoretically here. Theoretically, there is no halting problem in a finite world. And we humans live in what looks to be a locally finite world, so it doesn't apply to us. The halting problem is actually a statement on whether it's possible to always determine if a finite set of rules that have infinite memory will halt on all inputs. The answer is famously no. Thus the halting problem illustrates a property of infinities. It's a subtlety that's rarely mentioned. It is an interesting property. One thing it says to me is there are things in an infinite world a finite computation machine (like our human brains) will never be able to understand. While locally (say within the Milky Way) we live in a finite world the Universe itself may well be infinite. Ergo, there may be some aspects of the Universe we can never understand, and some things may happen that we can never predict.
  - srcreigh 3y ago
    It’s not so simple, even finite halting code has to handle the self recursion reversal trick somehow. Aka the finite bounds must exclude the “if H(X,I) loop forever; else halt” code because H would still be broken. You could try defining H to only work on input machines smaller than itself. However there’s still problems. If you don’t limit input size (aka the I in H(M,I) does machine M halt on input I), your code would still get tricked if M is just a tiny emulator and the input is the whole self defeating H program. So M and I both must be limited. Anyway that’s not to say a finite H would work even if the input size is limited. You’d have to prove it’s impossible to self recurse - so you’d need good compression. That’s all assuming self recursion is the only problem with the halt programs. Maybe it’s not, and it seems difficult to rule out other problems and see how they’d affect finitely bound TMs. I’m just spitballing here. For a while I was infatuated by the idea of snuffing out self recursion or otherwise somehow making a variant of halting programs possible. But self referential poison seems really, really tough to prove the non existence of. Anyways, I’m of the attitude that the proof for halting problem undecidability is a dumb trick. I’m simply fine with a halting program that doesn’t work correctly in self referential cases. As above though, that just leaves the whole problem vague aka don’t know about other issues and there’s the problem of actually solving it anyways (aka solving all of mathematics at once).

tromp 3y ago

> I managed to solve all BF programs up to length 12. With 8 possible instructions, that is equivalent to all programs up to 12 * log 8 = 36 bits. Curiously, that exactly matches how far we were able to analyze the behaviour of a functional busy beaver [1]. > it stopped after 9212 steps. The largest output of a 36 bit lambda term is a whopping 578960446186580977117854925043439539266349923328202820197287920039565648199686 bits long though... [1] https://oeis.org/A333479 https://oeis.org/A333479

smohare 3y ago
[dead]

saghm 3y ago

From what I recall, the "undecidable" part of the halting problem isn't determining that something halts, but determining that it _doesn't_ halt (i.e. the halting problem is verifiable, as opposed to the inverse "non-halting" problem, which isn't verifiable, which is always the case for the inverse of a verifiable problem).\ I've never properly learned brainfuck, so the answer to this might be trivial without needing to write a solver, but what's the shortest non-halting program you found?

shoo 3y ago
The shortest non-halting brainfuck program will have exactly three instructions. Here is one them: `+[]` here is another one: `-[]`. Brainfuck's state consists of an array of integers, an index into that array, a program counter, and some bookkeeping required to track which "[" corresponds to which "]". Let's assume the array a[:] is zeroed and the index i is set to 0 before the program begins executing. Then `+` increments the cell in the array a at index i, i.e. `a[i] += 1`; `[` begins a while loop, equivalent to `while a[i] != 0 {`; and `]` ends the while loop: `}` . So the program `+[]` is equivalent to something like a := (allocate a length N array of bytes, set to zero) i := 0 a[i] += 1 while a[i] != 0 { } which will not terminate. Why is this the shortest? `]` is the only instruction that might decrease the program counter, otherwise the program counter always increases by one or more. Therefore, a non-halting brainfuck program must include at least one `]`. Brainfuck programs are syntactically incorrect unless there is exactly one `]` occurring somewhere in the program after each `[`. So the shortest non-halting brainfuck program must have at least two instructions. There is only one syntactically valid brainfuck program with two instructions that might not halt: `[]`. But this will halt, assuming that the array `a` is initialised to zero before execution begins. So the shortest non-halting brainfuck program contains three instructions.
- LegionMammal978 3y ago
  To add to this, there is also the `,[]` program, which reads a single input byte, halts iff it is zero, and loops infinitely otherwise.
  - shoo 3y ago
    Fair point! Arguably the program `,` might not halt if a user never provides a byte of input to read! I've never seen a brainfuck machine with a read timeout.
- smohare 3y ago
  [dead]
lmm 3y ago
> I've never properly learned brainfuck, so the answer to this might be trivial without needing to write a solver, but what's the shortest non-halting program you found? It's a pretty trivial question in any language, it tends to just be while(true); or similar in that language.
- nixpulvis 3y ago
  What is it in the lambda calculus?
  - lmm 3y ago
    (Lx.xx)(Lx.xx) is the most famous/well-known one.
    - tromp 3y ago
      And as it turns out, the smallest one too. For combinatory logic with the usual {S,K} basis, it's S S K (S (S S K).
  - burnished 3y ago
    What does 'lambda calculus' mean? I read that lambda refers to binding to variables - so is 'calculus' really just a way to refer to calculating generally? I suppose I only know the word contextually from the math class that shares the name.
    - sam_bristow 3y ago
      "Lambda calculus is a notation for describing mathematical functions and programs. It is a mathematical system for studying the interaction of functional abstraction and functional application. It captures some of the essential, common features of a wide variety of programming languages." - https://www.cs.cornell.edu/courses/cs3110/2008fa/recitations/rec26.html https://www.cs.cornell.edu/courses/cs3110/2008fa/recitations...
      - 3y ago
deleted 3y ago
[deleted]
rstuart4133 3y ago
Actually, it's possible to determine if any machine with a finite (bounded) number of states (ie, finite memory) halts given a finite (bounded) input. You just enumerate all the states. If for some input there is a sequence of states that loops without consuming input, it's infinite, otherwise not. In practice it may not there may not be enough resources to build something to enumerate all the states on all inputs, but we are talking theoretically here. Theoretically, there is no halting problem in a finite world. And we humans live in what looks to be a locally finite world, so it doesn't apply to us. The halting problem is actually a statement on whether it's possible to always determine if a finite set of rules that have infinite memory will halt on all inputs. The answer is famously no. Thus the halting problem illustrates a property of infinities. It's a subtlety that's rarely mentioned. It is an interesting property. One thing it says to me is there are things in an infinite world a finite computation machine (like our human brains) will never be able to understand. While locally (say within the Milky Way) we live in a finite world the Universe itself may well be infinite. Ergo, there may be some aspects of the Universe we can never understand, and some things may happen that we can never predict.
- srcreigh 3y ago
  It’s not so simple, even finite halting code has to handle the self recursion reversal trick somehow. Aka the finite bounds must exclude the “if H(X,I) loop forever; else halt” code because H would still be broken. You could try defining H to only work on input machines smaller than itself. However there’s still problems. If you don’t limit input size (aka the I in H(M,I) does machine M halt on input I), your code would still get tricked if M is just a tiny emulator and the input is the whole self defeating H program. So M and I both must be limited. Anyway that’s not to say a finite H would work even if the input size is limited. You’d have to prove it’s impossible to self recurse - so you’d need good compression. That’s all assuming self recursion is the only problem with the halt programs. Maybe it’s not, and it seems difficult to rule out other problems and see how they’d affect finitely bound TMs. I’m just spitballing here. For a while I was infatuated by the idea of snuffing out self recursion or otherwise somehow making a variant of halting programs possible. But self referential poison seems really, really tough to prove the non existence of. Anyways, I’m of the attitude that the proof for halting problem undecidability is a dumb trick. I’m simply fine with a halting program that doesn’t work correctly in self referential cases. As above though, that just leaves the whole problem vague aka don’t know about other issues and there’s the problem of actually solving it anyways (aka solving all of mathematics at once).