分散制約解消系を融合する関数論理型プログラミング

1999 Fiscal Year Annual Research Report

• Project/Area Number: 10480053
• Research Institution: University of Tsukuba
• Principal Investigator: 井田 哲雄 筑波大学, 電子・情報工学系, 教授 (70100047)
• Co-Investigator(Kenkyū-buntansha): 南出 靖彦 筑波大学, 電子・情報工学系, 講師 (50252531) ; チャクラヴァーティ マヌエル 筑波大学, 電子・情報工学系, 講師 (30292535) ; ミデルドープ アート 筑波大学, 電子・情報工学系, 助教授 (30251044) ; 鈴木 大郎 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (90272179) ; 山田 俊行 筑波大学, 電子・情報工学系, 助手 (60312831)
• Keywords: 関数論理型言語 / 制約解消系 / 計算モデル / ナローイング計算系 / 求解完全性 / Mathematica

Research Abstract

制約解消系を融合する関数論理型言語のための計算モデルを構築し,このモデルに基づくプログラムシステムの開発を行なった.
1.計算モデルの構築
制約を扱える関数論理型言語の計算モデルを構築するため,遅延条件付きナローイング計算系(Lazy Conditional Narrowing Calculus,LCNCと略す)を設計した.LCNCは,本研究に先立ち我々が考案した遅延ナローイング計算系(Lazy Narrowing Calculus,LNCと略す)を,条件付きの場合へと拡張したものである.さらに,計算機上での実装を容易にし,実行効率を向上させるため,LCNCに内在する非決定性を除去する改良を加えた.また,高階のプログラムを扱えるようにするための拡張として,作用型項により高階の項を表現する場合の計算系である作用型遅延ナローイング計算系(Applicative LNC)と,λ式により高階の項を表現する場合の計算系である高階遅延ナローイング計算系(LNff)を新たに提示した.計算モデルとして重要な性質である求解完全性の結果を,各計算系についてそれぞれ得ることができた.
2.プログラミングシステムの開発
分散環境における関数論理型プログラムシステムの本格的な実装を行った.このシステムを,制約解消系を備えた関数論理型プログラミング環境CFLP(Constraint Functional Logic Programming system)と呼ぶ.CFLPはインタプリタ,スケジューラ,制約解消系の3つの要素で構成し,Mathematicaを用いた分散型ソフトウェアシステムとして実装した.CFLPはナローイング計算系を基本とし,関数論理型言語インタープリタが,分散環境を構成する計算機に配置された複数の制約解消系にアクセスしつつ,等式の求解を行なう.ナローイング計算系は項代数上で解を求め,問題固有のドメインで解釈される定数やそれらの定数に対する操作は,ドメイン固有の解法を実現する制約解消系を必要に応じて呼び出して利用する.CFLPは,分散制約解消系と関数論理型プログラム処理系との融合という,本研究の目標を実現するものとなっている.

Research Products

• [Publications] M.Marin,T.Ida T.Suzuki: "On reducing the Search Space of Higher-Order Lazy Narrowing"Proc.4th Fuji International Symposium on Functional and Logic Programming (FLOPS'99). 319-334 (1999)
• [Publications] Mircea Marin and Wolfgang Schreiner: "CFLP:a Mathematica Implementation of a Distributed Constraint Solving System"Proc.3rd International Mathematica Symposium (IMS'99). (1999)
• [Publications] 大崎人士,A.Middeldorp 井田哲雄: "等式付き書換え系における多ソート不変性"コンピュータソフトウエア. 16(1). 33-45 (1999)
• [Publications] M.Hamada,A.Middeldorp T.Suzuki: "Completeness Results for a Lazy Conditional Narrowing Calculus"Proc.2nd Discrete Mathematics and Theoretical Computer Science Conference DMTCS/CATS'99. 217-231 (1999)
• [Publications] M.Marin,T.Yanagi T.Ida,A.Middeldorp: "LNCA:A Lazy Narrowing Calculus for Applicative Term Rewriting Systems"Proc.1st JSSST Workshop on programming and Programming Languages (PPL'99). 3-14 (1999)
• [Publications] M.Marin,W.Schreiner T.Ida: "A Distributed System for Solving Equational Constraints Based on Lazy Narrowing Calculi"Proc.1st JSSST Workshop on programming and Programming Languages (PPL'99). 67-77 (1999)
• [Publications] Y.Minamide: "Space-Profiling Semantics of the Call-by-Value Lambda Calculus and the CPS Transformation"Proc.3rd International Workshop on Higher-Order Operational Techniques in Semantics,ENTCS. 26. 103-118 (1999)
• [Publications] T.Yamada,et al.: "Logicality of Conditional Rewrite Systems"Theoretical Computer Science. 236(1,2). 209-232 (2000)