所員 -星野 直彦-

名前 星野 直彦 (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意味論の研究においては不動転演算子の解釈をどのように与え るべきかという問題すら十分 に議論されていなかった。[2]において星野は標準的なGoI解釈は不動転演算子の 解釈の取り方によらず多相型 線型ラムダ計算の妥当(adequate)な意味論とはならないことを観察し,実現可 能性解釈を用いた圏論的モデ ルの構成から多相型線型ラムダ計算の為の妥当なGoI意味論を与えた。 最近ではGoIの圏論的枠組みがもたらす一般性に着目することで量 子的データを扱う量子ラムダ計算や計算効果をもつラムダ計算の為のGoI解釈 を統一的な手法により与えることを行った。種々の計算効果に対し統一的な形 で意味論を提供できることはゲーム意味論にはないGoIの強みの一例でありゲー ム意味論の成果を[3], [6]の結果に応用することによる体系的なプログラム検 証手法の構築を考えている。
  1. Naohiko Hoshino. Linear Realizability. In Proceedings of CSL 2007, volume 4646 of LNCS, pages 420-434, Springer.
  2. 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.
  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 Representation Theorem for Unique Decomposition Categories. In Proceedings of MFPS 2012. ENTCS, volume 286, pages 213--227.
  5. 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.
  6. Naohiko Hoshino, Koko Muroya, Ichiro Hasuo. Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects. To appear in Proceedings of LICS2014.