計算とルディクス: 論理・計算・複雑さのための一般的フレームワーク構築に向けて

点击翻译按钮获取中文摘要

本研究の主題は、線型論理から派生したルディクス("遊び"の理論)を研究し、「対話(相互作用)としての計算」の理解に役立てることにある。本年度は、過去2年間の研究の仕上げとして、下記の作業を行った。1.前年度に引き続き、線形論理証明論において重要な役割を果たす焦点化原理の分析を行った。4月に来訪したSaurin博士とともに、前年度に考案した焦点化原理の代数的表現についての最終討議を行った。成果は国際学会MFPS'10にて発表した。2.前年度に引き続き、無限的・余帰納法的な文脈で対話的完全性の研究を行った。これは数理論理学におけるラッセル・パラドックス、プログラミング理論における一般再起型の解釈、実現可能性理論における直行性の概念など、多くの重要概念を統合するものとなった。前年度に執筆した論文についての最終検討を行い、結果は論理・理論計算機科学分野において最も権威のある国際学会の一つであるLICS'10にて発表した。3.2008年-2009年度にかけて行った、伝統的なゲーデル完全性とゲーム意味論的な対話的完全性の関係をルディクスの枠組みで確立する研究について、最終版を雑誌論文の形にまとめ上げた。その際、ルディクスの体系と極性付き線型論理との対応関係について根本的な見直しを行った。論文は国際誌Logical Methods in Computer Scienceに投稿し、受理された。