| 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)
西崎 真也 東京工業大学, 大学院・情報理工学研究科, 助教授 (90263615)
腰越 秀之 千葉大学, 工学部, 助教授 (70110294)
|
|---|
| Project Period (FY) |
1998 – 1999
|
| Project Status |
Completed (Fiscal Year 1999)
|
| Budget Amount *help |
¥2,300,000 (Direct Cost: ¥2,300,000)
Fiscal Year 1999: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 1998: ¥1,400,000 (Direct Cost: ¥1,400,000)
|
|---|
| 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.
|
