Simon McGregor on Wed, 28 Jul 2010 04:07:04 -0700 (MST) |
[Date Prev] [Date Next] [Thread Prev] [Thread Next] [Date Index] [Thread Index]
Re: [game-lang] review of GDL |
So, I've been thinking about this further. The fluent calculus looks promising, but I'll leave it to someone better qualified to evaluate. I'm taking netiquette liberties again by replying to different peoples' comments in one post... >> [Joel said] >> Now, you might ask whether this actually matters for modeling *games*. >> I don't know of any board games which involve determining whether an >> aribtary program will halt or doing proof search, so the answer might >> just be that it doesn't matter at all---we're not going to use enough >> of the expressivity to get us into trouble, but at the same time we >> don't want to go through the trouble of coming up with precise boundaries >> within which safety is guaranteed, so we don't bother limiting the >> expressivity... My opinion is now strongly that we shouldn't do so; it's perfectly possible in principle to come up with unambiguous natural-language rules for valid game-theoretical boardgames which turn out to be undecidable in the general case. In practice, in the rare events that it looks like this might be happening (or when the rules imply something perfectly logical but gameplay-ridiculous, such as putting a trillion counters on each square), the game is deemed "broken" and a rules fix devised. >> [Joel said] >> I think a bigger problem comes up if you want to use existing tools for >> doing model checking or theorem proving, as they might not support the >> level of expressivity we're aiming at. Hard to tell at this point, >> though. Again, I'm of the opinion that this shouldn't shape our language design. Suppose that some abstract game has rules which are provably decidable in ZF, but not in first-order predicate calculus. I'm proposing that it should be possible to express the rules in our language, and we should just have to wait for advances in theorem-proving software before we can validate the rules automatically. It would be a really worthwhile accomplishment if we could devise a generic way to interface the language to logic tools, so that the games which don't use dangerous logical constructs can apply existing tools. If we decide to make the language sufficiently expressive to allow undecidable rules (which would be my current preference), then figuring out how to still allow existing tools to be used (in the cases where we can prove it's safe to use them) should factor into our language design. For instance, applying tool T (which uses logic L) to game G would come back with either something like "G's rules are decidable - see log for details" or "G uses construct X which is not modellable in L". Formally speaking, here's something like the most extreme and expressive case anyone is ever likely to want: * Rules are defined in some ZF(C?)-equivalent formal system. Possible moves are implicitly or explicitly modelled as sets. * Any set (e.g. the integers) can be labelled "exportable" - this means that the elements of the set will not be individually enumerated when describing it to a player. GUI programs, certain logic tools and AI programs will reject games which export sets that the program doesn't recognise. * A game is deemed "complete" if it comes with the following things: * Some algorithm for listing possible moves (as an enumeration of exportable sets and individual moves) in a given game-state, and the (possibly stochastic) consequences of those moves on the game-state (including information sets). * A proof in ZF(C?) that the algorithm always terminates correctly given the rules of the game. Obviously, this is an outrageously general formulation, but it forms one end of the expressivity spectrum (one where no algorithm can be guaranteed to find how to make a game "complete" or even determine whether a game can be made "complete"). > [Marc] > Yes. IIRC, this was similar to their argument at last year's general > game-playing workshop. "It [arithmetic] makes resolution much harder" is > what I kept hearing them say. That's precisely where I lost interest because > I'm not interested in the purity of the logical properties of the language > for uses that are irrelevant to our purpose. > > I just want to be able to express a game comfortably (e.g. having arithmetic > should not be a luxury.. it should be given), know what state I start out > in, know which moves are available to me in a given state, know how my state > changes when I take one of those moves, and know how I win or lose. Of > course we want to add our high-level board gaming concepts on top of this. If I understand correctly (Joel, please correct me!), I think the problem is as follows: having the whole of integer arithmetic allows you to construct rules where it's theoretically impossible to compute which moves are available in a given state, or how the state changes when you take a given move. At the moment, I'm leaning towards "yes, that's just an unfortunate fact about games, and programmers will have to be careful they don't specify undecidable rules" rather than "let's find some restrictions on integer arithmetic which make it easier to reason about", for the comfort reasons you describe. Simon _______________________________________________ game-lang mailing list game-lang@xxxxxxxxx http://lists.ellipsis.cx/mailman/listinfo/game-lang