2017 Fiscal Year Research-status Report
継続と文脈の概念にもとづく新しい関係的プログラム意味論
Project/Area Number |
16K12409
|
Research Institution | Tohoku University |
Principal Investigator |
住井 英二郎 東北大学, 情報科学研究科, 教授 (00333550)
|
Project Period (FY) |
2016-04-01 – 2019-03-31
|
Keywords | 継続 / 評価文脈 / 必要呼び / 名前呼び / 遅延評価 / 評価戦略 |
Outline of Annual Research Achievements |
本研究の「具体的内容」を「600字~800字で」「できるだけ分かりやすく」「専門用語を多用することは避けて」述べることは不可能なため、一部について述べる。 当年度は「継続」を表現する「評価文脈」を用い、名前呼び(call-by-name)と必要呼び(call-by-need)の計算の対応関係(ある種の等価性)を形式化した。 継続(continuation)とは計算の途中の時点での「残りの計算」を指す概念であり、評価文脈(evaluation context)によって表すことができる。例えば(1+2)×3という式において、[]×3という評価文脈は、1+2を計算し終わった後の継続を表す。ただし[]は1+2のような部分式が代入される穴(hole)であり、E[1+2]のような記法により、評価文脈の穴に部分式を代入した結果である(1+2)×3等の式を表す。一般に式Mから式Nに1ステップの計算が進む(簡約される)とき、式E[M]も式E[N]に簡約される。 評価文脈の定義の仕方により、様々な評価戦略(evaluation strategy)すなわち計算の順序を表すことができる。例えば関数呼び出しの前に引数の値を計算する値呼び(call-by-value)の評価文脈は引数の位置に穴が来ることを許すが、名前呼びでは許されない。評価文脈は、「必要」になったときに式の値を計算する必要呼びの計算の定式化においても重要な役割を果たす。本研究では評価文脈の定義を必要呼びの簡約の定義に埋め込む等の工夫により、名前呼びと必要呼びの対応関係の証明を既存研究より簡潔にし、定理証明器上の形式化を容易にした。 本研究は博士前期課程学生(当時)との共同研究である。
|
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 |
引き続き計画にもとづき研究を行う。
|
Causes of Carryover |
理由:いわゆる「基金化」の趣旨のとおり、科研費の対象は予測の不可能な基礎研究であり、完全な予算計画は本質的にありえないため。
使用計画:国民の血税を年度末に「消化」する等の不適切な行為は決して行わず、引き続き本研究に必要な物品の購入等に用いる。
|