| 研究課題/領域番号 |
05680276
|
|---|
| 研究種目 |
一般研究(C)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
廣川 佐千男 (廣川 左千男) 九州大学, 理学部, 助教授 (40126785)
|
|---|
| 研究分担者 |
古森 雄一 静岡大学, 理学部, 助教授 (10022302)
|
|---|
| 研究期間 (年度) |
1993 – 1994
|
| 研究課題ステータス |
完了 (1994年度)
|
| 配分額 *注記 |
1,700千円 (直接経費: 1,700千円)
1994年度: 900千円 (直接経費: 900千円)
1993年度: 800千円 (直接経費: 800千円)
|
|---|
| キーワード | 構成的論理 / ラムダ計算 / 型理論 / 直観主義論理 / 適切さの論理 / curry-Haward / 型としての論理式 / 古典論理 / 線形論理 |
|---|
| 研究概要 |
『論理式と型の対応』を拡張した『論理式とリダクション規則の対応』の定式化を得た。新しい結合子Pを導入しそのリダクション規則を求め、パースの論理式に対応する結合子論理を定式化した。このリダクション規則は古典論理の証明から構成的証明を抽出する自然な変形である。このリダクション規則によれば、同じ論理式に対する証明はすべて同等となるという知見を得た。従来、古典論理ではチャーチ・ロサ-の性質が成り立たないといわれているが、これを論理式と型との対応から説明するものである。ラムダ計算を拡張したラムダ・ニュー計算をそのリダクション規則による定式化も行なった。これは、継続についての計算規則に類似していることが分り、FelleisenやJacobの研究との関連は今後の課題となった。中間論理の論理式の解析により、一般的に論理式からリダクション規則を生成する見通しがついた。今後、クリプケ・モデルから含意論理式を生成するYankovやZakharyaschevの手法うことにより、統一的な解析実験が必要である。
古森は適切さの論理におけるP-W問題に対し、Gentzen流の手法を用いた統語的証明を得た。廣川はP-Wに対するラムダ計算の定式化を与え、P-Wにおける証明の構造を明らかにした。廣川は、与えられた含意論理式に対し直観主義論理における証明図全体は、ある種の文法で記述できるという結果を得た。更にこのような証明図全体が有限か無限かという問題の複雑さが多項式領域完全であるという知見を得た。高橋、赤間との共同研究では、さらにこのアイデアが高階の型の体系にも拡張できるこという知見を得た。
|
