1997 Fiscal Year Annual Research Report
| Project/Area Number |
09780242
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
長谷川 立 東京大学, 大学院・数理科学研究科, 助教授 (20243107)
|
|---|
| Keywords | 解析関手 / ラムダ計算 / 項書き換え系 / Kruskalの定理 |
|---|
| Research Abstract |
木の埋め込みに関する整列半順序の理論はKruskalの定理として,組合せ論でひろく研究されている.また,この定理から得られるrecursive path orderingは項書換え系の理論のなかで停止性を証明するもっとも強力な手法としてひろく用いられている.これらに関し,その有用性から,いままで各種の順序が提案されて個別に研究されてきた.当研究では,Joyalによる解析関手の理論を用いることで,これらの順序が一つの枠組のなかでユニフォームに議論できることを示した.この結果は1997年12月,ネパールのカトマンドゥで開かれたASIAN'97国際会議で発表された.
Girardは解析関手の特別の場合である正規関手を用いて一階のλ計算のモデルを与えた.これを高階のλ計算であるシステムFに拡張できるかどうかがオープンな問題として提起されている.当研究では,解析関手を更に拡張したgroupoid上のwreath積を用いて,システムFのモデルを作ることに成功した.この結果は1997年10月,九州大学で開かれた研究集会「記号論理学と情報科学」で発表された.
また,これらの関しての基礎理論を東京工業大学で1997年9月に開かれたWorkshop on Theories of Types and Proofsにおける招待講演で発表した.
|
