Lambda the Ultimate

Andris Birkmanis: Compare to a paper by Andreas Blass, who studies game semantics in a context of linear logic and (therefore?) limits interactions to "turn-based" (only one side has legal moves at each position - client/server paradigm).

I'd be interested in knowing whether it really is "therefore" or not, as I'm keenly interested in logics that can cope with uncertainty in multi-agent environments. So far, those sound like modal logics, but if I'm in error on that point, I'd be grateful for knowing it.

I'd be interested in knowing whether it really is "therefore" or not, as I'm keenly interested in logics that can cope with uncertainty in multi-agent environments.

I am still learning, and I am not a full-time student :( What's probably relevant, Japaridze treats ∃ and ∀ as blind quantifiers, as opposed to other, choice quantifiers:

The meaning of ∀xA(x) is similar to that of ∩xA(x), with the difference that the particular value of x that the user “selects” is invisible to the machine, so that it has to play blindly in a way that guarantees success no matter what that value is. This way, ∀ and ∃ produce games with imperfect information.

It may be worth to note that early papers by Japaridze have "modal logic" in their titles.

You may want to check the latest paper on computational logic for more technical results.

What bothers me, is how to introduce multiple agents. It may be obvious, but it eludes me. Then again, CL is geared towards global duality/simmetry, which is (IMHO) not well suitable for multi-agent environment, but that's only an intuition...

If you've been following Tim's postings here, I'd say it doesn't sound like we'll have to wait for 2010!

Well, the only recent post by him I read was about Icon(?)-inspired language.

And from official PR I am getting impression that Unreal 3 is more about "physics" and graphics, than logic(s). I don't expect games to prove (non-trivial) theorems in real time (yet). On the other hand, I have no clue, AIs in current games must do some planning, does it count as proving theorems?

Andris Birkmanis: Well, the only recent post by him I read was about Icon(?)-inspired language.

Right, but he's written about language design a few other times; googling "site:lambda-the-ultimate.org tim sweeney" is interesting. He also posts to the Haskell list from time to time.

Andris: And from official PR I am getting impression that Unreal 3 is more about "physics" and graphics, than logic(s).

Yes, but I don't expect it to be eight years from the time the first title based on Unreal Tech 3 ships to the time Tim uses his new language.

Andris: I don't expect games to prove (non-trivial) theorems in real time (yet). On the other hand, I have no clue, AIs in current games must do some planning, does it count as proving theorems?

In some sense. But I don't think Tim's interested in writing theorem provers, although his new language might make a good meta-language for doing that, just as ML or Haskell do. But also like ML and Haskell, the range of applicability of Tim's language should be quite a bit broader. What's been fascinating to me lately here on LtU have been the posts about type-safe network interaction, type-based information flow security, type-safe module upgrade and rebinding, type-based proof of lack of deadlock/race conditions... all things guaranteed to make a game developer's ears perk up, especially if that game developer's titles are involved in professional gaming leagues (yes, they exist) and/or the developer partners with other sponsors of events where cheating/hacking leads to people losing real money. I have to imagine that Tim's paying a lot of attention to these things as well, but obviously I can't speak for him.

I'm only half-following this conversation, but this reminds me of Harry Mairson's work:

• From Hilbert Spaces to Dilbert Spaces: Context Semantics Made Simple
• Slides (17MB!)

Warning: I think "made simple" is a euphemism for "freaking hard."

A quote from the paper:

just as the classical physicist (or freshman physics student) views the world via a model of massless beams and frictionless pulleys, and as machine architects have the Turing machines as their essential, ideal archetype

Hurray, Turing machine as an ideal, again.

PS: the paper is quite interesting, by the way. It reminds me of Interaction Combinators by Lafont (probably because both are inspired by Girard's GoI). ON EDIT: by "the paper" here I meant "Hilbert Spaces to Dilbert Spaces", not the computability logic paper.

Thanks for posting this.

You are very welcome. I am almost as proud as if I wrote the paper :)

Did it turned good after reading the remaining three quorters?

I would very much like to see an extension of CL to multi-party interactions... Got to figure that myself, I guess...

PS: sorry that I bumped this thread, didn't get to read your comment until now - looking for continuation-based semantics in UML state machines bogged me down :)

I'm interested to see how it is different from linear logic

Now that I returned to learning about logics, I found there are many views on what is the linear logic.

As a sequent calculus, I think CL is somewhat similar to Guglielmi's calculus of structures because of deep inference (and yes, that was mentioned in the OP, but I made the whole circle and found it out the hard way).

One of the differences between CL and CoS, though, seems to be that CL looks only at "surface occurrences" of choice connectives, while CoS (I am not sure about that) takes "deep" more literally.

This somehow reminds me of contexts for delimited continuations...

And the relation seems quite simple

Let's make it more explicit. Define LWn as:

LWn run = case Lr run of {true -> Wn run; false -> false}

or, using the usual shortcutting &&(and further departing from Epigramic spirit)

LWn run = Lr run && Wn run

The question is, whether a game can be defined (for the purposes of CL) not as a pair (Lr, Wn), but as a single LWn? In programming terms, what is the signature, and what is the implementation details? Due to the implications of halting problem, I believe that (Lr, Wn) contains more information than LWn, but is this information used by CL?

I see two possibilities:

1. All theorems of CL can be redefined to use only LWn without need for Lr.
2. Some theorem needs Lr.

Let's focus on the second possibility. Lr has two nice properties, leading to the third:

!(Lr run) => ∀tail: !(Lr (run # tail))

!(Lr run) => !(LWn run)

---

!(Lr run) => ∀tail: !(LWn (run # tail))

If it is crucial to know value of (Lr run) as opposed to (LWn run), then it means we are interested in the third property, that is, loss of all possible continuations of the run, deducing which from LWn is (probably) equivalent to halting problem.

Before going through all the theorems to verify, whether some of them needs the third property, I speculate further that it would be more natural to expect it to need another property instead (Decided run):

(Dr run) <=> ∀tail: (LWn (run # tail))

PS: Yes, I am trying to use LtU for the purpose expressed in its title :-)

PPS: Lr is a set of runs, but I use functional notation pretending it is a predicate (meta-predicate, if you wish, as it is living outside of CL and returns true/false not T/⊥).

As I understand it, if a player makes an illegal move, that counts as a win for its opponent. Similarly, if a player fails or refuses to move, that also counts as a win for the opponent.

That suggests that a winner can be determined for (almost) every run: Whichever player made the last legal move has won. So, Wn can be derived from Lr.

(Problems: Who wins the empty run? Are there runs with no winner?)

Thanks for participating!

As I understand it, if a player makes an illegal move, that counts as a win for its opponent.

Yes, and if we are just interested in who won the run (as opposed to "hope" to ever win "ultimately"), we can combine Lr and Wn into LWn, as I proposed.

Similarly, if a player fails or refuses to move, that also counts as a win for the opponent.

There is a problem here if we are talking about real time: when the opponent wins? Looks like immediately on his last move. It may look unconventional to talk about victory changing hands on (potentially) every move, but this is the only way I see. This victory is encoded in Wn. And when we see that in all extensions of the given run the winner always remains the same (think temporal logic), this is the victory in the conventional sense. This victory is partially encoded in Lr - partially, because Lr may say the run is legal, but still there is no hope for the player who did the last move (Lr works the other way - if there is any hope, Lr will accept the run). Intuitively, it means that Lr is not precise enough, and can be constructed arbitrarily imprecise (e.g., accepting all possible runs), that's the reason why I think it is not needed for the theory (though might be improving usability :) ).

That suggests that a winner can be determined for (almost) every run: Whichever player made the last legal move has won. So, Wn can be derived from Lr.

Not exactly, in free games a player might need to make multiple moves before reaching (temporary) victory.

(Problems: Who wins the empty run? Are there runs with no winner?)

Do you mean in the modified theory (without Wn?)?