| 研究課題/領域番号 |
25400192
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
数学基礎・応用数学
|
|---|
| 研究機関 | 群馬大学 |
|---|
研究代表者 |
藤田 憲悦 群馬大学, 大学院理工学府, 准教授 (30228994)
|
|---|
| 研究分担者 |
古森 雄一 千葉大学, 大学院理学研究科, 名誉教授 (10022302)
倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
|
|---|
| 研究協力者 |
Schubert Aleksy University of Warsaw, Institute of Informatics, Professor
鹿島 亮 東京工業大学, 情報理工学院, 准教授
中澤 巧爾 名古屋大学, 情報科学研究科, 准教授
松田 直祐 神奈川大学, 理学部, 助手
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2017-03-31
|
| 研究課題ステータス |
完了 (2016年度)
|
| 配分額 *注記 |
5,070千円 (直接経費: 3,900千円、間接経費: 1,170千円)
2015年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
2014年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
2013年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
|
|---|
| キーワード | ラムダ計算 / 型検査問題 / 型推論問題 / 決定可能性 / チャーチ流 / カリー流 / チャーチ・ロッサーの定理 / 型検査 / 型推論 / 合流性 |
|---|
| 研究成果の概要 |
ラムダ式の定式化と型問題の決定可能性との依存関係を詳細に研究した．そのために，決定可能な定式化（チャーチ流）と決定不能な定式化（カリー流）との間に位置する中間的構造を持つラムダ式を系統分類的に導入した．そして，式のスタイルに順序関係を導入して，式のスタイルでパラメータ化された型問題の定式化を与えることができた．これにより，ラムダ式の基本問題や性質が，スタイルのパラメータで分類されて，問題の本質的条件を解明する枠組みが得られた．これらにより，ラムダ計算の型問題に対する可解性・非可解性の特徴づけを式のスタイルの観点から明らかにすることができた．
|
