Relation between Semantics of Logical System and its Syntactic Properties

通过证明切消定理和赋值项，研究了如何将模态子结构逻辑的切消运算看作计算规则。由于模态子结构逻辑中包含了作为特例的直觉线性逻辑和直觉模态逻辑，因此我们可以对直觉线性逻辑和直觉模态逻辑的计算意义的类似研究给出一个综合的观点。到目前为止，许多这样的研究都是基于自然演绎的，但我们已经将术语分配给了以顺序演算方式给出的模态子结构逻辑。由于切规则对应于这种情况下的显式替换，因此我们能够将关于显式替换的结果应用于直觉模态逻辑的项赋值和切消运算作为计算规则。我们已经证明了一般情况下的无割可证性定理，但具体的消割运算及其性质还需要继续研究。我们还研究了带显式代换的类型化λ微积分的推广，并提出了一类环境下的系统。上下文是一个带孔的λ术语，它被引入来实现系统内部的元级操作。在系统中，由于不能使用传统的α-转换的替换操作，因此给出了一种新的替换定义方法，即重命名自由变量。证明了该系统具有良好的合流性和强归一化性，并在考虑α-变换的情况下，给出了简单型λ-微积分的保守性定理。

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.