| 研究実績の概要 |
研究が多岐にわたるため、そのうちの一つについて述べる。本研究は博士前期課程学生（当時）との共同研究である。
いわゆる遅延評価(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に査読を経て採択され、発表予定である。
|
