| 研究概要 |
型理論に順序構造を導入した順序ソート型理論によって,モジュール表現や継承機構を備えた論理型言語と推論処理の実現が期待できる.本年度の研究ではこの観点から,理論的な性質を明らかにする問題に焦点を絞って研究を行った.まず単純型付きラムダ計算体系を基に,順序ソート型理論の定式化を行った.従来の型推論では幾つかの非整合的な性質があることから,新しく制限関数の概念に基づいた部分型関係を導入し,ラムダ計算の演算規則や代入法則などの基本的資質を明らかにした.さらに,変数変換によって継承機構を整合的に実現するラムダ計算体系を定義した.ラムダ計算体系は,論理型を導入することによって自然に高階論理言語を定義可能であり,人工知能で有用な推論機構を明快に与えることが出来る.型を概念に部分型関係を概念間の順序構造と見なす観点から階層的知識表現としての性質を考察した.また,部分型による型推論規則を与え,型継承に基づく推論処理と証明論としての性質を明らかにした.推論処理を自動化する上で高階単一化,高階一般化が重要な問題であるが,順序ソートの場合には確立されていない。一般の高階単一化は計算不能であり実用の観点からもあまりにも範囲が広すぎる.そのため,本研究では2階論理式のマッチングに焦点を絞り効率的アルゴリズムの設計の観点からの研究を行った.順序を考慮しない場合は多項式計算量のヒューリスティックを導入したアルゴリズムが得られた.更に順序構造を導入した2階述語マッチングへの拡張を行っている状況である.型順序関係を用いた論理体系についてそのクリプケ可能世界意味論を与え,一つの可能世界を知識モジュールと見なすことによって,モジュール構造をもった論理プログラム理論としての意味付けが可能である.まだ,順序ソート型理論と論理体系,継承や型変換の機能を備えたモジュール理論との完全な融合は出来ていないが,人工知能基礎論における知識表現と推論に新しい発展をもたらす可能性を秘めており,今後も研究を推進する計画である.
|
