メンバー

TOP > メンバー > 星野 直彦

星野 直彦

名前 星野 直彦 (Hoshino, Naohiko)

助教

E-Mail naophiko (emailアドレスには@kurims.kyoto-u.ac.jp をつけてください)


研究内容 プログラミング意味論の研究

紹 介

 表示的意味論はプログラムの挙動の見積や性質を調べる為の有効な道具である。 例えばプログラムの入出力の関係や、プログラムの等しさ、実行中に メモリのどの領域にアクセスがあるかなどが考えられる。表示的意味論の多くは プログラムを何らかの関数として表現することで、プログラムの入出力の 関係を捉えている。この手法は多くの成功を収めているが一方で

・プログラムの入出力についてのみ着目しているため実行プロセスについての 知見が得られない。
・等価なプログラムが異る関数として表現されていることがある。

など改善すべき点があった。
1990年代後半頃から研究され始めた相互作用の幾何学(Geometry of Interaction、GoI)およびゲーム意味論によってこれらの問題は解決されつつ ある。プログラムの実行はプログラムによる環境への変数の値の要求とその要 求に対する環境からの返答の繰返しからなる対話と捉えることができる。相互 作用の幾何学とゲーム意味論の特色はプログラムの実行プロセスを二人のプレー ヤーの対話として表現する点である。まずはAbramsky, JagadeesanとMalacariaの3人組とHylandおよびOngの2人組によりそれぞ れ関数型プログラミング言語PCF (Programming Computable Functions) の表示的意味論がゲーム意 味論を用いて与えられた。このゲーム意味論では等価なプログラムは本質的に 同じ対話プロセスとして表現されている。またその後Ghicaによるゲーム意味論 のプログラム等価性の自動検証への応用やMackieによる相互作用の幾何学のコ ンパイラへの応用などが研究されている。
本研究の目標は相互作用の幾何学とゲーム意味論を融合させ互いの欠点を補い あうことでこれらの表示的意味論のあらたな応用を発見することである。相互 作用の幾何学とゲーム意味論の以下のような欠点がある。

・ ゲーム意味論の定義は初等的であり、与えられたプログラミング言語に 対してどのようにしてゲーム意味論をあたえるかという問題はプログラミング 言語ごとに取り組まれている。
・ 相互作用の幾何学を多様なプログラミング言語の表示的意味論 として応用しようという研究自体が多くない。

まず相互作用の幾何学をなるべく体系的に多様な関数型プログラミング言語の表示的意味論とし て応用してみるというのがこれまでの研究で行ってきたことである。相互作用 の幾何学にはtraced monoidal categoryおよび$\mathbf{Int}$構成を基盤とし たAbramsky, Haghverdi及びScottによる圏論的な枠組みがある。これを用いる と``$\Box\Box\Box$''プログラミング言語の表示的意味論の目星が或る程度つ いていると$\mathbf{Int}$構成を経由して関数型``$\Box\Box\Box$''プログラ ミング言語の表示的意味論をどのようにして与えればいいかの目星もおおよそ つく。この考えによって関数型量子プログラミング言語と代数的副作用をもつ 関数型プログラミング言語の相互作用の幾何学による表示的意味論を与えたの が[1]と[4]である。また[3]においては[1]の成果を再帰的計算を許す代数的副作用をもつ関 数型プログラミング言語に拡張した。[2]ではMackieの結果と同様のアイデアを用いて 代数的副作用をもつ関数型プログラミング言語のトークン機械への変換を実装している。 この変換は[1]で構成した表示的意味論に基いたものである。

  1. Naohiko Hoshino, Koko Muroya and Ichiro Hasuo. Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects. In Proccedings of LICS 2014, paper 52, IEEE Computer Society.
  2. Koko Muroya, Naohiko Hoshino and Ichiro Hasuo. Memoryful GoI with Recursion. Short abstract presented at LOLA 2015
  3. Koko Muroya, Naohiko Hoshino, Ichiro Hasuo. Memoryful Geometry of Interaction II: Recursion and Adequacy. In Proceedings of POPL 2016, pages 748--760.
  4. Ichiro Hasuo and Naohiko Hoshino. Semantics of Higher-Order Quantum Computation via Geometry of Interaction. In Annals of Pure and Applied Logic, Volume 168, Issue 2, 2017, pages 404-469.

← BACK TO THE TOP

← BACK TO THE TOP

  • Follow on

Research Institute for Mathematical Sciences (RIMS)