Re: [game-lang] review of GDL

[Simon McGregor <londonien@xxxxxxxxx>]

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