研究課題
本研究の「具体的内容」を「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)の評価文脈は引数の位置に穴が来ることを許すが、名前呼びでは許されない。評価文脈は、「必要」になったときに式の値を計算する必要呼びの計算の定式化においても重要な役割を果たす。本研究では評価文脈の定義を必要呼びの簡約の定義に埋め込む等の工夫により、名前呼びと必要呼びの対応関係の証明を既存研究より簡潔にし、定理証明器上の形式化を容易にした。本研究は博士前期課程学生（当時）との共同研究である。
2: おおむね順調に進展している
前年度の成果に加え、当年度も前述の成果等が得られているため。
引き続き計画にもとづき研究を行う。
理由：いわゆる「基金化」の趣旨のとおり、科研費の対象は予測の不可能な基礎研究であり、完全な予算計画は本質的にありえないため。使用計画：国民の血税を年度末に「消化」する等の不適切な行為は決して行わず、引き続き本研究に必要な物品の購入等に用いる。
すべて 2018 2017
すべて 雑誌論文 (1件) (うち査読あり 1件、 オープンアクセス 1件) 学会発表 (1件)
Functional and Logic Programming: 14th International Symposium, FLOPS 2018
巻: 印刷中 ページ: 印刷中（全16頁）
