Quantization, Categorification and Geometrization of Program Semantics

2022 Fiscal Year Final Research Report

• Project/Area Number: 18K11165
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60010:Theory of informatics-related
• Research Institution: Kyoto University
• Principal Investigator: Hasegawa Masahito 京都大学, 数理解析研究所, 教授 (50293973)
• Project Period (FY): 2018-04-01 – 2023-03-31
• Keywords: プログラミング言語 / 意味論 / 圏論 / 量子トポロジー / テンソル圏 / ラムダ計算

Outline of Final Research Achievements

This study aimed at developing novel semantics of low-level implementations of programming languages via geometric and topological approaches. In particular, we introduced a braided lambda calculus in which permutations of variables are realized by braids carrying information on the low-level geometric implementation. We established the fundamental correspondence between the braided combinatory algebras and braided closed operads, and more generally the correspondence between planar combinatory algebras and planar closed operads, where the construction of operads from combinatory algebras plays the central role. We also investigated new constructions of traced monoidal categories, which give a categorical foundation of our approach, by studying Hopf monads which lift the trace.

Free Research Field

理論計算機科学

Academic Significance and Societal Importance of the Research Achievements

本研究はプログラミング言語の理論の基礎付けに関するものであり、圏論や幾何学の新しい知見や技法をプログラム意味論に取り入れること、および必要となる圏論の整備の両方を目指したものである。本研究によりプログラミング言語設計やプログラム検証に用いることのできる数学的手法が拡充され、短期的には、このような幾何的アプローチに基づく理論研究の活性化・深化、また、長期的には、今後のソフトウェア開発・検証技術の発展に寄与することが期待される。