Re: [game-lang] review of GDL

[Simon McGregor <londonien@xxxxxxxxx>]

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