Ludics with repetitions (Exponentials, Interactive types and Completeness)

摘要

Ludics is peculiar in the panorama of game semantics: we first have thedefinition of interaction-composition and then we have semantical types, as aset of strategies which "behave well" and react in the same way to a set oftests. The semantical types which are interpretations of logical formulas enjoya fundamental property, called internal completeness, which characterizesludics and sets it apart also from realizability. Internal completeness entailsstandard full completeness as a consequence. A growing body of work start toexplore the potential of this specific interactive approach. However, ludicshas some limitations, which are consequence of the fact that in the originalformulation, strategies are abstractions of MALL proofs. On one side, norepetitions are allowed. On the other side, the proofs tend to rely on the veryspecific properties of the MALL proof-like strategies, making it difficult totransfer the approach to semantical types into different settings. In thispaper, we provide an extension of ludics which allows repetitions and show thatone can still have interactive types and internal completeness. From this, weobtain full completeness w.r.t. a polarized version of MELL. In our extension,we use less properties than in the original formulation, which we believe is ofindependent interest. We hope this may open the way to applications of ludicsapproach to larger domains and different settings.