Well, the proof is contrived, but that's not the point: it's also unnecessary
and it may also be insufficient.
To claim a system is Turing complete, what you need is (a) a store, from and to
which you can read and write; (b) branching (if-statements); and (c) the
ability to repeat instructions an arbitrary number of times (while-statements).
It's easy to show that M:tG has all of the above: the Stack is a store; you
read from and write to it when you place abilities on and resolve them from
it. Branching and loops are present in ability text sentences like the
following:
You win the game if you control a land of each basic land type and a creature
of each color. [1]
When you cast this spell, copy it for each spell cast before it this
turn. [2]
As to a demonstration that the system actually works- you can point to any
M:tG game.
Finally- the proof in the OP may not be general enough. It uses only a limited
sub-set of M:tG cards, so the best we can tell is that that specific sub-set
of M:tG cards is Turing complete. For a more general proof, you at least have
to explain why a specific subset is chosen and explain why you can substitute
it with any other subset without loss of generality.
The problem is that "card" is not a granular enough unit of the M:tG game to
define as a symbol of an alphabet. A really general proof would make use of
tokens of the ability text language. Such a proof would hold for any set of
cards.
A formal system, in this case the game, is Turing complete if it can be used to implement a Turing machine. Complaining about using only a limited and very specific subset of available cards in a contrived way is like saying that a computer is not a computer because a large number of transistors aren't part of it, and if I rewire it randomly it ceases to work.
Regarding "unnecessary", unlike typical competitive or recreational games in which players often do what they want, this particular setup results in an automaton in which players cannot disrupt the operation of the Turing machine:
"The idea of my Magic Turing machine is that the players do nothing at all, except when the game offers them a choice."
The article explains that the setup only allows choices to do optional actions, and it is assumed the players always do them. As "programming" human players to simulate a Turing machine would be too easy, they are replaced by mindless placeholders.
If you used humans, they could follow the rules in their head (with written reference sheets); tapes could be lines of objects belonging to an alphabet of different types (e.g. coins of different countries and denominations, Barbie dolls of different model years, wax crayons of different colours), and the machine head would move by walking in front of the next tape position. No need to involve a proper formal system like a card game.
>> The article explains that the setup only allows choices to do optional actions, and it is assumed the players always do them. As "programming" human players to simulate a Turing machine would be too easy, they are replaced by mindless placeholders.
Yes, I read that bit - I didn't realise it was meant to make things "harder". That alone is good enough to convince me the proof is unnecessary. If you can make a proof easier, then you make it easier. There's no need for harder proofs.
Also, the fact that the proof does not involve human actions is another piece of evidence against the generality of the proof. You can model human choices as a distribution and allow for a fully-automated proof, that doesn't require human input in the strict sense. But leaving human actions out of the proof makes it less general- because the full game does involve such actions.
For Turing completeness it is not sufficient to demonstrate that a system has "a store". The store needs infinite capacity and random access. Infinite capacity alone is not enough - a stack has infinite capacity but a stack machine has demonstrably weaker expression power than a Turing machine: https://en.wikipedia.org/wiki/Pushdown_automaton
Same goes for if-statements. The statements need to be general enough and work with the rest of the system to be usable to express the Turing machine. In particular your example of an if statement that starts "you win the game if..." makes this statement sorta useless, as it ends the computation. You can't make a Turing machine if every "if" ends the program. Same goes for any other "if" in the rules - they are usually pretty limited.
"As to a demonstration that the system actually works- you can point to any M:tG game."
Again, that alone is not sufficient. It only proves that the system works for expressing one kind of computation, namely MtG games. For Turing completeness, you need to demonstrate that any Turing machine computation can be expressed as an MtG game, which is what the linked proof does.
There's no limitation on the size of the M:tG Stack, so it is infinite. Also, that M:tG uses a Stack as a store doesn't make it a pushdown automaton. For a pushdown automaton you need the stack to control decisions, but that is not the case here- there's still player actions and the effects of cards in the game etc.
The if-statement I quoted is just one example. The following does not end the game:
At the beginning of your upkeep, draw a card if you control the creature with the greatest toughness or tied for the greatest toughness. [1]
The important thing to note of course is that the above are well-formed sentences in the ability text language. So the language allows if-statements and it doesn't matter how many cards with if-statements are actually printed.
Also, strictly speaking, winning the game doesn't necessarily terminate processing. The ability of the card Shahrazad [2], for instance, creates a sub-game that may end without ending the original game:
Players play a MAGIC subgame, using their libraries as their decks. Each player who doesn't win the subgame loses half his or her life, rounded up.
Like I say, if you can show that the system has the components it needs to be Turing complete, then you've shown that it is Turing complete. Simulating a Turing machine is just another way to show Turing-completeness.
"The language allows if-statements and loops" is not sufficient for the language to be Turing-complete. A language with loops in which the only form of selection is "if 4 > 3 then…" is not Turing-complete. Just pointing to a specific if-statement appearing on a card and saying "yeah, that's probably enough to make Magic Turing-complete" does not constitute a proof.
I think you might be confused by the term "language". In the context of the proof, "language" means "anything that is the Oracle text of a card". You seem to be using it as "anything that could be printed on a card". I think you're saying "the game of Magic-but-where-I'm-allowed-to-choose-what-the-cards-say is Turing complete", which is undeniably true but also not the point.
Yes, that's exactly what I'm saying- why is it not the point? If you were
trying to prove that Java is Turing-complete you wouldn't look at all the Java
programs ever written and try to build a Turing machine with those programs.
Instead, you'd use the symbols in the language to write a (new) program that
simulates a Turing machine, or a set of functions that suffice to prove Turing
completeness.
The proof the author has given is equivalent to building a Turing machine out
of existing programs in his language of interest. M:tG cards have instructions
printed on them in the ability text language - so those instructions, rather
than the cards themselves are the symobls in the language. The cards are best
seen as scripts or small programs written in that language.
But why should anyone restrict themselves to existing cards when trying to
prove the Turing completeness of the language?
Note, also, that the rules of well-formed sentences in the ability text
language are given in the M:tG Comprehensive Rules or at least some of them
are- there's no complete formal definition of the language. Still, there's
plenty enough for anyone to be able to form syntactically correct
ability text.
So, again- if you're trying to prove the Turing completeness of a language,
why would you not use the full expressive power of the language to compose new strings? And instead
restrict yourself to just a few pre-existing strings of it?
The game of 'Magic: The Gathering' consists of both the rules and the cards available in it (which are written in a kind of language). If you are printing your own cards, most players would agree you are not really playing 'Magic: The Gathering', but your own homebrew game based on it.
Maybe, but if we're doing formal proofs then we're not in the realm of opinion anymore. So the point is to substantiate any claim as to what, exactly, is reasonable to call "the mtg language". I really doubt there's any context in which a language can be formally described as "a limited number of texts"... especially if that language is supposed to be Turing complete (which implies non - finite-ness) !
As to the relation between the language and the rules, if you think about it, if the language is not equivalent to the rules, then it can't represent (and, therefore, modify) every rule in the game (as it is supposed to). And if the language and the rules are equivalent, then proving one is Turing complete also proves it for the other. So you can ignore the rules and focus any proof on the language.
Just to make it plain. In formal language theory, a language is a set of symbols and a set of rules that determine what is a valid string.
Given such a definition of the ability text language, you don't need to restrict yourself to only those strings that are actually printed on cards.
In the same sense, we don't define the English language as every text ever written in English - but as some unknown formal system that can produce an unknown, probably infinite, number of strings that includes all text ever written in English.
To claim a system is Turing complete, what you need is (a) a store, from and to which you can read and write; (b) branching (if-statements); and (c) the ability to repeat instructions an arbitrary number of times (while-statements).
It's easy to show that M:tG has all of the above: the Stack is a store; you read from and write to it when you place abilities on and resolve them from it. Branching and loops are present in ability text sentences like the following:
You win the game if you control a land of each basic land type and a creature of each color. [1]
When you cast this spell, copy it for each spell cast before it this turn. [2]
As to a demonstration that the system actually works- you can point to any M:tG game.
Finally- the proof in the OP may not be general enough. It uses only a limited sub-set of M:tG cards, so the best we can tell is that that specific sub-set of M:tG cards is Turing complete. For a more general proof, you at least have to explain why a specific subset is chosen and explain why you can substitute it with any other subset without loss of generality.
The problem is that "card" is not a granular enough unit of the M:tG game to define as a symbol of an alphabet. A really general proof would make use of tokens of the ability text language. Such a proof would hold for any set of cards.
___________
[1] Coalition Victory: http://gatherer.wizards.com/Pages/Card/Details.aspx?multiver...
[2] Storm keyword ability; e.g. Dragonstorm: http://gatherer.wizards.com/Pages/Card/Details.aspx?multiver...