継続と文脈の概念にもとづく新しい関係的プログラム意味論

2018 年度 研究成果報告書

• 研究課題/領域番号: 16K12409
• 研究種目: 挑戦的萌芽研究
• 配分区分: 基金
• 研究分野: ソフトウェア
• 研究機関: 東北大学
• 研究代表者: 住井 英二郎 東北大学, 情報科学研究科, 教授 (00333550)
• 研究協力者: 松田 一孝 ; キセリョーヴ オレッグ
• 研究期間 (年度): 2016-04-01 – 2019-03-31
• キーワード: 継続 / （評価）文脈 / プログラム等価性 / call/cc / λ計算 / （環境）双模倣

研究成果の概要

「難解な専門用語の使用はできるだけ避けるか…適宜説明を加えて」「最大300文字」との指示に従って述べる。「継続」とは、計算機プログラムを実行している途中の「残りの計算」を指す概念である。「文脈」とは、プログラム中のある部分に対し、そのまわりの部分（前者を[]という記号で置き換えた、「穴」のあるプログラム）を指す。本研究では、「継続」を扱う機能の一つであるcall/ccという演算を含む関数型（式の値を計算する「評価」以外の、いわゆる「副作用」がない）プログラムの等価性（動作の等しさ）を証明するための理論を「環境双模倣」という手法にもとづき確立し、その知見を他の研究にも活かすことができた。

自由記述の分野

プログラム理論

研究成果の学術的意義や社会的意義

現代社会において計算機を中心とする情報処理システムの重要性は言をまたないが、多くの計算機ソフトウェアの理論的基礎は薄弱であり、毎日のように「不具合」（という名の誤動作）を起こして社会的問題となっている。本研究のような「プログラミング言語理論」は、狭義の「プログラム」のみならず、広義の「計算モデル」も含め、数理論理学的基礎による堅固な理論の確立・発展・応用を目指している。本研究もその一つであり、前述の「継続」と「文脈」という、広義の計算機プログラムにおいて重要な概念を扱った、「二つのプログラムの動作が等しい」という基本的な性質を証明する手法の成果である。