From Producer-Consumer Games to Substructural Calculi

Abstract

Substructural logics are routinely motivated by ‘resource consciousness’. However, there often is discrepancy between this informal motivation and the logic that is supposedly modeled by it. We adopt Japaridze’s stance that privileges an intuitive game semantics over proof theory. But we take a different family of games, called Producer-Consumer (P-C-)games as starting point. In P-C-games one considers complex tasks built up from elementary requests for atomic items by C, to be matched by ‘supply item’ moves by P. Corresponding moves arise by letting either C or P choose between immediate sub-tasks or by letting the players repeat specific requests. The interaction between C and P is modeled as a formal game with infinite runs, where such a run is declared to be winning for P if each elementary request by C is eventually satisfied by P. Different variants of the game arise from different ways to regulate the succession of moves. In difference to the game formats usually considered for linear logic, we do not impose a strict alternation of moves between the two players, but rather aim at modeling asynchronousity. This leads to games of imperfect information. The main challenge of the proposed research program is to identify scheduling conditions and game variations under which the game is equivalent (with respect to the existence of winning strategies for P) to a game of perfect information, where the search for winning strategies for winning strategies for P can be identified with proof search in a (substructural) sequent or hypersequent calculus. The talk will focus on conceptual challenges, rather than on technical results for specific games and logics.