On algebraic structure of functional programming languages: towards mathematical foundation of logical relations

• Project/Area Number: 26730004
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Theory of informatics
• Research Institution: Kyoto University
• Principal Investigator: Hoshino Naohiko 京都大学, 数理解析研究所, 助教 (20611883)
• Project Period (FY): 2014-04-01 – 2019-03-31
• Project Status: Completed (Fiscal Year 2018)
• Budget Amount: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000); Fiscal Year 2017: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2016: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2015: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2014: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
• Keywords: 論理関係 / 圏論的意味論 / 関数型プログラミング言語

Outline of Final Research Achievements

Logical relation is a powerful mathematical technique to prove mathematical properties of functional programming languages such as: observational equivalence of programs, strong normalization of lambda terms and parametricity principle of second-order lambda calculi. The main contribution of this research project is a construction of categorical models for higher-order (high-level) functional programming languages starting from categorical models of first-order (low-level) programming languages. We applied this construction technique to give adequate categorical models for higher-order functional programming languages with algebraic effects and a higher-order functional programming language with continuous probabilistic distribution and "scoring" mechanism. Our construction can be regarded as a program translation technique of higher-order (high-level) programming languages into first-order (low-level) programming languages.

Academic Significance and Societal Importance of the Research Achievements

本研究の成果からは種々の特徴（代数的副作用や連続的確率分布を扱えるなど）を持った高階の関数型プログラミング言語を同様の特徴を持つ一階のプログラミング言語に変換する手法が得られる．ここでの変換の数学的正しさは変換の導出に用いた論理関係により保証されている．この変換手法を経由することで一階のプログラミング言語の検証手法を高階の関数型プログラミング言語の検証手法に拡張することができると期待される．特に連続的確率分布を扱うプログラミング言語の検証は機械学習の研究の進展によりその重要性が増している．

Research Products

• [Journal Article] Geometry of Bayesian Programming (2019)
  • Author(s): Ugo Dal Lago and Naohiko Hoshino
  • Journal Title: To appear in Proceedings of Logic in Computer Science 2019 Volume: -
  • Peer Reviewed
• [Journal Article] Partial Traces on Additive Categories (2018)
  • Author(s): Hoshino Naohiko
  • Journal Title: Electronic Notes in Theoretical Computer Science Volume: 341 Pages: 219-237
  • DOI: 10.1016/j.entcs.2018.11.011
  • NAID: 120006695789
  • Peer Reviewed
• [Presentation] Partial Traces on Additive Categories (2018)
  • Author(s): Naohiko Hoshino
  • Organizer: Mathematical Foundations of Programming Semantics
  • Int'l Joint Research
• [Presentation] Memoryful Geometry of Interaction II: Recursion and Adequacy (2016)
  • Author(s): Koko Muroya, Naohiko Hoshino, Ichiro Hasuo
  • Organizer: Principle of programming language
  • Place of Presentation: St. Petersburg, Florida, United States
  • Year and Date: 2016-01-22
  • Int'l Joint Research
• [Presentation] Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects (2014)
  • Author(s): Naohiko Hoshino, Koko Muroya, Ichiro Hasuo
  • Organizer: Logic in computer science
  • Place of Presentation: Vienna, Austria
  • Year and Date: 2014-07-14 – 2014-07-18
• [Remarks]
  • URL: http://www.kurims.kyoto-u.ac.jp/~naophiko/