| Project/Area Number |
17K00005
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Theory of informatics
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| Project Period (FY) |
2017-04-01 – 2024-03-31
|
| Project Status |
Completed (Fiscal Year 2023)
|
| Budget Amount *help |
¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2020: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2019: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2018: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2017: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
|
|---|
| Keywords | ラムダ計算 / α同値 / 古典論理 / 証明検証系 / minlog / 直観主義論理 / 数理論理学 / 検証 |
|---|
| Outline of Final Research Achievements |
The purpose of this research is to study various properties of computational systems based on classical logic. But, in the process of first proving the properties of traditional lambda calculus, which is the foundation of this, using the verification system minlog, we realized that there is a new proof of the well-known theorem that α-reduction becomes an equivalence relation. The symmetry law is the most difficult to prove when proving that an equivalence relation exists, but by closely analyzing the renaming required when performing α-reduction, we can accurately determine the order in which variable collision avoidance occurs. Then, we can decompose the variable renaming required for collision avoidance into simpler ones, and by tracing them in reverse, we can construct an α-reduction that reverses the α-reduction of interest.
|
| Academic Significance and Societal Importance of the Research Achievements |
伝統的ラムダ計算は20世紀初頭から研究されており、現代の多くの計算系の土台になるものである。伝統的ラムダ計算においてα簡約が同値関係になるという基本的な定理は古くからよく知られており様々な方法で証明されているが、それにも関わらずまだ新しい証明があることは驚きであった。α簡約では変数の衝突を防ぐために変数の名前替えを行うが、それは代入の特別な場合とみなすことができ、代入の過程を詳しく把握することにより変数の名前替えを単純なものに分解し、それを利用してα簡約の性質を考えるというアプローチは今までに見られなかったアイディアであり、変数の名前替えについて新しい知見を得ることができた。
|
