[科普中國(guó)]-博弈語義

博弈語義是一種邏輯的語義，基于在博弈論概念上的真理或有效性的概念，后來博弈語義成為各種編程語言的完全抽象的語義模型。

概念博弈語義是一種邏輯的語義，基于在博弈論概念上的真理或有效性的概念，比如對(duì)一個(gè)游戲者存在一種獲勝策略。保爾·洛倫茨首先在1950年代晚期為邏輯介入了博弈語義。此后在邏輯中已經(jīng)研究了很多不同的博弈語義。博弈語義也已經(jīng)應(yīng)用于編程語言的形式語義。

量詞博弈語義的基礎(chǔ)性考慮已經(jīng)被Jaakko Hintikka和Gabriel Sandu更加強(qiáng)調(diào)，特別是為了友好獨(dú)立邏輯(IF邏輯，更加新近的友好信息邏輯)，它是帶有分支量詞的邏輯。復(fù)合性原理被認(rèn)為對(duì)這些邏輯失敗，所以Tarski主義的真理定義不能提供合適的語義。

要解決這個(gè)問題，量詞被給予博弈論意義，全稱量詞和存在量詞表示一個(gè)游戲者從這個(gè)域做的一個(gè)選擇。在全稱情況下，給游戲者的自然名字是“證偽者”;在存在情況下，是“證實(shí)者”。注意一個(gè)單一的反例證偽一個(gè)全稱量化陳述，而一個(gè)單一的例子足夠證實(shí)一個(gè)存在量化陳述。Wilfrid Hodges提議了復(fù)合語義并證明了它等價(jià)于給IF-邏輯的博弈語義?；A(chǔ)性考慮已經(jīng)推動(dòng)了其他人的工作，比如Japaridze的可計(jì)算性邏輯。1

直覺主義邏輯，指稱語義，線性邏輯Lorenzen和Kuno Lorenz的主要?jiǎng)訖C(jī)是為直覺主義邏輯找到一種博弈論（他們的術(shù)語是"對(duì)話式"Dialogische Logik）語義。Blass首先指出在博弈語義和線性邏輯之間的聯(lián)系。這個(gè)路線進(jìn)一步由Samson Abramsky、Radhakrishnan Jagadeesan、Pasquale Malacaria和獨(dú)立的由Martin Hyland和Luke Ong發(fā)展，對(duì)組合性加以特別強(qiáng)調(diào)，就是遞歸的在語法上定義策略。使用博弈語義，上面提及的作者們解決了長(zhǎng)期存在的為可計(jì)算函數(shù)的編程語言定義完全抽象模型的問題。于是，在博弈語義的基礎(chǔ)上，產(chǎn)生了為各種編程語言提供了完全抽象的語義模型，以及由此產(chǎn)生了用軟件模型檢測(cè)進(jìn)行軟件驗(yàn)證的新的語義導(dǎo)向的方法。2

本詞條內(nèi)容貢獻(xiàn)者為:

黎明 - 副教授 - 西南大學(xué)