Project/Area Number  10680334 
Research Category 
GrantinAid for Scientific Research (C).

Section  一般 
Research Field 
計算機科学

Research Institution  Chiba University 
Principal Investigator 
SAKURAI Takafumi Chiba University Faculty of Science Assistant Professor, 理学部, 助教授 (60183373)

CoInvestigator(Kenkyūbuntansha) 
西崎 真也 東京工業大学, 大学院・情報理工学研究科, 助教授 (90263615)
腰越 秀之 千葉大学, 工学部, 助教授 (70110294)
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 Fiscal Year 
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 semadjointness 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 cutfree provability can be proved in the semantic structure that is constructed using FLalgebra or somonoid. By this construction, we have clarified the reason why the cutfree 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 simplytyped λ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.
