[科普中国]-博弈语义

博弈语义是一种逻辑的语义，基于在博弈论概念上的真理或有效性的概念，后来博弈语义成为各种编程语言的完全抽象的语义模型。

概念博弈语义是一种逻辑的语义，基于在博弈论概念上的真理或有效性的概念，比如对一个游戏者存在一种获胜策略。保尔·洛伦茨首先在1950年代晚期为逻辑介入了博弈语义。此后在逻辑中已经研究了很多不同的博弈语义。博弈语义也已经应用于编程语言的形式语义。

量词博弈语义的基础性考虑已经被Jaakko Hintikka和Gabriel Sandu更加强调，特别是为了友好独立逻辑(IF逻辑，更加新近的友好信息逻辑)，它是带有分支量词的逻辑。复合性原理被认为对这些逻辑失败，所以Tarski主义的真理定义不能提供合适的语义。

要解决这个问题，量词被给予博弈论意义，全称量词和存在量词表示一个游戏者从这个域做的一个选择。在全称情况下，给游戏者的自然名字是“证伪者”;在存在情况下，是“证实者”。注意一个单一的反例证伪一个全称量化陈述，而一个单一的例子足够证实一个存在量化陈述。Wilfrid Hodges提议了复合语义并证明了它等价于给IF-逻辑的博弈语义。基础性考虑已经推动了其他人的工作，比如Japaridze的可计算性逻辑。1

直觉主义逻辑，指称语义，线性逻辑Lorenzen和Kuno Lorenz的主要动机是为直觉主义逻辑找到一种博弈论（他们的术语是"对话式"Dialogische Logik）语义。Blass首先指出在博弈语义和线性逻辑之间的联系。这个路线进一步由Samson Abramsky、Radhakrishnan Jagadeesan、Pasquale Malacaria和独立的由Martin Hyland和Luke Ong发展，对组合性加以特别强调，就是递归的在语法上定义策略。使用博弈语义，上面提及的作者们解决了长期存在的为可计算函数的编程语言定义完全抽象模型的问题。于是，在博弈语义的基础上，产生了为各种编程语言提供了完全抽象的语义模型，以及由此产生了用软件模型检测进行软件验证的新的语义导向的方法。2

本词条内容贡献者为:

黎明 - 副教授 - 西南大学