関数型プログラミング言語の代数構造の解明：論理関係の数学的理論の構築に向けて

2017 Fiscal Year Research-status Report

• Project/Area Number: 26730004
• Research Institution: Kyoto University
• Principal Investigator: 星野 直彦 京都大学, 数理解析研究所, 助教 (20611883)
• Project Period (FY): 2014-04-01 – 2019-03-31
• Keywords: 圏論的意味論 / 論理関係

Outline of Annual Research Achievements

これまでの研究において論理関係を用いてPCFに対する完全抽象性を満たす圏論的意味論の構成を目指してきた。構成ではGirardによる相互作用の幾何を出発点にしている。相互作用の幾何にはAbramsky, HaghverdiとScottによる圏論的な枠組みがある。これまではその圏論的な枠組みの中でも、Abramsky, JagadeesanとMalacariaによるゲーム意味論（AJMゲーム意味論）との類似が知られている、集合と部分関数からなるトレース付き対称モノイダル圏を用いた相互作用の幾何を採用してきた。これはAJM意味論がPCFに対する完全抽象性を満たす圏論的意味論を提供することが知られているからである。今年度の研究において明らかになったことはAJMゲーム意味論と相互作用の幾何の類似を介した論理関係を用いてPCFに対する完全抽象性を満たす圏論的意味論の構成における困難が論理関係によってはAJMゲーム意味論における圏論的意味論の構成、特にゲームの圏の射を戦略に対する群の作用についての同値類によって与えるという構成が捉えられないことである。これは論理関係がプログラムの入出力についての情報のみを見ている一方で、AJMゲーム意味論における戦略に対する群の作用はプログラムの実行プロセスに関する内包的な情報についてのものだからである。このことから相互作用の幾何を出発点にし、論理関係を用いてPCFに対する完全抽象性を満たす圏論的意味論の構成するには既存の相互作用の幾何の枠組みに射に対する群の作用の概念を組み込むか、射の同値類を考える必要のないHylandとOngによるゲーム意味論との類似があるメモリ付きの相互作用の幾何を構成の出発点にする必要があると考えられる。

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

AJMゲーム意味論では圏論的意味論の構成でゲームの戦略に対する群作用についての同値類によって射を定義している。この同値類を考えるという点が完全抽象性の証明の中の重要な点の一つである。一方で相互作用の幾何では圏論的意味論の構成で部分同値関係による射の同値類を考えている。当初はゲームの戦略に対する群作用についての同値類の議論を部分同値関係による射の同値類の議論で置き換えられると楽観的に考えていたため。

Strategy for Future Research Activity

これまではAJMゲーム意味論との類似性をもつ集合と部分関数から得られる相互作用の幾何を用いて論理関係によるPCFに対する完全抽象性を満たす圏論的意味論の構成を目指してきたが、今後はHylandとOngによるゲーム意味論との類似性があるメモリ付き相互作用の幾何を出発点にした論理関係によるPCFに対する完全抽象性を満たす圏論的意味論の構成を目指す。またこれまでの研究で得られたAJMゲーム意味論と相互作用の幾何の論理関係を通した類似性を体系化することで具体的な成果を与える。

Causes of Carryover

研究の遅れのため計画していた国際会議への出張を取りやめたため。次年度の旅費として使用予定。