コバヤシ サトシ   KOBAYASHI SATOSHI
  小林 聡
   所属   京都産業大学  情報理工学部 情報理工学科
   職種   教授
発表年月日 2008/02/12
発表テーマ Game semantics and translational semantics for limit computable mathematics
会議名 Third NII TypeTheory Workshop
学会区分 研究会・シンポジウム等
発表形式 口頭(一般)
単独共同区分 単独
開催地名 東京
発表者・共同発表者 小林聡
概要 古典論理上の証明から計算に関する内容を抽出しようとする研究は、二重否定変換に基礎を置くものが多く、抽出されたプログラムは難解なものになりやすい。本研究では、弱い排中律を持つ理論に対して、二重否定によらない新しい変換意味論を与える。この変換はバックトラッキングゲームにヒントを得たもので、抽出されるアルゴリズムは一種のバックトラックを含むが、CPS を用いないために単純で理解しやすいものとなる。