Joel Uckelman on Tue, 3 Aug 2010 04:53:25 -0700 (MST)


[Date Prev] [Date Next] [Thread Prev] [Thread Next] [Date Index] [Thread Index]

Re: [game-lang] review of GDL


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

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

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

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