表題番号:2024C-432
日付:2025/04/03
研究課題強力なデータ構造と並行性をもつ高水準言語の表現力強化
研究者所属(当時) | 資格 | 氏名 | |
---|---|---|---|
(代表者) | 理工学術院 基幹理工学部 | 教授 | 上田 和紀 |
(連携研究者) | 早稲田大学理工学術院 | 助手 | 山本直輝 |
- 研究成果概要
- 本研究では,高い汎用性をもちながら通常のプログラミング言語が直接サポートしないグラフ構造を扱う高水準言語として研究開発を推進しているLMNtal言語の機能深化に取り組み,以下の成果を得た.1. プログラミング言語において重要な役割を演じるグラフ型の概念の新たな定式化を行った.特に,グラフ構造の一部(部分グラフ)に対して型を付与するための差分型概念を定義し,それが効率的な静的型検査を可能にすることを示すとともに,ユーザ定義可能な強力なグラフパターンマッチングに応用できることを示した.2. モデリング言語の観点からは,既存のLMNtalのグラフマッチング機能を格段に強化すべく,(i) マッチングを抑止する否定条件,および (ii) 不特定多数のサブグラフに対する同時パターンマッチングと書換えを可能にする量化パターンの概念を統合的に扱うための構文と意味論を定義した.また,定義した意味論を実現するためのLMNtal仮想機械命令の設計と実装を行い,並行計算や量子計算を含む複数の例題を用いて,記述力確認と処理系上での動作確認を行った.3. さらに,グラフ書換え概念が論理学,特に線形論理のProof Netsと密接な関係を持つことに着目して,既存のLMNtalがもつ膜概念とProof NetsがもつBox概念の関係を綿密に検討した.これを通じて,LMNtalの既存の膜操作機能の拡張を言語仕様および実装に対して行い,線形論理の重要な断片であるMELL (Multiplicative Exponential Linear Logic) の証明およびカット除去操作がLMNtalで簡潔にエンコードできることを示した.以上の研究開発を通じて,LMNtal言語と複数の隣接分野とのつながりを格段に強化することができた.