2003 Fiscal Year Annual Research Report
| Project/Area Number |
15500003
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
長谷川 立 東京大学, 大学院・数理科学研究科, 助教授 (20243107)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
長谷川 真人 京都大学, 数理解析研究所, 助教授 (50293973)
|
|---|
| Keywords | 線形倫理 / 強正規性 / ラムダ計算 |
|---|
| Research Abstract |
直観主義線型論理のシンタックスに関する考察を行なった.線形論理は,計算機言語における記憶領域などのリソースの使いかたを制御する道具として,主としてシステム内部で利用する方法が開発されてきた.われわれは一歩進んで,システム内部だけではなく,言語そのものの設計に線型論理を用いることを考えている.このとき重要なのは,ユーザがすぐに理解できるような簡明な計算規則が与えられていることであるが,この点に関しては必ずしも十分に解明されているわけではない.最初に考えるべきこととして,もっとも抽象度の高いレベルでの計算規則を考察した.この方向でもっとも完成度が高いのは,Barber-Plotkinによるdual intuitionistic linear logicであるが,そのシステムは等式論理として与えられているだけであって,どのように計算規則をいれれば良いのかは明らかではない.特に,linear contextをどう処理すべきかは難しい.この困難は,dual intuitionistic linear logicの場合のみにとどまらず,let構文を持つような言語を考えるときにいつでも付きまとうものである.そこで,問題を一般化して,通常のλ計算にcontext intrusionと呼んでいる新しい計算規則を加えた体系を考えて,その性質を研究した.この体系が,Church-Rosser性や強停止性といった基本的な性質を満たすかどうかを調べている.簡単な場合には,これらが成り立つことがほぼ確かめられた.context intrusionの体系に関する性質を用いると,dual intuitionistic linear logicだけではなく,他にもMoggiによるcomputational lambda calculusの強停止性など,いくつかの関連した問題に対する解答が得られる.
|
Research Products
(3 results)
-
[Publications] Y.kakutani, M.hasegawa: "Parametrizations and fixed-point operators on control categories"Proc.6th International Conference on Typed Lambda Calculi and Applications. 180-194 (2003)
-
[Publications] Y.kameyama, M.hasegawa: "A sound and complete axiomatizaiton of delimited antinuations"Proc.8th ACM SIGPLAN International Conference on Functional Programming. 177-188 (2003)
-
[Publications] M.hasegawa: "Semantics of linear continuation-passing in call-by-name"Proc.7th International Conference on Functional and Logic Programming. (In Press). (2004)
