Exhausting Strategies, Joker Games and Full Completeness for IMLL with Unit (Preliminary Version)
Andrzej S. Murawski, C.-H. Luke Ong · Electronic Notes in Theoretical Computer Science · 1999
We present a game description of free symmetric monoidal closed categories, which can also be viewed as a fully complete model for the 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 generalises the Triple Unit Problem.