| 研究課題/領域番号 |
08458059
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 筑波大学 |
|---|
研究代表者 |
井田 哲雄 筑波大学, 電子・情報工学系, 教授 (70100047)
|
|---|
| 研究分担者 |
鈴木 太郎 (鈴木 大郎) 筑波大学, 電子・情報工学系, 助手 (90272179)
CHAKRAVARTY マヌエル (チャクラヴァーティ マニ) 筑波大学, 電子・情報工学系, 講師 (30292535)
AART Middeld (ミデルドーブ アート) 筑波大学, 電子・情報工学系, 助教授 (30251044)
|
|---|
| 研究期間 (年度) |
1996 – 1997
|
| 研究課題ステータス |
完了 (1997年度)
|
| 配分額 *注記 |
3,800千円 (直接経費: 3,800千円)
1997年度: 1,000千円 (直接経費: 1,000千円)
1996年度: 2,800千円 (直接経費: 2,800千円)
|
|---|
| キーワード | ナロ-イング / 高階関数・論理型言語 / 計算モデル / 条件付き項書換え系 / 完全性 / 高階関数論理型言語 / 求解完全性 / 安全性 |
|---|
| 研究概要 |
関数型言語では、関数の高階性を利用することで、プログラムの可読性が増し、かつ、強力な表現能力を得られることが古くから知られている。しかし、現在提案されている関数論理型言語のほとんどは一階である。本研究では、高階関数論理型言語を実現するための理論的な基礎付けを与えることを目指した。我々が得た主な研究成果を以下に示す。
1.一階のナロ-イング計算系であるLNC(Lazy Narrow-ing Calculus)における計算を吟味し、より効率良く実行できる計算系LNCd(deterministic Lazy Narrowing Calculus)の設計を行った。LNCdでは、適用すべき推論規則がつねに一意に定まるので、LNCと比べて実行効率の向上をはかることができた。2.項書換え系やラムダ計算で知られる標準化定理(standardization theorem)の新たな証明法を考案し、左線形な項書換え系およぎ条件付き項書換え系について標準化定理が成り立つことをあきらかにした。標準化定理は、関数型言語における遅延評価機構の理論的基礎を与える。この定理を証明したことで、一階ナロ-イングの実行効率の向上をはかることができた。3.関数論理型言語の族を構成する次の3つの言語、すなわち、多ソ-ト一階関数論理型言語、インタラクティブ一階関数論理型言語、単純型付き作用型関数論理型言語の公理的、代数的、操作的、圏論的意味論を与えた。関数論理型言語の構文的部分を等式論理として定式化し、等式の解釈を与えることによって意味論を構成した。各意味論の間の厳密な対応関係を示し、これらの意味論が正当であることを示した。4.高階項書換え系に対するナロ-イングを実現する高階ナロ-イング計算系HLNC(Higher-order Lazy Narrowing Calculus)を提案し,その球解完全性を示した。HLNCは一階の項書換え系に対するナロ-イングを実現していたLNCを高階に拡張したものである。HLNCは定数をもつラムダ計算を包含しており、ラムダ項を含む高階関数・論理型言語の基礎となる計算モデルを与えている。
|
