重复的Ludics（指数型、交互型和完整性）
Ludics with repetitions (Exponentials, Interactive types and Completeness)
摘要：
Ludics在游戏语义学的全景中是独特的：我们首先定义了互动组合，然后我们有语义类型，作为一组策略，它们“表现良好”，并以相同的方式对一组测试做出反应。作为逻辑公式的解释的语义类型具有一个基本的属性，称为内部完整性，这是荒谬的特征，也使其与可实现性区分开来。因此，内部完备性需要标准的完全完备性。越来越多的工作开始探索这种特定的互动方法的潜力。然而，ludics有一些局限性，这是由于在原来的公式，战略是抽象的MALL证明。一方面，不允许重复。另一方面，证明倾向于依赖于MALL证明类策略的非常特定的属性，使得难以将语义类型的方法转移到不同的设置中。在本文中，我们提供了一个扩展的ludics，它允许重复，并表明仍然可以有交互式类型和内部完整性。从这一点上，我们得到充分的完整性w.r.t.一个偏振版的MELL。在我们的扩展中，我们使用的属性比原始公式少，我们相信这是独立的利益。我们希望这可以为ludics方法在更大的领域和不同的环境中的应用开辟道路。
英文摘要：
Ludics is peculiar in the panorama of game semantics: we first have the definition of interaction-composition and then we have semantical types, as a set of strategies which "behave well" and react in the same way to a set of tests. The semantical types which are interpretations of logical formulas enjoy a fundamental property, called internal completeness, which characterizes ludics and sets it apart also from realizability. Internal completeness entails standard full completeness as a consequence. A growing body of work start to explore the potential of this specific interactive approach. However, ludics has some limitations, which are consequence of the fact that in the original formulation, strategies are abstractions of MALL proofs. On one side, no repetitions are allowed. On the other side, the proofs tend to rely on the very specific properties of the MALL proof-like strategies, making it difficult to transfer the approach to semantical types into different settings. In this paper, we provide an extension of ludics which allows repetitions and show that one can still have interactive types and internal completeness. From this, we obtain 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 of independent interest. We hope this may open the way to applications of ludics approach to larger domains and different settings.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
