| 研究概要 |
直観主義線型論理のシンタックスに関する考察を行なった.線形論理は,計算機言語における記憶領域などのリソースの使いかたを制御する道具として,主としてシステム内部で利用する方法が開発されてきた.われわれは一歩進んで,システム内部だけではなく,言語そのものの設計に線型論理を用いることを考えている.このとき重要なのは,ユーザがすぐに理解できるような簡明な計算規則が与えられていることであるが,この点に関しては必ずしも十分に解明されているわけではない.最初に考えるべきこととして,もっとも抽象度の高いレベルでの計算規則を考察した.この方向でもっとも完成度が高いのは,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の強停止性など,いくつかの関連した問題に対する解答が得られる.
|
