| 研究課題/領域番号 |
17K00005
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎理論
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
桜井 貴文 千葉大学, 大学院理学研究院, 教授 (60183373)
|
|---|
| 研究分担者 |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2024-03-31
|
| キーワード | ラムダ計算 / α同値 / 古典論理 / 証明検証系 / minlog |
|---|
| 研究成果の概要 |
本研究の目的は古典論理に基づく計算系に関する様々な性質を研究することであったが、まずその土台となる伝統的ラムダ計算の性質を検証系minlogを使って証明していく過程で、α簡約が同値関係になるというよく知られた定理に新しい証明があることに気付いた。同値関係になるになることの証明のうち困難なのは対称律であるが、α簡約を行うときに必要な名前替えの動きを詳しく分析することにより変数の衝突回避がどういう順序で起こるかを正確に把握することができる。すると、衝突回避のための変数の名前替えを単純なものに分解できるので、それを逆にたどることにより注目するα簡約を逆にたどるα簡約を構成することができる。
|
| 自由記述の分野 |
計算の論理と意味、プログラム意味論
|
| 研究成果の学術的意義や社会的意義 |
伝統的ラムダ計算は20世紀初頭から研究されており、現代の多くの計算系の土台になるものである。伝統的ラムダ計算においてα簡約が同値関係になるという基本的な定理は古くからよく知られており様々な方法で証明されているが、それにも関わらずまだ新しい証明があることは驚きであった。α簡約では変数の衝突を防ぐために変数の名前替えを行うが、それは代入の特別な場合とみなすことができ、代入の過程を詳しく把握することにより変数の名前替えを単純なものに分解し、それを利用してα簡約の性質を考えるというアプローチは今までに見られなかったアイディアであり、変数の名前替えについて新しい知見を得ることができた。
|
