Science Forums 2

[CraigD]

The Brainfuck esoteric computer language is discussed in the thread [thread=]“Brainfuck”[/thread]. In this post, I’ll describe a variation of this language I call “Lobotomized Brainfuck”, and give a halting deciding program for it.

Lobotomized Brainfuck (LBF) is Brainfuck with only the characters +, [, and ]. Thus, it has only a single 1-byte cell, which is assumed to overflow without error, that is, incrementing the value 255 results in a value of 0. It can be interpreted on any Brainfuck interpreter that has this overflow behavior.

A halting deciding program for LBF is described by the following vague pseudo-code logical expression:
If, for each [...] in program P
( if (count of + before [...]) =mod 256= 0
or (count of + before [...]) =mod (count of + within [...])= 256
) and (count of + withing ]...]) == 0
, program P halts.

The following MUMPS code implements this program:

n (XLLBFHP,R) s P=R,I=1 f  s J=$f(P,"[",I) x XLLBFHP(3) q:'R!'J  x XLLBFHP(1) q:'I  e  x XLLBFHP(2) q:'R!'I  ;XLLBFHP: Lobotomized Brainfuck halting program
s E=$e(P,I,J-2),L1=$l(E)-$l($tr(E,"+")) i '(L1#256) s D=1 f I=J:1 s E=$e(P,I),D=$s(E="[":1,E="]":-1,1:0)+D s:E="" (I,R)="" q:'I  i 'D s I=I+1 q  ;XLLBFHP(1): if (count of + before [...]) =mod 256= 0
s I=$f(P,"]",J),E=$e(P,J,I-2),L2=$l(E)-$l($tr(E,"+")) i $s(L2:(L1#L2)-(256#L2),1:1) s R=0 q  ;XLLBFHP(2): or [not] (count of + before [...]) =mod (count of + within [...])= 256
s R=1,E=$e(P,I,$s(J:J-2,1:$l(P))) i $p(E,"]",1,$l(E,"]")-1)["+" s R=0 ;XLLBFHP(3): [not] (count of + withing ]...]) = 0

The following use of it:

f  r R," " S R=$P(R," ") x XLLBFHP W $s(R="":" invalid",R:" ends",1:" doesn't end"),!

produced the following output for various LBF programs:

[]                  ends
+                   ends
+[]                 doesn't end
+[+]                ends
[+++]               ends
+++++[+]            ends
+[++]               doesn't end
+++[+++++]          doesn't end
++++[+++]           ends
+++++[+[++]]        doesn't end
++[+[++]]           doesn't end
+[+[++]++++[+++]]   ends
+[+[++[+++]][++]]   doesn't end
+[[+++]]            ends
+[++]               doesn't end
++++[+++]           ends
+[+]++[++]          ends
+[[+]++[++]]        ends
+[[+]++[++]]+       ends
+[[+]++[++]+]       doesn't end
+[[+]++[++]+]+[+]   doesn't end
[[[[]               invalid
]]]][               invalid
+[+[++[+++][++]]    doesn't end
+[+][]]]]           ends

I use the output “ends” and “doesn’t end” as synonyms for HALTS and LOOPS in the previous posts description of halting program results.

If the runtime failure of a syntactically ill-formed LBF program is considered halting, then the “invalid” results above may be considered “ends”. Note, however, that although this program returns R=”” indicating that the program is ill-formed, it is not a validity checking program, so may also return “ends” and “doesn’t end” for syntactically invalid programs.

As mentioned in post #1, this program is an example of a halting program that doesn’t run the program it decides, but rather analyzes the input program’s structure.