Discreet Games, Light Affine Logic and PTIME Computation

Abstract

This paper introduces a model of IMLAL, the intuitionistic multiplicative (⊗ ⊸ § !)-fragment of Light Affine Logic, based on games and discreet strategies. We define a generalized notion of threads, so that a play of a game (of depth k) may be regarded as a number of interwoven threads (of depths ranging from 1 to k). To constrain the way threads communicate with each other, we organize them into networks at each depth (up to k), in accord with a protocol:

• • A network comprises an O-thread (which can only be created by O) and finitely many P-threads (which can only be created by P).

• • A network whose O-thread arises from a ! -game can have at most one P-thread which must also arise from a ! -game.

• • No thread can belong to more than one network.

• • Only O can switch between networks, and only P can switch between threads within the same network.

Strategies that comply with the protocol are called discreet, and they give rise to a fully complete model of IMLAL. Since IMLAL has a polytime cut-elimination procedure, the model gives a basis for a denotational-semantic characterization of PTIME.

On leave from Nicholas Copernicus University, Toruń, Poland.