| 研究課題/領域番号 |
18H03218
|
|---|
| 研究機関 | 筑波大学 |
|---|
研究代表者 |
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
|
|---|
| 研究分担者 |
浅井 健一 お茶の水女子大学, 基幹研究院, 准教授 (10262156)
Kiselyov Oleg 東北大学, 情報科学研究科, 助教 (50754602)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2022-03-31
|
| キーワード | 多段階計算 / プログラム生成 / 先進的型システム / 多相型 / 一般化代数データ型 / 型安全性 / スクープ安全性 / 計算エフェクト |
|---|
| 研究実績の概要 |
４年間の研究計画の初年度にあたり、先進的型システムをもつ言語をターゲット言語とするプログラム生成の安全性、特に、型安全性とスコープ安全性に関する基礎理論の考察を行った。
ML系プログラム言語が持つlet多相とコード生成と計算エフェクトの３つを併せ持つプログラム言語に対して、素朴な型システムを想定すると、型安全性が壊れることが知られている。そこで、本研究では、このような組み合わせのプログラム言語は、アプリケーション記述において必要、もしくは、有用であることを明らかにし、ついで、このようなアプリケーションを記述できる程度に表現力が強く、かつ、型安全性が成立する程度に制限が効いている言語と型システムを設計した、伝統的に「値制限」と呼ばれる多相型の導入法と、「緩い値制限」と呼ばれる導入法のそれぞれに対して、自然でプログラマにとってわかりやすい制限をもうけて、結果として型安全性をもつ型システムを実現した。このうち、値制限に基づく方法は見通しの良い証明がつくが、緩い値制限に基づく方法は非常に難解な証明が必要であるため、本研究では、サブサンプションとよばれる規則を追加することとした。このルール自体が意味論的に健全であることの証明は次年度以降に行う。
このほか、依存型を持つプログラム言語に対して部分計算などのメタプログラミングを行う場合の型安全性の確保や、近年研究が非常に盛んになっている「代数的効果とハンドラ」に基づいて、プログラム生成との関係や他の言語へのプログラム変換や型の保存性などについて検討を行った。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究はプログラム生成に関する基礎理論から言語設計・実装、そして、アプリケーションの記述までを含んだものであり、本年度の研究では、多相型をもつプログラムの生成について成果を得た。また、プログラム生成で重要となる計算エフェクトの研究においては、「代数的効果とハンドラー」をML系言語に翻訳したり、故ルーティンを持つ言語に変換する研究を行い、そこでも先進的型システムの役割の重要性を解き明かした。これらの成果の論文発表は来年度以降となるが、本研究の中間をなす部分で成果を得ており、研究は順調に進展していると判定した。
|
| 今後の研究の推進方策 |
初年度で得られた基礎理論に基づき多相型を持つプログラムの生成については、型安全に行える言語を得ており、これをプログラム言語として実装し、アプリケーションを記述する必要がある。
２年目以降は、多相型以外の重要な型である一般化代数データ型や依存型を持つプログラムの生成について検討し、初年度と同様な成果を得ることを目標とする。
|
