StackFlow

From Esolang
Jump to: navigation, search

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.

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 line 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

StackFlow is 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.

Implementing StackFlow in Magic: the Gathering

In order to create an implementation of StackFlow using Magic cards, we need some way to represent stacks, and some way to represent rules, that compute according to the rules of the game. The computation is done entirely using triggered abilities, with no choices to be made by any player, and requires only two players. (It can be seen that StackFlow works in quite a similar way to triggered abilities in Magic already; everything happens as a consequence of stack elements being popped, including the popping of other stack elements.)

A method of representing stacks in Magic, due to Alex Churchill, already exists; a stack is represented using a creature for each stack element, with the creature's creature type representing the symbol, and the creature's toughness representing the distance from the head of the stack. (Toughnesses can go unboundedly high in Magic, meaning that we can track the order of an unlimited number of stack elements.) We use a toughness of 3 for the head of the stack, to prevent creatures dying incidentally as a side effect during other actions. All these stacks are controlled by the same player (and all the events take place on the other player's turn).

We use a different creature type for each symbol of each stack. Additionally, for each stack symbol, we use an additional creature type, which is given to all creatures in that stack. Our creatures are generated as tokens with only one creature type, but because which stack a creature belongs to is entirely defined by that creature type, we can grant the other creature type using copies of Dralnu's Crusade (with their text altered using Artificial Evolution in order to make them refer to different creature types), to create static "all Xs are Ys" effects. Dralnu's Crusade also has two other effects; the color-changing effect is irrelevant in this construction, but the +1 to power and toughness that it gives is relevant, and thus is cancelled out using Engineered Plague set to the same creature type. (In order to create the large number of enchantments with the same name required without running afoul of deck construction rules, the enchantments are temporarily enchanted using Opalescence, allowing token copies of them to be created using cards like Rite of Replication, which can be repeatedly salvaged from the graveyard and re-cast using cards like Elixir of Immortality; Opalescence can be destroyed again when we're done in order to make the enchantment creatures back into enchantments.)

For each of the creature types that represent stacks, there is a Noxious Ghoul which is altered using Artificial Evolution to look at that creature type, controlled by the active player (the opponent of the player who controls all the stacks), and protected from the effect of the other Noxious Ghouls via giving it all creature types using Blades of Velis Vel. The inactive player controls one copy of Cathars' Crusade. The combined effect is that whenever a creature enters the battlefield on one of the stacks, all creatures on the stacks will become tougher by 1 (due to the effect of Cathars' Crusade), and then all creatures on all other stacks will become less tough by 1 (due to the effect of Noxious Ghoul, which resolves later due to being controlled by the active player and Magic's tiebreak rules for simultaneous triggers.

For each stack, we add one further symbol, a "blank symbol", with a creature type to match. Unlike regular symbols, we put sufficiently many copies of Engineered Plague on the battlefield, set to that symbol's creature type, so that any 2/2 token creature of that type dies instantly upon being created. Creating a creature of the blank symbol type, therefore, will increase the toughness of all creatures in that stack without adding any new creatures to the stack. This effect can be used to adjust the toughness at which a stack starts, increasing it by 1.

We also need to be able to adjust the toughness at which a stack starts in the other direction (so as to be able to pop a stack via reducing it to 0). To do this, we use a creature type that is not used for any other purpose, and have a Noxious Ghoul set to that creature type (owned by the inactive player), together with two Engineered Plagues that are also set to that creature type. This means that creating a 2/2 creature token of that type under the active player's control will cause all creatures on the stacks to get -1/-1. In order to decrease the toughness at which a stack starts by 1, it suffices to increase the toughness at which all other stacks start by 1 (via pushing blank symbols onto them), then decreasing the toughness at which all stacks start by 1.

Finally, all that we need is a method of creating specific creatures, in a specific order, under specific controllers, whenever a creature of a specific type dies, noting that we only need a construction for the case where the creatures owned by the active player (which push symbols or blank symbols onto the stacks) are created before the creatures owned by the inactive player (which symmetrically pop all stacks). We achieve this using a series of Rotlung Reanimators (protected from Noxious Ghouls using Blades of Velis Vel):

  • For the "push"/toughness increase rules, we have one Rotlung Reanimator controlled by each player; the copy controlled by the inactive player resolves first and creates the required token, while the copy controlled by the active player resolves second, and creates a creature of an otherwise unused type, which has sufficiently many copies of Engineered Plague pointed at it that it instantly dies, just like the blank symbols do. The death can be triggered on recursively, meaning that any number of "push" rules can run in response to a death, and in a specific order.
  • For the "pop"/toughness reduce rules, we have a Rotlung Reanimator controlled by the active player; it creates a token of an otherwise unused type, and that type has a Dralnu's Crusade causing it to additionally be of the global-toughness-decreasing type, and sufficiently many Engineered Plagues set to that type that it has 0 toughness upon creation (and thus dies as soon as state-based actions are checked). However, the Reanimator does have to wait for state-based actions, whereas the Noxious Ghoul that looks at the global-toughness-decreasing type triggers as soon as the token is created, and thus the Reanimator's effect enters the stack second and so resolves first. The result is that we can chain any number of Rotlung Reanimator triggers (ending in the last rule of a sequence, for which the created token is of a type that no Rotlung Reanimator triggers on); the Noxious Ghoul triggers build up below them on the Magic stack, and then all resolve at the end of the ruleset.

Now all we need to do is to be able to encode rules as a sequence of triggered abilities. For each symbol of each stack, we arrange that when a creature of the type that represents that symbol dies, the following events happen in order:

  • Two blank symbols are pushed onto that stack (because the head of stack will have toughness 1 after it is popped, and the head of a stack is supposed to have toughness 3, so we need to add two in order to get it to where it should be);
  • For each symbol that that rule pushes onto a stack, a token of the corresponding creature type is created (a "push" rule);
  • For each stack that is not popped by the rule, three blank symbols are pushed onto that stack;
  • All creatures on the stacks have their toughness reduced by 3.

At first, it seems that this would require a great many creature types to trigger on. However, the last step is shared between all rules, and the penultimate step is shared between all rules on a stack. Thus, the total usage of creature types is:

  • 1 per stack (the creature type common to all symbols on that stack);
  • 1 per symbol (the creature type for that symbol);
  • 1 (the global toughness decreasing symbol);
  • 1 per symbol (the second of the two pushes that occur when that symbol is popped; the first does not need a creature type of its own because it triggers on the symbol itself);
  • 1 per "push" rule (the push that that rule causes);
  • 3 times (the number of stacks minus 1) per stack (the blank symbol pushes);
  • 3 (the triggers for the global toughness reductions).

Given t stacks, y symbols, r rules, this gives a total usage of t + y + 1 + y + (r - y) + (3t(t-1)) + 3 = 3t² - 2t + y + r + 4 creature types. For the cyclic-tag-in-StackFlow program above, we have t = 5, y = 20, r = 41, for a total usage of 130 creature types; large, but not so large that it is impossible to find enough creature types to implement the program. (This construction does not attempt to implement output, nor any of the optimizations suggested above.) The actual required usage is in fact 129, because halt rules have no reason to maintain the invariants on the toughness of the head of the stack; thus, there is no symbol required for the second push of the halt rule, because it can be omitted without causing issues.

Finally, we need to handle the start and end of the program. Starting the program is simple enough: we get all the stacks set up appropriately (via token creation and manually placing counters); place, copy, and edit the text of all the support cards (the Dralnu's Crusades, Engineered Plagues, etc.); float a huge amount of mana; ensure nobody has any cards remaining in hand apart from the cards needed to fulfil the rest of these steps; destroy all irrelevant permanents (e.g. with a combination of Oblivion Stone and Armageddon); exile all cards from graveyards that have any abilities that have an effect from there (if any were used to set the gamestate up), e.g. via Tormod's Crypt; and finally "manually" pop stack 1 via simultaneously reducing the toughness of all the creatures in it (and no other creatures) by 3, with the last remaining card in the any of the players' hands, and spending all the resulting mana. Although it is awkward to get such a specifically targeted toughness reduction, we can use damage instead (a creature which has taken 3 damage acts identically to a creature whose toughness is 3 lower for the purposes of this construction); there are many cards that can accomplish this (such as the classic Fireball, given enough mana).

For ending the program, we need to implement halt rules, in addition to the implementations of push/pop rules given above; that is, implement "whenever a creature type dies, a specific player loses the game". This can be accomplished using Vengeful Dead, the same way as in Alex Churchill's construction, which directly kills a player on 1 life (and is protected from Noxious Ghouls using Blades of Velis Vel, as with the other creatures that exist only for their triggered ability), and it is simple enough to arrange for the players to be on 1 life in advance. One interesting extra possibility to note is that who wins the game depends on the controller of the Vengeful Dead, which otherwise doesn't matter, and thus different "halt" rules in the program can cause different players to win.

Taken together, all this constitutes a proof that there are Magic gamestates for which the eventual outcome of the game (win, lose, or draw) depends on an arbitrary computable unsolved problem. In fact, because the players have no further decisions once the machinery of the abilities has been set in motion (and with no cards in hand nor relevant abilities they can activate), the players can simply announce that they are passing priority until the end of the turn (explicitly permitted by the Magic tournament rules), at which point the game immediately ends, but it may require solving an arbitrarily difficult problem in order to determine which of these events actually happened; although the rules oblige players to attempt to break up infinite loops, this restriction does not exist when the players have no opportunity to do so.

External resources