Brain-Flak is a minimalistic, stack-based, Turing complete, esoteric programming language.

A big concern among Brain-Flak enthusiasts is a concept informally called "stack cleanliness".

The basic idea for stack cleanliness is that only certain values on the stack will be edited and all other values will remain unchanged

More formally:

Given an input arity (a tuple of positions on the active and inactive stack before the program runs), and an output arity (another tuple of the same sort after the program runs) and a function that maps between the two, a program is is considered stack clean iff it performs the function, ends on the stack it started, and the values on the stack that are not in the input remain the same regardless of the conditions of the stack.

The question is: Given a program that is known to halt for all input, a function and the two required arity tuples, is stack cleanliness computable?

  • 1
    $\begingroup$ By assuming that the given program halts you may get around the Halting problem reduction (on first glance) but is this still the problem you are interested in? How do you decide that the program under consideration halts? $\endgroup$ – Raphael Nov 2 '16 at 8:01
  • $\begingroup$ @Raphael To be honest I am mostly concerned with this problem purely out of curiosity. Brain-Flak is by no means a practical language and anything I do in it tends to be for sport. However on the practical side I would be nice to have a program that proves the stack cleanliness for halting of programs automatically if such a program could exist, because with most "practical" Bflk programs a proof of halting is fairly trivial while proof of stack cleanliness tends to be on the harder side. $\endgroup$ – Sriotchilism O'Zaic Nov 2 '16 at 16:04

I don't know the language in detail, but my guess is: no, stack cleanliness is not computable.

For every natural $n$, consider a Brain-Flak program $P_n$ which does the following:

  • take a natural $k$ as input;
  • without modifying the stack below, simulate Turing Machine number $n$ on empty input, for at most $k$ steps;
  • if the machine does not halt within $k$ steps, revert the stack to the original state, and return $0$;
  • otherwise, if it does halt, modify the stack below and return $0$.

$P_n(k)$ is guaranteed to halt for any inputs $n,k$.

$P_n$ will be stack-clean (on all inputs $k$, by definition) if and only if the TM number $n$ never terminates on empty input.

The latter is known to be undecidable (it's not even semi-decidable).

Hence stack cleanliness over input arity 1, output arity 1, and constant zero function is already undecidable.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.