研究課題
本年は、国際会議論文1本、学術論文誌4本の出版(及び出版決定)のめざましい成果を得た。論文誌コンピュータソフトウェアVol.22で出版された論文は、変数束縛と代入の機構を持つ言語の代数的モデルであるΣモノイドから具体的な「言語」を構成した。これは数学的にはこ代数的な自由生成によってΣモノイドを構成することによる。結果として得られる言語は、自動証明システムやプログラム変換でよく用いられる高階抽象構文と呼ばれるものに類似した言語であるが、いくつかの点で拡張されており、また付随する代入操作を統一的に説明することができた。特にラムダ計算を文脈の「穴」で拡張した体系との興味深い一致を示した。論文誌コンピュータソフトウェアに出版決定された論文は、Klopによって提案された高階書換えの体系コンビナトリー簡約系がΣモノイドによって健全かつ完全にモデル化できることを示したものである。また、論文誌Higher-Order and Symbolic Computationに出版決定された論文「Explicit Substitutions and Higher-Order Syntax」は一階の関数記号と明示的代入からなる言語が、ある関手による始代数によって自然にモデル化できることを示したものである。ここで特徴的なことは、明示的代入をKan拡張を用いて表現することができる点である。また型なしλ計算に明示的代入を加えた場合でも、同様なモデル化ができることを示した。さらにこれらの始代数によるモデル化は、抽象構文を操作するような関数型プログラムにおいて有用な代数データ型を導くことを示した。最後に一階の言語に比べて、高階抽象構文のモジュラー性の困難さを解析した。
すべて その他
すべて 雑誌論文 (5件)
コンピュータソフトウェア(岩波書店) Vol.22 No.3
ページ: 201-207
Proceedings of 16th International Conference on Rewriting Techniques and Applications (RTA'05)(Springer) LNCS 3467
ページ: 135-149
コンピュータソフトウェア(岩波書店) (採録決定)
Higher-Order and Symbolic Computation (Springer Science+Business Media) (採録決定)
