2001 Fiscal Year Final Research Report Summary
Relation between Semantics of Logical System and its Syntactic Properties
| Project/Area Number |
12680329
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | CHIBA UNIVERSITY |
|---|
Principal Investigator |
SAKURAI Takafumi Chiba University, Faculty of Science, Assistant Professor, 理学部, 助教授 (60183373)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
YAMAMOTO Mitsuharu Chiba University, Faculty of Science, Research Associate, 理学部, 助手 (00291295)
KOMORI Yuichi Chiba University, Institute of Media and Information Technology, Professor, 総合メディア基盤センター, 教授 (10022302)
TSUJI Takashi Chiba University, Faculty of Science, Professor, 理学部, 教授 (70016666)
|
|---|
| Project Period (FY) |
2000 – 2001
|
| Keywords | modal substructural logic / intuitionistic modal logic / cut elimination / explicit substitution / first-class context / substitution / α-conversion / α変換 |
|---|
| Research Abstract |
We have investigated how the cut elimination operations of the modal substructural logic can be regarded as computation rules, by proving the cut elimination theorem and assigning terms. We can give an integrated viewpoint to the similar researches on the computational meaning of the intuitionistic linear logic and the intuitionistic modal logic, because the modal substructural logic contains the intuitionistic linear logic and the intuitionistic modal logic as special cases. Many such researches done so far are based on natural deduction, but we have assigned terms to the modal substructural logic given in the sequent calculus style. Since the cut rule corresponds to the explicit substitution in this case, we were able to apply the results about the explicit substitution to obtain a term assignment to the intuitionistic modal logic and cut elimination operations as computation rules. We have proved the cut-free provability theorem in general case, but we need to continue the research on the concrete cut elimination operations and its properties.
We have also studied about the extension of the typed λ-calculus with explicit substitution and proposed the system with first-class contexts. A context is a λ-term with holes and it is introduced to implement the meta-level operation within the system. In the system, we cannot use the traditional substitution operation that uses α-conversion, so gave a new method of defining substitution where we rename free variables. We have shown that the system has good properties such as confluence and strong normalizability and elaborated the conservativity theorem over the simply typed λ-calculus by taking account of α-conversions.
|
