1999 Fiscal Year Final Research Report Summary
Relation between Semantics of Type Theory and its Syntactic Properties
| Project/Area Number |
10680334
|
|---|
| 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 Faculty of Science Professor, 理学部, 教授 (10022302)
TSUJI Takashi Chiba University Faculty of Science Professor, 理学部, 教授 (70016666)
|
|---|
| Project Period (FY) |
1998 – 1999
|
| Keywords | Type Theory / Semantics / Model / Category Theory / Syntactic Property / Strong Normalization / Substructural Logic |
|---|
| Research Abstract |
In 1998, we have obtained some results about model theoretic proof of syntactic properties of 2nd order λ-calculus. In the usual category theoretic model construction of 2nd order λ-calculus, function space and 2nd order quantification are defined using adjointness. But we considered the structure obtained by replacing adjointness used in the usual structure by sem-adjointness and found that it characterizes the structure common in the proof of strong normalization and that of uniqueness of β-normal form.
When we applied for this project, what we planned to do in 1999 was to develop the above results to CC and PTS. In fact, we found that bicategory is more appropriate to describe the structure necessary to prove the strong normalization of CC. But, to show that our general plan about the model theoretic proof of syntactic properties can be applied to wider area, we postponed the detailed investigation of the development and studied the properties of substructural logics. We have shown that cut-free provability can be proved in the semantic structure that is constructed using FL-algebra or so-monoid. By this construction, we have clarified the reason why the cut-free provability does not hold for some of the substructural logics. Furthermore, we have constructed the Kripke semantics using this structure and made observations on the relationship with the Kripke semantics of intuitionistic modal logics. But we found that it is hard to generalize the Kripke semantics of intuitionistic modal logics to that of substructure logics, because the Kripke semantics of intuitionistic modal logics is constructed using the properties specific to intuitionistic modal logics.
We have also studied the simply-typed λ-calculus with explicit environment and shown that fundamental properties such as confluence and strong normalizability hold. The idea of the proof of strong normalizability came from the semantics, but the completed proof is purely syntactical for now.
|
