2001 Fiscal Year Annual Research Report
| Project/Area Number |
12680329
|
|---|
| Research Institution | CHIBA UNIVERSITY |
|---|
Principal Investigator |
桜井 貴文 千葉大学, 理学部, 助教授 (60183373)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 光晴 千葉大学, 理学部, 助手 (00291295)
古森 雄一 千葉大学, 総合メディア基盤センター, 教授 (10022302)
辻 尚史 千葉大学, 理学部, 教授 (70016666)
|
|---|
| Keywords | 様相部分構造命題論理 / 直観主義的様相論理 / カット除去 / 明示的代入 / 文脈 / 代入操作 / α変換 |
|---|
| Research Abstract |
本年度は、様相部分構造命題論理のカット除去定理を証明し項を付与することにより計算規則とみなす方法についての研究を行なった。直観主義的線型論理や直観主義的様相論理に項を付与して計算論的な意味を考察する研究は各所で行われているが、様相部分構造命題論理は特別な場合として直観主義的線型論理や直観主義的様相論理を含むのでそれらに対する統一的な視点を与えるのが本研究の目的である。従来の多くの研究は自然演繹に基づいているが、本研究ではシークエント計算による体系に項を付与する。こうするとカットが明示的代入に対応するので、明示的代入に関して得た結果を利用して直観主義的様相論理に関する項の付与と計算規則としてのカット除去手順を得ることができた。一般の場合についてもカット除去可能定理は既に証明したので、具体的なカット除去手順を記述するのは容易と思われたが、実はそうではなく様相!と?の扱いは明らかではないことが判明した。!に関してはBarberとPlotkinによる線型論理に項を付与する研究があるが、?に関してはいまだに不明であり、さらに研究を継続する必要がある。
また前年度に引き続き、明示的代入を持つ体系を拡張して第一級文脈を持つようにした体系に関する研究も行なった。その体系では束縛変数は名前を持つので代入操作は従来の名前のα変換による方法を用いることができず、自由変数の名前を変更するという新しい方法を与えた。本年度は、単純型付λ計算に対する保守的拡大性をより精密に述べた定理を示すことにより従来のα変換との関係に関する性質を明らかにした。
|
-
[Publications] Masahiko Sato: "A Simply Typed Context Calculus with First-Class Environments"The Journal of Functional and Logic Programming. 2002・4. 1-41 (2002)
-
[Publications] Mitsuharu Yamamoto: "Abstract A^* Algorithm and Its Application to Linearly Priced Timed Automata"Proceedings of The Second Asian Workshop on Programming Languages and Systems(APLAS 2001). 193-205 (2001)
-
[Publications] Masami Hagiya: "Symbolic Analysis of Timed Multiset Rewriting and Its Application to Protocol Analysis (Extended Abstract)"Rewriting in Proof and Computation, International Workshop, RPC'01. 34-41 (2001)
