| 研究課題/領域番号 |
12680329
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
桜井 貴文 千葉大学, 理学部, 助教授 (60183373)
|
|---|
| 研究分担者 |
山本 光晴 千葉大学, 理学部, 助手 (00291295)
古森 雄一 千葉大学, 総合メディア基盤センター, 教授 (10022302)
辻 尚史 千葉大学, 理学部, 教授 (70016666)
|
|---|
| 研究期間 (年度) |
2000 – 2001
|
| キーワード | 様相部分構造命題論理 / 直観主義的様相論理 / カット除去 / 明示的代入 / 文脈 / 代入操作 / 束縛変数 / α変換 |
|---|
| 研究概要 |
様相部分構造命題論理のカット除去定理を証明し項を付与することによりカット除去操作を計算規則とみなす方法についての研究を行なった。直観主義的線型論理や直観主義的様相論理に項を付与して計算論的な意味を考祭する研究は各所で行われているが、様相部分構造命題論理は特別な場合として直観主義的線型論理や直観主義的様相論理を含むのでそれらに対する統一的な視点を与えるのが本研究の目的である。従来の多くの研究は自然演繹に基づいているが、本研究ではシークエント計算による体系に項を付与する。こうするとカットが明示的代入に対応するので、明示的代入に関して得た結果を利用して直観主義的様相論理に関する項の付与と計算規則としてのカット除去手順を得ることができた。一般の場合についてもカット除去可能定理は既に証明したが、具体的なカット除去手順を記述とその性質についてはさらに研究を継続する必要がある。
また上記の研究と関連して、明示的代入を持つ体系の拡張についても研究を行ない、第一級文脈を持つようにした体系を構成したした。脈とは穴を持つλ項であり、文脈を体系内で扱えるように拡張することによりメタなレベルで行なっている操作を形式化できるようにするのが目的である。その体系では束縛変数は名前を持つので代入操作は従来の名前のα変換による方法を用いることができず、自由変数の名前を変更するという新しい代入の方法を与えた。そしてその体系は合流性や強正規化性という望ましい性質を持っていることを示し、単純型付λ計算に対する保守的拡大定理をα変換を考慮に入れることにより精密化した。
|
