2018 Fiscal Year Annual Research Report
高階・型付きの計算体系に基づくプログラミングの理論と応用の展開
| Project/Area Number |
15H02681
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
住井 英二郎 東北大学, 情報科学研究科, 教授 (00333550)
|
|---|
| Project Period (FY) |
2015-04-01 – 2020-03-31
|
| Keywords | 関数型プログラミング言語 / セキュリティ型つきλ計算 / 非機密化(declassification) / 遅延評価 / 名前呼び / 必要呼び |
|---|
| Outline of Annual Research Achievements |
本研究の目的は「古くから研究されているが最近になって目覚ましく実用化が進み産業界でも注目されている『関数型言語』を中心とする、高階・型付き計算およびプログラミングの理論の深化と応用の拡大を目指す」ことである。当年度は前年度までに引き続き、複数のサブテーマについて様々な研究を実施した。その一部について、「専門用語を多用することは避けてください」との指示に可能な限り従いつつ、「600字～800字で」概要を述べる。本研究は研究協力者ら（事務上、分担金の配分を必要とせず研究分担者とならない研究者や、研究者番号を持たず研究分担者になれない博士後期課程学生・博士前期課程学生・学部4年生（いずれも研究実施当時）を含む）との共同研究である。
１．高機密情報（高機密情報を処理した結果の情報を含む）の一部を必要に応じて公開できるように低機密情報として扱う非機密化(declassification)という機構を備えたセキュリティ型付きλ計算の理論の発展・改良を行なった。λ計算とは理論計算機科学や数理論理学において重要な理論の一つで、関数型プログラミング言語の基礎的計算モデルとなっている。当年度は、前年度までの理論を定理証明支援器で定式化することにより、修正は比較的容易だが重要な誤りを発見・修正した。また、本理論の核心である高機密情報を条件とする分岐（if-then-else式）の扱いに困難があったため、それを本質的に改良する方法を考察・着想した。
２．式の値が必要になってから計算する、いわゆる遅延評価(lazy evaluation)の基礎理論として、式の値が必要になるたびに計算し直す名前呼び(call-by-name)と、計算結果を記憶する必要呼び(call-by-need)の対応について、従来より単純な対応関係を考察・着想し、定理証明支援器で定式化した。
|
| 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 |
引き続き研究協力者らと共同で、上述の研究を実施する。本研究のような基礎的研究の実施には研究者らの「時間」と「エネルギー」が最も決定的なリソースである。そのため、引き続き科研費や学内外のルールを遵守しつつ必要な人員を雇用する。当科研費は次年度（令和元年度）が最終年度であり、その成果をムダにせず次の研究につなげるためには新たな研究費の獲得が必要不可欠である。研究自体を実施する「時間とエネルギー」とのバランスに苦慮しているが尽力したい。
|
