研究課題/領域番号 |
26730004
|
研究種目 |
若手研究(B)
|
配分区分 | 基金 |
研究分野 |
情報学基礎理論
|
研究機関 | 京都大学 |
研究代表者 |
星野 直彦 京都大学, 数理解析研究所, 助教 (20611883)
|
研究期間 (年度) |
2014-04-01 – 2019-03-31
|
研究課題ステータス |
完了 (2018年度)
|
配分額 *注記 |
3,770千円 (直接経費: 2,900千円、間接経費: 870千円)
2017年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2016年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2015年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2014年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
|
キーワード | 論理関係 / 圏論的意味論 / 関数型プログラミング言語 |
研究成果の概要 |
論理関係は関数型プログラミング言語の数学的性質(例えば,プログラムの観測的同値性の判定,強正規化定理の証明,パラメトリシティ原理の証明など)を示すための有効な手法である.本研究の成果は論理関係の手法を用いて一階のプログラミング言語の数学的モデルから高階の関数型プログラミング言語の数学的モデルを構成する手法を構成し,この構成法を種々の副作用を持つプログラミング言語や連続的確率分布を扱うことのできる関数型プログラミング言語へ応用したことである.この高階の関数型プログラミング言語の数学的モデル構成法はその高階の関数型プログラミング言語を一階のプログラミング言語へ変換する手法と見ることもできる.
|
研究成果の学術的意義や社会的意義 |
本研究の成果からは種々の特徴(代数的副作用や連続的確率分布を扱えるなど)を持った高階の関数型プログラミング言語を同様の特徴を持つ一階のプログラミング言語に変換する手法が得られる.ここでの変換の数学的正しさは変換の導出に用いた論理関係により保証されている.この変換手法を経由することで一階のプログラミング言語の検証手法を高階の関数型プログラミング言語の検証手法に拡張することができると期待される.特に連続的確率分布を扱うプログラミング言語の検証は機械学習の研究の進展によりその重要性が増している.
|