2005 Fiscal Year Annual Research Report
メタプログラミングシステムのための正しいモジュール化の研究
| Project/Area Number |
16700005
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
浜名 誠 群馬大学, 工学部, 助手 (90334135)
|
|---|
| Keywords | メタプログラミング / モジュール化 / 高階抽象構文 / 項書換え系 / 等式仕様 / 圏論的意味論 / 普遍代数 / 停止性 |
|---|
| Research Abstract |
本年は、国際会議論文1本、学術論文誌4本の出版(及び出版決定)のめざましい成果を得た。
論文誌コンピュータソフトウェアVol.22で出版された論文は、変数束縛と代入の機構を持つ言語の代数的モデルであるΣモノイドから具体的な「言語」を構成した。これは数学的にはこ代数的な自由生成によってΣモノイドを構成することによる。結果として得られる言語は、自動証明システムやプログラム変換でよく用いられる高階抽象構文と呼ばれるものに類似した言語であるが、いくつかの点で拡張されており、また付随する代入操作を統一的に説明することができた。特にラムダ計算を文脈の「穴」で拡張した体系との興味深い一致を示した。
論文誌コンピュータソフトウェアに出版決定された論文は、Klopによって提案された高階書換えの体系コンビナトリー簡約系がΣモノイドによって健全かつ完全にモデル化できることを示したものである。
また、論文誌Higher-Order and Symbolic Computationに出版決定された論文「Explicit Substitutions and Higher-Order Syntax」は一階の関数記号と明示的代入からなる言語が、ある関手による始代数によって自然にモデル化できることを示したものである。ここで特徴的なことは、明示的代入をKan拡張を用いて表現することができる点である。また型なしλ計算に明示的代入を加えた場合でも、同様なモデル化ができることを示した。さらにこれらの始代数によるモデル化は、抽象構文を操作するような関数型プログラムにおいて有用な代数データ型を導くことを示した。最後に一階の言語に比べて、高階抽象構文のモジュラー性の困難さを解析した。
|
Research Products
(5 results)
