一阶因果关系的结构
The Structure of First-Order Causality
摘要：
博弈语义学通过将公式解释为博弈来描述证明的交互行为，在博弈中，证明诱导策略。这样的语义在这里引入捕获的依赖关系引起的量化一阶命题逻辑。在阐述这种语义时必须面临的主要困难之一是描述可定义策略的特征，即实际上表现得像证据的策略。这通常是通过将模型限制为满足微妙组合条件的策略来实现的，这些条件在组合下的保持性通常很难表现出来。在这里，我们提出了一个原始的方法来实现这一任务，这需要结合先进的工具，从游戏语义，重写理论和范畴代数。我们介绍了一个图表表示的monoidal类别的可定义的战略，我们的模型，通过发电机和关系：这些战略可以产生从一个有限的原子战略和战略之间的平等承认有限的公理化，这个方程结构对应的极化变化的概念双代数。因此，这项工作的桥梁代数和指称语义，以揭示一阶量词诱导的依赖关系的结构，并奠定了基础，在程序设计语言的因果关系的机械化分析。
英文摘要：
Game semantics describe the interactive behavior of proofs by interpreting formulas as games on which proofs induce strategies. Such a semantics is introduced here for capturing dependencies induced by quantifications in first-order propositional logic. One of the main difficulties that has to be faced during the elaboration of this kind of semantics is to characterize definable strategies, that is strategies which actually behave like a proof. This is usually done by restricting the model to strategies satisfying subtle combinatorial conditions, whose preservation under composition is often difficult to show. Here, we present an original methodology to achieve this task, which requires to combine advanced tools from game semantics, rewriting theory and categorical algebra. We introduce a diagrammatic presentation of the monoidal category of definable strategies of our model, by the means of generators and relations: those strategies can be generated from a finite set of atomic strategies and the equality between strategies admits a finite axiomatization, this equational structure corresponding to a polarized variation of the notion of bialgebra. This work thus bridges algebra and denotational semantics in order to reveal the structure of dependencies induced by first-order quantifiers, and lays the foundations for a mechanized analysis of causality in programming languages.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
