直観論理、表示的意味論、線形論理
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2021/07/21 22:25 UTC 版)
「ゲーム意味論」の記事における「直観論理、表示的意味論、線形論理」の解説
ローレンツェンと Kuno Lorenz の目的は、直観論理のためのゲーム理論的な意味論を見出すことであった。Blass で初めて線形論理とゲーム意味論の関連が指摘された。この方向で Samson Abramsky、 Radhakrishnan Jagadeesan、Rasquale Malacaria や、(それとは別に)Maritin Hyland と Luke Ong が研究を進め、合成性に重点を置いた(すなわち、文法から帰納的に戦略を定義する)。ゲーム意味論を使って、これらの研究者は長年の課題であったプログラミング言語 PCF(プログラミング言語)(英語版) の完全抽象モデルの定義に成功した。その結果、ゲーム意味論によって各種プログラミング言語の完全抽象モデルが構築され、ソフトウェアのモデル検査の新たな形式的手法が導かれた。
※この「直観論理、表示的意味論、線形論理」の解説は、「ゲーム意味論」の解説の一部です。
「直観論理、表示的意味論、線形論理」を含む「ゲーム意味論」の記事については、「ゲーム意味論」の概要を参照ください。
- 直観論理、表示的意味論、線形論理のページへのリンク