权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Relation between Semantics of Type Theory and its Syntactic Properties

类型论语义与其句法性质的关系

基本信息

批准号：
10680334
负责人：
SAKURAI Takafumi
金额：
$ 1.47万
依托单位：
Chiba University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
1998
资助国家：
日本
起止时间：
1998 至 1999
项目状态：
已结题

项目摘要

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.

1998年，我们得到了关于二阶λ-演算句法性质的模型论证明的一些结果。在二阶λ-演算的范畴论模型构造中，函数空间和二阶量化都是用伴随性来定义的。但是我们考虑了用半伴随性代替通常结构中的伴随性所得到的结构，发现它刻画了强正规化证明和β-正规形唯一性证明中常见的结构，当我们申请这个项目时，我们计划在1999年将上述结果推广到CC和PTS。事实上，我们发现双范畴更适合描述证明CC强规范化所必需的结构。但是，为了表明我们关于句法性质的模型论证明的总体方案可以应用于更广泛的领域，我们推迟了对发展的详细考察，并研究了子结构逻辑的性质。我们已经证明了无割可证性可以在使用FL-代数或SO-幺半群构造的语义结构中得到证明。通过这种构造，我们澄清了为什么无割可证性对某些子结构逻辑不成立的原因。此外，我们还利用这种结构构造了Kripke语义，并观察了它与直觉模态逻辑的Kripke语义的关系。但是我们发现，直觉模态逻辑的Kripke语义很难推广到子结构逻辑，因为直觉模态逻辑的Kripke语义是利用直觉模态逻辑的特性构造的。我们还研究了显式环境下的简单型λ演算，并证明了其基本性质，如合流性和强规范化性。强可规范化性证明的思想来自于语义，但现在完成的证明是纯语法的。