Home

In the beginning was game semantics

In the beginning was game semantics

Giorgi Japaridze

[...] the story and philosophy of computability logic (CL) [...]
According to its philosophy, syntax — the study of axiomatizations or any other, deductive or nondeductive string-manipulation systems — exclusively owes its right on existence to semantics, and is thus secondary to it. CL believes that logic is meant to be the most basic, general-purpose formal tool potentially usable by intelligent agents in successfully navigating real life. And it is semantics that establishes that ultimate real-life meaning of logic. Syntax is important, yet it is so not in its own right but only as much as it serves a meaningful semantics, allowing us to realize the potential of that semantics in some systematic and perhaps convenient or efficient way.
[...]
the philosophy of CL relies on two beliefs that, together, present what can be considered an interactive version of the Church-Turing thesis:
Belief 1.
The concept of static games is an adequate formal counterpart of our intuition of ("pure", speed-independent) interactive computational problems.
Belief 2.
The concept of winnability is an adequate formal counterpart of our intuition of algorithmic solvability of such problems.
I already posted links to papers of Giorgi Japaridze several times, but most of them were pretty technical, and also that was before the latest expansion of LtU's readership.

In short, CL is about trying to generalize traditional (both classical and intuitionistic) logic beyond batch computation (well, I hope everybody knows why logic is relevant to computation, if not - look for Curry-Howard isomorphism, or CHI). There are several approaches to doing that, but Giorgi believes they go the wrong way by trying to build upon the syntax, while it's semantics that is primary.

If you believe that computation is more than calculating a function, and that logic is a good way to understand computation - then I recommend to read at least the introduction and the references' list of this paper (the paper is a single chapter for a book, would love to see the whole book).

By Andris Birkmanis at 2005-11-21 20:14 | Semantics | other blogs | 11862 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Introduction to Cirquent Calculus and Abstract Resource Semantic

Introduction to Cirquent Calculus and Abstract Resource Semantic
This paper introduces a refinement of the sequent calculus approach called cirquent calculus. While in Gentzen-style proof trees sibling (or cousin, etc.) sequents are disjoint sequences of formulas, in cirquent calculus they are permitted to share elements. Explicitly allowing or disallowing shared resources and thus taking to a more subtle level the resource-awareness intuitions underlying substructural logics, cirquent calculus offers much greater flexibility and power than sequent calculus does.
[...]
Removing contraction from the full collection of its rules yields a sound and complete system for the basic fragment CL5 of computability logic. Doing the same in sequent calculus, on the other hand, throws out the baby with the bath water, resulting in the strictly weaker affine logic. An implied claim of computability logic is that it is CL5 rather than affine logic that adequately materializes the resource philosophy traditionally associated with the latter.
A supporting paper that introduces an enhancement of sequent calculus. Reminds me of some French1 logician who used icons with frogs on his website - forgot his name...

The paper is quite readable, and uses just enough graphics so I am able to understand it.

1[on edit: I was wrong, he is Alessio Guglielmi, and this name sounds Italian, my apologies]

[on another edit: ha! behold the footnote on page 35! also, I vaguely remember Charles A. Stewart mentioning Alessio was his colleague?]

By Andris Birkmanis at Tue, 2005-11-22 12:27 | login or register to post comments

To share or not to share

When I first browsed the paper, my thought was that cirquent calculus was very similar to Arnon Avron’s hypersequent calculus. Both deal with structures somewhat more complex than sequents. After a closer look, however, I realized that there is hardly much similarity. The idea of sharing (central in cirquent calculus) appears to be substantially new, and unavoidable if one wants to seriously talk about resources. Linear logic did not elevate to that point, and that’s too bad.

Resource logics aside, I wonder if among the benefits of cirquent calculus could be exponential improvements (over cut-free classical logic) of proof sizes.

By H.Harada at Tue, 2005-11-29 13:17 | login or register to post comments

Let's have fun

It is amusing how humor is used in this paper (I mean "In the beginning was game semantics") to make some serious philosophical points. Here are my favorite excerpts:

"The reason for the failure of [the Law of the Excluded Middle] in CL is not that this principle ... is not included in its axioms."

"[...] solvable in a sense that some constructivistically-minded might fail - or pretend to fail - to understand."

"[...] simplicity is good, yet, if it is most important, then nothing can ever beat ... the empty logic."

Thanks, Andris!
By H.Harada at Wed, 2005-11-30 03:19 | login or register to post comments

You are welcome

...I didn't write the paper, though :)

I wholeheartedly suggest reading it nevertheless, as I feel that computability logic has a great potential for clarifying several areas related to interaction (and even Frank recognized there is some need for going beyond "purely functional" land). I may be missing some works by other authors, of course, and therefore overestimate the value of Giorgi Japaridze's research...

By Andris Birkmanis at Wed, 2005-11-30 09:27 | login or register to post comments