Exhausting strategies, joker games and full completeness for IMLL with unit

摘要

We present a game description of free symmetric monoidal closed categories, which can also be viewed as a fully complete model for Intuitionistic multiplicative linear logic with the tensor unit. We model the unit by a distinguished one-move game called Joker. Special rules apply to the joker move. Proofs are modelled by what we call conditionally exhausting strategies, which are deterministic and total only at positions where no joker move exists in the immediate neighbourhood, and satisfy a kind of reachability condition called P-exhaustion. We use the model to give an analysis of a counting problem in free autonomous categories which generalizes the Triple Unit Problem.