| 研究課題/領域番号 |
12680346
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 国立情報学研究所 (2001-2003)
京都大学 (2000) |
|---|
研究代表者 |
龍田 真 国立情報学研究所, 情報学基礎研究系, 教授 (80216994)
|
|---|
| 研究分担者 |
照井 一成 国立情報学研究所, 情報学基礎研究系, 助手 (70353422)
|
|---|
| 研究期間 (年度) |
2000 – 2003
|
| 研究課題ステータス |
完了 (2003年度)
|
| 配分額 *注記 |
3,000千円 (直接経費: 3,000千円)
2003年度: 600千円 (直接経費: 600千円)
2002年度: 600千円 (直接経費: 600千円)
2001年度: 600千円 (直接経費: 600千円)
2000年度: 1,200千円 (直接経費: 1,200千円)
|
|---|
| キーワード | 構成的論理 / 型理論 / プログラム理論 / 強正規化可能性 / 置換簡約 / 構成的集合 / 余帰納的定義 / 実現可能性解釈 / プログラム合成 |
|---|
| 研究概要 |
本研究の目的は、構成的集合と余帰納的定義をもつ構成的論理を構築し、この論理体系を用いて、余帰納型を用いたプログラムの性質を明らかにし、また、構成的集合と余帰納的定義を用いたプログラム合成システムを試作することであった。次のような3つの研究成果を得た。(1)論理式Aが長D-正規証明をもつならば、Aの長正規証明が唯一であることを証明した。(2)古典二階自然演繹の強正規化可能性の証明に関して、CPS変換を用いた従来の証明が本質的誤っていることを主補題に対する反例をあげて示し、この原因が継続消滅の現象によることを指摘し、オグメンテーションの概念を用いてこの証明を完成させた。例外処理ラムダ計算や値呼びラムダミュー計算など他の類似の体系のCPS変換を用いた強正規化可能性の従来の証明が、継続証明により同様にして本質的に誤っていることを指摘した。(3)構成的二階自然演繹に置換簡約を追加した論理体系の強正規化可能性の簡明な証明を与えた。従来知られている証明は、Prawitzによる証明だけであり、これは記述が不完全であり、また複雑な帰納法を必要とした。原子選言論理のアイデアを用い、構成的二階自然演繹に置換簡約を追加した論理体系が原子選言論理に簡約を保存して翻訳できること、原子選言論理は飽和集合が定義でき飽和集合を用いた強正規化可能性の証明方法が使えることの2つから、新しい簡明な証明を得た。
|
