Light Affine Logic and Game Models of PTIME

By constructing fully complete models for increasingly rich fragments of Girard's system of Light Logics, Murawski and I have obtained a fully complete game model of Light Affine Logic (LAL) [MO00,MO01b], which may be considered as a denotational model of polytime computable functions. There is good prospect that the game model is ripe for applications. A priority is to extract a proof that LAL is PTIME sound. We expect the model to be useful for resolving certain syntactic issues (for example, that LAL augmented by the additives remains PTIME sound). As the game model is a semantics of polytime algorithms, it would be interesting to use it to analyse algorithms in the style of Colson (for example, to show that certain functions are not computable by polytime algorithms of a given kind). Turning to the syntax of LAL, do we need full universal quantification over types to achieve PTIME completeness, or would a restricted form of polymorphism suffice? Another problem is to use Hofmann's linear combinatory algebra of polytime Turing machines to construct a realizability model of LAL (and so extract a semantic proof of the PTIME soundness of the Logic). A related problem here is to find a linear combinatory algebra for PTIME computation that is based on a calculus, and so convenient for expressing and ``calculating'' algorithms (e.g. a kind of untyped light affine $\lambda$-terms).