StackFlow
StackFlow is an esoteric programming language created by User:ais523 in 2014, which is entirely based on simple stack operations. The language is intended for the purpose of implementing in other languages in order to prove them Turing complete. In particular, the motivating example was the card game Magic: the Gathering; although Magic had already been proven Turing-complete, ais523 wanted to find a construction in which none of the players had any ability to interfere with the execution of the program, and in pursuit of that goal, it helped to have a language that was simpler than a Turing machine and worked almost entirely in terms of stacks of small enums, which are the easiest data structure to simulate in Magic. StackFlow is entirely usable on its own, though, and may be interesting in other contexts.
Ironically, StackFlow turned out to be more difficult to implement in Magic than expected; nowadays, most constructions that would have been expected to use StackFlow instead use a simpler, but comparable, language, The Waterfall Model, which has mostly replaced StackFlow for use as a target language in Turing-completeness proofs because it can be trivially compiled into it (thus a proof that a language can implement StackFlow can trivially be modified to use The Waterfall Model instead, often simplifying it in the process).
Semantics
All data in a StackFlow program is stored on one of a number of stacks; the number of stacks is fixed for any given program, and specified as part of the source of that program. Each stack is associated with a finite set of symbols, which are the only elements that can be stored on that stack; different stacks can have different sets of symbols. StackFlow programs should attempt to be conservative with the number of stacks they use, and the number of symbols in each stack; implementations may impose a limit on the number of stacks, the total number of symbols among all stacks, and/or the total number of rules associated with symbols and stacks. (Implementations should aim to avoid imposing limits unless they are written in a language sufficiently primitive that allowing an unbounded number of symbols or stacks would make the implementation much more complicated. Even then, they should attempt to make the limits as large as possible, and definitely sufficiently large that the language remains Turing complete.) At the start of program execution, each stack has contents specified in the program.
Each symbol of each stack is associated with a set of rules, that runs whenever that symbol is popped from that stack. The set of rules for a symbol may specify that the program halts (in which case, no other actions are allowed in the set of rules, because they would be pointless). If they don't, the rules must specify which stack the next symbol is popped from, and may specify any number of stacks, and for each such stack, a symbol to push onto it. For example, a rule might have a meaning of "when symbol B is popped from stack 1, push symbol A onto stack 2, symbol D onto stack 4, and pop the next symbol from stack 5".
StackFlow programs must be constructed so that it can be statically verified that none of the stacks ever become empty. More precisely, for each stack, the symbol at the tail of that stack at the start of the program must either push a copy of itself back onto the stack when popped (so that it cannot ever be dislodged from the tail of that stack), or else halt the program when popped. Additionally, all stacks must be initially nonempty. A StackFlow implementation should reject any program that does not obey these rules, and refuse to execute it.
Implementations should, if they can handle the extra complexity, implement the following optimizations:
- If the rules for a particular symbol of a stack push a copy of that symbol back onto that stack when that symbol is popped, there is no way that that symbol can ever be dislodged, so whenever it is pushed onto that stack, all other elements of that stack should be discarded.
- Likewise, if the rules for a particular symbol of a stack halt the program, then whenever that symbol is pushed onto that stack, all other elements of that stack should be discarded.
- If no rule allows for popping from a particular stack (other than the first), then symbols pushed onto that stack should not be stored at all. Rather, if the implementation can handle output, those symbols should be output to the user (in some suitable notation).
None of these rules are completely vital (given that none of them change the semantics of the program), and failing to follow them does not prevent a program being a StackFlow implementation, but failing to follow them will have a tendency to cause memory leaks. Implementations may also discard other parts of stacks at any time, so long as they can prove that they are unreachable and will never be popped (for instance, due to entropy-based reasoning about the particular program they are executing).
At the start of program execution, the first stack is popped, triggering whatever consequences are specified in the program for popping the symbol at its head. Then program execution proceeds via the side effects of popping stacks, forever or until the set of rules associated with a symbol cause the program to halt.
StackFlow, as defined, has no capabilities for input. If an implementation wishes to provide facilities for input, it should do so via allowing the definition of rules in which the next stack to pop form is influenced by the user.
Syntax
StackFlow has a Markdown-based syntax (being one of the few syntaxes even less appropriate for a programming language than SGML), and as such uses `.md` as its file extension. A program consists of a list of stack definitions (separated via a double newline), each of which looks something like this:
Stack 1 ------- Initial contents: `A` `B` `C` `C` `B` Rules: * `A`: push `A` on 1; push `D` on 2; pop 3 * `B`: halt * `C`: push `B` on 2; pop 1
Specifically, the first line of a stack definition contains Stack and a decimal number (which must be 1 for the first stack, 2 for the second, and so on); the second line must be made entirely from hyphens and have the same length as the first line; the third line must be blank. Then the fourth line contains Initial contents: and a (space-separated) list of symbols (the first is the tail of the stack, the last the head), the fifth line is blank, the sixth line contains Rules:, the seventh line is blank, and the remaining lines are each formed from an asterisk, a space, a symbol, a colon, and a ; -separated list of rules (that's a semicolon and a space). Symbol names consist of an arbitrary set of printable characters (other than backquotes, backslashes and vertical whitespace), surrounded by backquotes. (Although horizontal whitespace is legal in a symbol name, implementations should produce warnings upon attempts to place tab characters in symbol names.) Extra horizontal whitespace is allowed before the asterisks on the eighth line onwards, and extra trailing whitespace is allowed on any line, but otherwise, the whitespace must be exactly as shown here.
The rules themselves are of the form push `symbol` on stack number, pop stack number, and/or halt; the last rule in each set must be either pop or halt, and the others must all be push. Additionally, all mentioned stack numbers in a set of rules must be different, and halt must stand on its own.
In addition to stack definitions, the program can also contain comments; comments cannot appear inside stack definitions, only between them, and must be separated from the surrounding stack definitions via double newlines. Either the first or second line of a comment must fail to fit the syntax for the first or second line of a stack definition (respectively); there are no restrictions on the other lines (except that a double newline cannot appear inside a comment, although this is mostly irrelevant because multiple comments can appear in a row). If the first and second lines of a suspected comment look like a stack definition, it is a stack definition (or a syntax error) and not a comment, regardless of what the rest of the lines are, and regardless of whether the number on the first line is correctly in sequence or not (if it isn't, the implementation should report an error).
The definition of a "double newline" is actually a little more general than the name suggests; it must start and end with a newline, but can contain arbitrary embedded whitespace, including other newlines. This is mostly to avoid stack definitions being accidentally commented out via trailing spaces. Implementations should also take note that stack definitions contain embedded double newlines, that are part of the definition, and thus naively splitting on double newlines will not work correctly.
This specification of StackFlow does not concern itself with issues of input/output encoding; each interpreter is free to use any sensible choice, such as ASCII or UTF-8.
Computational class
6-stack construction (or 5 without I/O)
StackFlow can be proven Turing-complete via showing that any cyclic tag system can be compiled to StackFlow, making a change to the halting rules (adding an explicit halt symbol, rather than halting when the tape length drops to zero). In this construction, all the resulting programs are identical apart from the initial contents of stack 5, which specify the rules being used by the cyclic tag system in question.
Here is an example cyclic tag program compiled to StackFlow; the program is explained using comments in the program itself. (Note that StackFlow's comment syntax is particularly suited to writing literate programs.) The cyclic tag program embedded in that example is a simple nontrivial example, with rules "skip run run" and "skip skip run", but arbitrary cyclic tag programs (including those with halting and/or output) can be substituted.
Cyclic tag interpreter in StackFlow =================================== This program implements a cyclic tag system in StackFlow. The program can easily be adapted to any cyclic tag system via changing the initial contents of stack 5. This program uses 5 stacks, with a total of 20 symbols amongst them, and a total of 41 rules among all the symbols (6 stacks, 28 symbols, and 57 rules if output is desired). Cyclic tag systems ------------------ A cyclic tag system consists of an infinite, but repeating (and thus storable with finite memory), list of rules, and one queue. There are only two types of elements allowed in the queue: "run the next rule", "skip the next rule". Traditionally, each rule simply enqueues a specific sequence of elements at the tail of the queue, and the program halts when the queue becomes empty, otherwise dequeuing the head of the queue and running or skipping the next rule as appropriate. In this construction, the queue becoming empty leads to the program entering an infinite loop and never halting; instead, "halt" is a specific type of rule, as in StackFlow. This construction also allows rules that output information to the user, as an extension to the normal behaviour of cyclic tag; this makes debugging easier. Cyclic tag systems are known to be Turing complete because they can simulate regular tag sytems (which are known to be abe to simulate Turing machines): in a regular tag system, the queue holds rules instead of "run"/"skip" indications, and rather than basing run or skip based on the contents of the queue, every *n*th rule dequeued from the queue is run and the rest are skipped (with the value of *n* provided by the program). That construction is quite simple: each element of the queue in the tag system is stored as a sequence of elements in the cyclic tag system whose length is equal to the number of different rules available in the tag system, with a "skip" in all but one position, and a "run" in the position corresponding to the rule in question. The rules of the cyclic tag system consist of the rule of the tag system (encoded as explained above), followed by a number of empty rules equal to *n*-1 times the number of rules of the tag system. There is no need for a cyclic tag system to be able to specify the initial queue; this construction simply starts with a fixed initial queue of "run" (allowing the first rule to specify the initial queue). This program can trivially be generalized to allow arbitrary initial queues, though. Idea behind the construction ---------------------------- StackFlow is based on tags, but cyclic tag is based on queues: the queue that stores data is a queue directly, and the rules are also implemented as a queue, via enqueuing data as soon as it is dequeued (thus causing the rules to cycle indefinitely). This construction thus uses the well-known construction of a queue in terms of two stacks: data is dequeued by popping it from the first and enqueued by pushing it onto the second, and when the first empties, all data is popped from the second and pushed back onto the first. This accounts for four of the stacks in the construction: stacks 1 and 2 which hold the cyclic tag queue, and stacks 4 and 5 which hold the cyclic tag rules. There are two remaining stacks. Stack 6 is simply used for output, and is never popped from; it can be removed if no output is desired. The remaining stack is stack 3, used to temporarily hold a copy of the current rule (and, in a non-optimizing implementation, permanently hold copies of rules that don't run, because there is no way to pop them without running). Copying data from one stack to another reverses it (as is the nature of stacks), but this behaviour is exploited in the implementation of queues, and in the case of the symbols making up a rule, the reversal behaviour doesn't really matter; it can simply be reversed in the original stack. The rules are actually reversed four times (if a rule is executed, it's copied in reverse from 5 to 4, from 4 to 3, from 3 to 2, and from 2 to 1, meaning that the first symbol of each rule must appear nearer the head of stack 5 (even though the first rule itself appears nearer the tail). The only other complexity is in the handling of `end`, which separates rules; it needs to appear at the tail of the rule in stack 3 (because it needs to be popped after the rule itself), but also needs to appear at the tail of the rule in stack 4, for the ame reason. As such, it cannot be simply copied around. Rather, the construction exploits the fact that every rule ends with `end`; the `end` on stack 3 is added by stack 1 (when a rule is skipped) or by stack 3 (when a rule is run), rather than by stack 4 (which does most of the pushing onto stack 3). Stack 1 ------- Initial contents: `redo` `run` `skip` Rules: * `redo`: push `redo` on 1; pop 2 * `run`: pop 3 * `skip`: push `end` on 3; pop 4 Stack 1 holds the older elements of the cyclic tag queue. Popping it runs the next element of the cyclic tag queue: `run` will pop stack 3 (copying the contents of the current rule to stack 2, then popping stack 4 to move on to the next rule), and `skip` will pop stack 4 (moving on to the next rule, while leaving the contents of the current rule on stack 3 forever). When it empties, `redo` is popped, causing stack 2 to be reversed onto stack 1, and then continuing with this newer set of elements. The reason that the rule for `skip` pushes `end` onto stack 3 is that stack 4 (which is normally responsible for populating stack 3) cannot push `end` onto it because it would end up on the wrong position on that stack. When `run` is used, stack 3 is responsible for pushing the `end` onto itself, but when `skip` is used, stack 3 never gets a chance to execute anyway (nothing pops it), and so rule 1 is the only rule that gets an opportunity to push the `end`. The initial contents of the stack are designed so that at the start of the program, the first rule will run; stack 3 is meant to hold the current rule, but doesn't at the start of the program, so an extra `skip` is provided in order to load the first rule onto stack 3, and then a `run` is used to run it. Stack 2 ------- Initial contents: `done` Rules: * `done`: push `done` on 2; pop 1 * `run`: push `run` on 1; pop 2 * `skip`: push `skip` on 1; pop 2 Stack 2 holds the newer elements of the cyclic tag queue. Once stack 1 empties, it pops stack 2; then all the `run` and `skip` will be copied from stack 2 onto stack 1 (reversing the order in the process), and control will be given back to stack 1 to continue whatever it was doing before. Thus, pushing onto stack 2 has the same effect as enqueuing onto the tail of stack 1; stack 2 only exists because StackFlow only allows pushes to happen at the head of a stack. To ensure this invariant, the only rule that pops from stack 2 is the `redo` rule of stack 1. Stack 3 ------- Initial contents: `end` Rules: * `halt`: halt * `output 0`: push `0` on 6; pop 3 * `output 1`: push `1` on 6; pop 3 * `run`: push `run` on 2; pop 3 * `skip`: push `skip` on 2; pop 3 * `end`: push `end` on 3; pop 4 Stack 3 holds the current cyclic tag rule. When popped, it copies that rule onto stack 2, effectively pushing its contents onto the cyclic tag queue. The `output 0` and `output 1` rules are unnecessary, and can be deleted if no output is desired. Stack 4 ------- Initial contents: `next` Rules: * `halt`: push `halt` on 3; push `halt` on 5; pop 4 * `output 0`: push `output 0` on 3; push `output 0` on 5; pop 4 * `output 1`: push `output 1` on 3; push `output 1` on 5; pop 4 * `run`: push `run` on 3; push `run` on 5; pop 4 * `skip`: push `skip` on 3; push `skip` on 5; pop 4 * `end`: push `end` on 5; pop 1 * `next`: push `next` on 4; pop 5 Stack 4 and 5 form a circular queue that holds all the cyclic tag rules. When popped, it copies the current rule onto stack 3 (apart from the `end`, which must be added by other rules, because the `end` needs to appear at the tail of the rule rather than the head); it also copies the current rule onto stack 5, so that it can be run again; and it pops stack 1, to run or skip the rule that it just copied to stack 3. Although there are a lot of rules here, they are all of the form "*X*: push *X* on 3; push *X* on 5; pop 4", apart from `end` and `next`. The rule for `end` doesn't copy onto stack 3 (as explained above), and then moves onto stack 1, so that the next rule can be run or skipped. `next` runs when stack 4 empties, and copies all the rules back from stack 5 onto stack 4, by popping it. This keeps the rules cycling indefinitely. As always, the `output 0`/`output 1` symbols can be deleted if there is no need for output. Stack 5 ------- Initial contents: `done` `run` `run` `skip` `end` `run` `skip` `skip` `end` Rules: * `halt`: push `halt` on 4; pop 5 * `output 0`: push `output 0` on 4; pop 5 * `output 1`: push `output 1` on 4; pop 5 * `run`: push `run` on 4; pop 5 * `skip`: push `skip` on 4; pop 5 * `end`: push `end` on 4; pop 5 * `done`: push `done` on 5; pop 4 This works exactly like stack 2, serving as the other half of the queue formed from stack 4. Apart from `done`, which just gives control back to stack 4, all the rules are of the form "*X*: push *X* on 4; pop 5". (And just like stack 4, the `output 0`/`output 1` symbols can be deleted if there is no need for output.) This stack is also where the rules of the cyclic tag system are stored at the start of the program, and its initial contents can be changed to change which cyclic tag program this StackFlow program simulates. The rules are written from tail to head (i.e. left to right in the initial contents line); each rule ends with an `end`, towards the head. However, the symbols within each rule are written backwards, from tail to head; for instance, an initial contents of `done` `output 0` `output 1` `end` would output 1 and then 0. This is because `end` has special handling, and the symbols are otherwise reversed twice on their way to stack 3, and four times on their way to stack 1, and thus will run in a head-first order. Stack 6 ------- Initial contents: `0` Rules: * `0`: halt * `1`: halt This stack serves only to collect the output of the program, and is never popped. The rules and initial contents are thus entirely arbitrary; "halt" is used in order to obey the rule that the tail of the initial contents of a stack must either halt, or push itself back onto the stack. Because no rule pops from stack 6, StackFlow implementations that understand output will output anything pushed onto stack 6 to the user. If output is unnecessary, then so is stack 6, and it can be removed from the program altogether.
4-stack construction
The above construction requires 5 stacks; however, StackFlow is Turing-complete even with only 4 stacks.
Consider a machine with two stacks and two symbols available for the stacks, such that underflowing the stack isn't allowed, but you can have any number of states. This is Turing-complete, because you can compile an ordinary two-stack machine down to it by representing symbols as multiple symbols.
We want to compile such a machine to StackFlow with four stacks. Stacks 3 and 4 in the StackFlow host shall simulate the two stacks of the guest in a straightforward way, so they use the same two-symbol alphabet as the guest and the same initial contents too (plus a third halt symbol to comply with the StackFlow rule about an empty stack). Stacks 1 and 2 of the host use an alphabet with a symbol for each of the states of the guest. These latter stacks will contain garbage that we can't clean up but don't care about, only the top elements matter and those too only momentarily. The top of stack 1 is initially the symbol for the guest's initial state.
When the guest machine enters a state, we simulate that by popping the corresponding symbol from stack 1 or 2 of the host. If the guest rule for a state pushes a symbol to a stack, then the host rule for popping the symbol of that state (from stack 1 or 2) shall simulate the push by pushing the symbol to the corresponding stack, then it shall push the symbol for the next guest state to stack 1, then pop stack 1. If the guest rule for a state pops a symbol from a stack, then the host rule for popping the symbol of that state shall push the two possible next states to stack 1 and stack 2 respectively, then pop the corresponding stack. In addition, the host has the rules that if a 0 is popped from stack 1 or from stack 2, then pop stack 3; and if a 1 is popped from stack 1 or from stack 2, then pop stack 4. Finally, if the guest rule for a state halts, then popping that symbol shall halt the host as well.
This way, we can simulate any two-stack machine or Turing-machine with any initial state in 4-stack StackFlow with only linear slowdown (but potentially many symbols and excessive memory use). We could similarly simluate a machine with N stacks by a StackFlow program with (N+2) stacks.
User:b_jonas would like to know what computational complexity StackFlow with just three or two stacks has.
Direct compilation of The Waterfall Model
The Waterfall Model can be compiled into StackFlow directly. Each waterclock is compiled into a stack that supports two sorts of symbol; one of these symbols is self-pushing and only ever appears once (at the bottom of the stack), the other appears a number of times equal to the current value of the waterclock. Zeroing triggers are implemented using the rules for the self-pushing symbol (it pushes itself, then pushes further elements onto itself and onto the other stacks to represent the topping-up of waterclocks). These stacks are arbitrarily arranged into a circular sequence, and every symbol rule in the construction finishes via popping the next stack in sequence. As a result, the stacks are always checked for zero-ness in sequence, decrementing them in the process (implementing the steady decrement), and the order of the checks does not matter because The Waterfall Model disallows two waterclocks from being decremented on the same cycle. Halting waterclocks can be implemented via replacing their self-pushing symbol with a halt-rule symbol instead.