所員 -星野 直彦-

名前 星野 直彦 (Hoshino, Naohiko)
助教
E-Mail naophiko (emailアドレスには@kurims.kyoto-u.ac.jp をつけてください)
研究内容 プログラミング意味論の研究
紹 介
 プログラミング言語の意味論,特に相互作用の幾何学(Geometry of Interaction,GoI)と 実現可能性解釈の研究を行っている。GoIはGirardにより始めら れた線型論理の意味論の一つで線型論理のカット除去に関する研究がその端緒で ある。Curry-Howard同型を通してGoIを多 相型線型ラムダ計算の意味論と見なすことができ,さらにプログラミング言語の 重要な機構である不動点演算子のGoI解釈について研究がなされている。GoI意味 論の特色は,プログラミ ング言語の解釈がその言語の実装を与えていること,1990年代後半から今に至る まで種々のプログ ラミング言語の完全抽象性問題を解決したゲーム意味論とよく似た構造を持って いること, Abramsky, Haghverdi, Scottらによって整備された圏論的枠組を持つことが挙げ られる。 与えれらたプログラミング言語に対する完全抽象性を満たすモデルを与えること はプログラム意味論の 研究において1980年代から取り組まれてきた問題であり,その動機はプログラミ ング言語の 計算可能性を特徴づけるという哲学的問題意識とプログラミング言語の検証への 応用の2つ挙げられる。 実際ゲーム意味論を用いたプログラミング言語の観測的同値を検証する研究があ る。ゲーム意味論は完全 抽象性問題に対し多くの結果をもたらした強力な意味論である一方で,ゲーム意 味論の定義は初等的であ り,また,与えられた言語に対して完全抽象性を満たすゲーム意味論があるか, どのようにそれを定義すべきかと いう問題は与えられた言語ごとに取り組まれている。こういった状況に対し, GoIの圏論 的枠組みを通してゲーム意味論を捉えなおすことで新たな「ゲーム意味論」を構 成することを目指している。
 しかしながらGoI意味論の研究においては不動転演算子の解釈をどのように与え るべきかという問題すら十分 に議論されていなかった。[4]において星野は標準的なGoI解釈は不動転演算子の 解釈の取り方によらず多相型 線型ラムダ計算の妥当(adequate)な意味論とはならないことを観察し,実現可 能性解釈を用いた圏論的モデ ルの構成から多相型線型ラムダ計算の為の妥当なGoI意味論を与えた。また[2]に おいてGoI意味論の圏論的枠組みの中で 基本となるunique decomposition categoryのある部分クラスが加算双直積を持 つ圏に埋め込める事を証明した。 この結果は与えられたunique decomposition categoryがどのような計算の世界 の意味論を与えているかを調べ るための足掛かりになると考えている。現在はよく知られているGoI意味論がそ れぞれどのような計算可能性の世界と 関連しているかを調べる手法を研究している。
  1. Naohiko Hoshino. Step Indexed Realizability Semantics for a Call-by-Value Language Based on Basic Combinatorial Objects. In Proceedings of LICS 2012, pages 385--394, IEEE Computer Society.
  2. Naohiko Hoshino. A Representation Theorem for Unique Decomposition Categories. In Proceedings of MFPS 2012. ENTCS, volume 286, pages 213--227.
  3. Ichiro Hasuo and Naohiko Hoshino. Semantics of Higher-Order Quantum Computation via Geometry of Interaction. In Proceedings of LICS 2011, page 237-246, IEEE Computer Society.
  4. Naohiko Hoshino. A Modified GoI Interpretation for a Linear Functional Programming Language and its Adequacy. In Proceedings of FoSSaCS 2011, volume 6604 of LNCS, pages 320-334, Springer.
  5. Naohiko Hoshino. Linear Realizability. In Proceedings of CSL 2007, volume 4646 of LNCS, pages 420-434, Springer.