Re: [game-lang] review of GDL

[Simon McGregor <londonien@xxxxxxxxx>]

On Tue, Aug 3, 2010 at 12:53 PM, Joel Uckelman <uckelman@xxxxxxxxx> wrote:
> Thus spake Simon McGregor:
>>
>> >> [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.
>
> I was hoping that we'd be able to avoid writing even a single-step model
> checker. (To be clear: In this context, model checking is the problem of
> determining whether a given game state is reachable via finitely many legal
> moves from the initial state, while single-step model checking is the
> problem of determining whether state B is a legal successor of state B.)
> I've never written a model checker myself, but my impression is that it's
> quite a task.

Well, one desideratum is that (in at least some cases) it should be
possible to automatically generate a finite list of available moves
from the rules. This is at least as difficult a task as model checking
(as you've described it), so we need to think carefully about how to
go about it.

>> 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.
>
> I'm struggling to think of any game where you would actually need AC in
> the statement of the rules (unless it's a concocted example). You might
> think of a sequence of dice rolls as a choice function, but that only
> requires finites choice, which you get already from ZF.

Agreed.

>> * 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.

> I would call these "implicit" instead.

Yes, perhaps that's clearer.

>> * 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).
>
> It's not too hard to build epistemic models where you don't have finite
> information sets, IIRC. I'm guessing that you could also build ones where
> you not only don't have finite information sets, but the information sets
> aren't even recursively enumerable, so you couldn't even get a nice finite
> representation of them...

>>   * A proof in ZF(C?) that the algorithm always terminates correctly
>> given the rules of the game.
>
> While we might be able to always have an algorithm which terminates,
> I don't expect that we will be able to get a proof of this; it looks
> the same as the Halting Problem to me.

If the rules are written in ZF with no other constraints, then there
is clearly no algorithm which can correctly enumerate all the possible
moves from a given state (and consequently no proof that any algorithm
is correct, assuming ZF is consistent). This is because you can
specify a game whose next state depends on whether the nth Turing
machine (in some suitable enumeration) halts with itself as input.

On the other hand, I'm imagining that a sufficiently well-behaved
logic will correspond to a set of computable constraints on the syntax
of the rules. Consequently, the algorithms which handle that logic
will both correctly enumerate the moves and also be provably correct
(assuming the syntactic restrictions). Or is that a terribly naive
view?


Simon
_______________________________________________
game-lang mailing list
game-lang@xxxxxxxxx
http://lists.ellipsis.cx/mailman/listinfo/game-lang