Journal article icon

Journal article

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

Abstract:
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.
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
Merton College
Role:
Author


Publisher:
Elsevier
Journal:
Theoretical Computer Science More from this journal
Volume:
294
Issue:
1-2
Pages:
269–305
Publication date:
2003-02-01
Edition:
Publisher's version
ISSN:
0304-3975


Language:
English
Keywords:
Subjects:
UUID:
uuid:837c07ab-3f66-4040-bc24-bedb44aa9b35
Local pid:
ora:10777
Deposit date:
2015-03-31

Terms of use



Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP