Theory and Implementation of Staged Computation with Dependent Types
| Project/Area Number |
23K24819
|
|---|
| Project/Area Number (Other) |
22H03563 (2022-2023)
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Multi-year Fund (2024)
Single-year Grants (2022-2023) |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
浅井 健一 お茶の水女子大学, 基幹研究院, 教授 (10262156)
Kiselyov Oleg 東北大学, 情報科学研究科, 客員研究員 (50754602)
|
|---|
| Project Period (FY) |
2022-04-01 – 2026-03-31
|
| Project Status |
Granted (Fiscal Year 2024)
|
| Budget Amount *help |
¥17,290,000 (Direct Cost: ¥13,300,000、Indirect Cost: ¥3,990,000)
Fiscal Year 2025: ¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2024: ¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2023: ¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2022: ¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
|
|---|
| Keywords | プログラム生成 / プログラム特化 / 依存型 / 仕様記述 / プログラム解析・検証 / 型システム / 段階的計算 / 計算エフェクト / オフショアリング |
|---|
| Outline of Research at the Start |
暗号、データベース、画像処理など個々の領域における高性能プログラムを開発するためには、特定の領域ごとに特化したプログラムを生成する「プログラム生成法」が非常に有効であることをが知られている。本研究は、このプログラム生成法を大幅に発展させるため、「生成されるプログラムのサイズ」や「生成されるプログラムの計算誤差」など、量的情報を的確に表現できるシステムを構築して、それらの量に関する推論を行いながら、最適なプログラムを生成する方法を構築するものであり、研究目的が達成されれば、高性能・高信頼プログラムを必要とする様々な応用領域の発展に貢献するものである。
|
| Outline of Annual Research Achievements |
研究初年度となる２０２２年度は、本研究の基盤となる段階的計算体系において、計算リソース（メモリ量など）や生成されたコードのサイズ・性能などの量を扱うプログラム生成技法とその実例について調査を行った。特に、依存型を用いない従来型の型システムにおいてこれらの量的な情報をもとに質の高いプログラムを生成したりプログラム解析・検証を行った成功例について詳細に検討を行った。そのような研究の１つとして、亀山らが開発してきたプログラム生成・解析・検証を統一して行うフレームワークについて、暗号分野の適用事例をさらに洗練させて性能向上を果たした。特に、従来は、数論的変換関数だけの実装にとどまっていたのに対し、本研究では、多項式乗算など、より大きな関数を適用対象として、高性能コードの生成とその正しさの検証を同時に達成することに成功した。
上記と並行して、コード重複を回避する段階的計算において重要となる計算エフェクトについて理論・実装の両面からの研究を行い、代数的エフェクトと限定継続コントロールオペレータの関係を解明したり、限定継続コントロールオペレータに関する統一的型システムを与えることに成功した。
さらに、高性能コード生成において鍵となる技術の１つである「オフショアリング」の実装および応用例の作成を進めた。オフショアリングは、コード生成器を記述する高レベル言語と、生成されるコードを記述する低レベル言語の橋渡しをする技術であり、現代的な高性能コードの生成においては必須とされる技術である。段階的計算を実現するプログラミング言語MetaOCamlにオフショアリング機能を標準装備することに生成するとともに、C言語へのオフショアリングに関する従来手法において変数の取り扱いに問題がある事を発見して、改善手法を提案した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
異なる機関に属する研究代表者と２名の研究分担者の間のコミュニケーションが適切にとれており、直接顔を合わせての集会を開催することができ、本研究の目指すべき方向、現時点の技術動向、今後の展開についての意識合わせがしっかりとできている。このグループでの研究集会を継続して開催することも合意している。
研究成果としての論文業績も一定の本数出ており、現在のところは異なる機関をまたがっての共著論文はないが、相互の研究内容を深く知ることができており、本科研費を軸にした今後の研究の展開を展望できている。
|
| Strategy for Future Research Activity |
本研究の主題である依存型などの精密な型を用いて、生成されるコードの質を高めることを目的とした研究を推進する。研究分担者Kiselovが提唱したtagless final法を基盤として、依存型を持つ言語である Coq や Agdaに展開することにより、上記の研究目的を達成することを目指す。研究メンバー３名はこれらの技術の１つ以上に強みを持っており、３名の連携により、研究を行う。
|
Report
(1 results)
Research Products
(14 results)
