2017 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 | 遅延評価 / 名前呼び / 必要呼び / 評価戦略 / λ計算 |
|---|
| Outline of Annual Research Achievements |
研究が多岐にわたるため、そのうちの一つについて述べる。本研究は博士前期課程学生（当時）との共同研究である。
いわゆる遅延評価(lazy evaluation)とは、「必要」になるまで式の値を計算しない評価戦略(evaluation strategy)のことである。例えばf(b,x) = if b then x+x else 0なる関数fに対しf(false,1+2)を計算する場合、変数xに束縛（代入）される式1+2の値は関数呼び出し時ではなくx+xが計算されるまで計算されず、この場合はbがfalseなので計算されない。
遅延評価の古典的な仕様として、名前呼び(call-by-name)がある。これは例えば前述の関数fに対してf(true,1+2)を計算する場合、f(true,1+2) → if true then (1+2)+(1+2) else 0 → (1+2)+(1+2) → 3+(1+2) → 3+3 → 6のように計算を行う方式であるが、この例からもわかるように、同じ式の値を何度も計算してしまう。そこで実装としてはf(true,1+2) → let x=1+2 in (if true then x+x else 0) → let x=1+2 in x+x → let x=3 in x+x → 3+3 → 6のように計算を行う必要呼び(call-by-need)がしばしば用いられる。
本研究（の一つ）では、名前呼びと必要呼びの対応の証明を改良し、定理証明器Coq上で厳密に定式化・検証した。この成果は国際会議FLOPS 2018に査読を経て採択され、発表予定である。
|
| 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 |
引き続き研究計画のとおり、高階・型付きのプログラミング言語理論にもとづく研究を行う。
|
Research Products
(1 results)
