| 研究課題/領域番号 |
06680333
|
|---|
| 研究種目 |
一般研究(C)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 神戸大学 (1995)
龍谷大学 (1994) |
|---|
研究代表者 |
林 晋 神戸大学, 工学部, 教授 (40156443)
|
|---|
| 研究分担者 |
小林 聡 龍谷大学, 理工学部, 助手 (70234820)
中野 浩 龍谷大学, 理工学部, 講師 (30217799)
小林 聡 龍谷大学, 理工学部, 助手 (60195831)
|
|---|
| 研究期間 (年度) |
1994 – 1995
|
| 研究課題ステータス |
完了 (1995年度)
|
| 配分額 *注記 |
1,500千円 (直接経費: 1,500千円)
1995年度: 600千円 (直接経費: 600千円)
1994年度: 900千円 (直接経費: 900千円)
|
|---|
| キーワード | 構成的プログラミング / プログラム検証 / プログラム論理 / 形式的方法 / 型理論 / 構成的数学 |
|---|
| 研究概要 |
1.PXのcatch/throw論理による拡張とnon-informative quantifier : catch/throw論理を構成的プログラミングに適用する場合に生じる問題をPXのCIG帰納法がもつframeの概念を利用して解決した。また、この帰納法を用いてPXを拡張し使用実験を行った。また、PXはLispに基づくシステムであるが、Lispのcatch/throwでは、catchが返す値が正常終了による値であるか、throwが発生し、それがcatchされたものなのかは判定することができない。この事実を反映する推論規則をnon-informative quantifierを使い定式化した。
2.非決定的キャッチアンドスロー機構: キャッチアンドスロー機構により自然に非決定的な計算が導入されることを示し、その非決定性を許しても、この機構を導入した構成的プログラミングが破綻しないことを理論面から保証することに成功した。
3.computational monad,evaluation logicとnon-informative quantifier : S4様相論理に対応する構成的型理論の研究を行い、実現可能性解釈によるプログラム抽出と、構成的型理論からMoggiのmonad型の理論への型のcollapsingが本質的に同じものであることを明らかにした。また、evaluation modalityをnon-informative quantifierの拡張として、とらえらえることにより、表現力の高い構成的様相論理を定義できることを示した。
4.その他: Common Lispの多値メカニズムに基づく実現可能性解釈を持つPXであるmvPXと、ユーザーインターフェースを飛躍的に改良したP2Xの二つを実現した。また、PXの基礎をなすFefermanの理論を改良する方法を提唱し、Frege構造との関連を明らかにした。
|
