Simon McGregor on Wed, 28 Jul 2010 07:39:03 -0700 (MST) |
[Date Prev] [Date Next] [Thread Prev] [Thread Next] [Date Index] [Thread Index]
Re: [game-lang] review of GDL |
On Wed, Jul 28, 2010 at 12:06 PM, Simon McGregor <londonien@xxxxxxxxx> wrote: > 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. Better than these "completeness" criteria would be an "overseer" X consisting of a generic move-listing algorithm X_moves along with a rule-checking algorithm X_check. * X_moves(game-state G) is, under fairly general conditions C on the rules, provably guaranteed to correctly terminate (preferably in polynomial or even log-linear time) outputting the list of legal moves in game-state G and their (stochastic) consequences for the next game-state (including information sets). * X_check(rules R) is provably guaranteed to correctly terminate (again, preferably quickly) for all rules, describing whether they meet conditions C. * The proofs could (initially) be checked by humans rather than machine, which avoids incompleteness problems by not specifying the formal system in which the proofs are written. Rules would be written to be "safe under X", i.e. X_check(R) would be required to output True, and X_moves would be used for listing and processing moves. But the language would be designed to permit later rules to be declared "safe under Y" when someone designs and implements a better overseer Y (or one devised specifically for a tricky set of rules - it could even be so specific that Y_check(R) = (R==r) for some specific r, providing the associated proof is sound). I think this might be my ideal for the language. We could start with X being based on a first-order fluent calculus, but use a syntax which allows in principle for more expressive logics. Improving the overseer to handle some adequate version of integer arithmetic in the game-states would be a high priority. (I don't know what version, but 99.999% of games using integer arithmetic don't have rules which depend on universal quantifiers over the entire set of integers, so that's a possible start.) For fast-and-loose programmers, there could also be some generic overseer P for listing moves, where P_moves is not guaranteed in general to terminate; they'd be taking the risk of writing uncomputable rules (declared "risky under P"). How does that sound? Simon P.S. Now all we have to do is devise a nice intuitive syntax for a category theoretic language, which abstract board-game components can easily be implemented in :-P P.P.S. No. Just say no. _______________________________________________ game-lang mailing list game-lang@xxxxxxxxx http://lists.ellipsis.cx/mailman/listinfo/game-lang