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.