ラムダ計算の型問題に対する可解性・非可解性の特徴付け

2016 年度 研究成果報告書

• 研究課題/領域番号: 25400192
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 研究分野: 数学基礎・応用数学
• 研究機関: 群馬大学
• 研究代表者: 藤田 憲悦 群馬大学, 大学院理工学府, 准教授 (30228994)
• 研究協力者: Schubert Aleksy University of Warsaw, Institute of Informatics, Professor ; 鹿島 亮 東京工業大学, 情報理工学院, 准教授 ; 中澤 巧爾 名古屋大学, 情報科学研究科, 准教授 ; 松田 直祐 神奈川大学, 理学部, 助手
• 研究期間 (年度): 2013-04-01 – 2017-03-31
• キーワード: ラムダ計算 / 型検査問題 / 型推論問題 / 決定可能性 / チャーチ流 / カリー流 / チャーチ・ロッサーの定理

研究成果の概要

ラムダ式の定式化と型問題の決定可能性との依存関係を詳細に研究した．そのために，決定可能な定式化（チャーチ流）と決定不能な定式化（カリー流）との間に位置する中間的構造を持つラムダ式を系統分類的に導入した．そして，式のスタイルに順序関係を導入して，式のスタイルでパラメータ化された型問題の定式化を与えることができた．これにより，ラムダ式の基本問題や性質が，スタイルのパラメータで分類されて，問題の本質的条件を解明する枠組みが得られた．これらにより，ラムダ計算の型問題に対する可解性・非可解性の特徴づけを式のスタイルの観点から明らかにすることができた．

自由記述の分野

ソフトウェア基礎理論