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

Relation between Semantics of Logical System and its Syntactic Properties

逻辑系统语义与其句法性质的关系

基本信息

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

项目摘要

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.

通过证明割消定理和赋项，研究了模态子结构逻辑的割消运算如何被看作计算规则。由于模态子结构逻辑包含了直觉线性逻辑和直觉模态逻辑的特殊情况，因此可以对直觉线性逻辑和直觉模态逻辑的计算意义的类似研究给出一个统一的观点。到目前为止，许多这样的研究都是基于自然演绎，但我们已经分配的条款，以模态子结构逻辑在微积分风格。由于割规则对应于这种情况下的显式替换，我们能够应用有关显式替换的结果来获得直觉模态逻辑的项分配和割消运算作为计算规则。我们已经证明了一般情况下的割免可证性定理，但具体的割消运算及其性质还需要继续研究，我们还研究了带显式替换的类型λ-演算的推广，提出了一类上下文系统。上下文是一个带有漏洞的λ-项，它的引入是为了实现系统中的元级操作。在该系统中，不能使用传统的使用α-转换的替换操作，因此给出了一种新的定义替换的方法，即对自由变量进行重命名。我们证明了该系统具有良好的收敛性和强正规化性等性质，并通过考虑α-转换，阐述了简单型λ-演算的守恒性定理.