所員 -星野 直彦-

名前 星野 直彦 (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. In Proceedings of LICS 2014, article 52.