• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

1997 Fiscal Year Annual Research Report

数学基礎論のプログラミング言語理論への応用

Research Project

Project/Area Number 09740162
Research InstitutionTokyo Woman's Christian University

Principal Investigator

永山 操  東京女子大学, 文理学部, 講師 (30237557)

KeywordsLinear Logic / proof nets / strongly planarity / Correctness theorem / Lambek Calculus
Research Abstract

昨年度までの、非可換なLinear Logicの証明図にあたるnon-commutative proof netsについての研究をさらに進めた。まず、今まであまり研究されていなかったnon-commutativeなsystemにおけるnetsの概念として、strongly planar marked nets導入し、そのwell-formed structureに対する必要充分条件について考察した。ここで、tree-likeな平面的グラフと、そのグラフによって仕切られるregionsとの条件を考えることにより、平面的グラフに対するオイラーの公式が適用できる。これにより、regionsがあるcondition(region condition)を満たす時、well-formed structureかどうかを調べるのに、旧来のswitching conditionにおいて行われたいた。サブグラフのacyclicityとconnectnessの検証がどちらか一方でよいことがわかった。さらにこのregion conditionのもとでは、switching conditionで考慮されるサブグラフの数も劇的に減らすことができた。旧来のswitching conditionでは、mをpar-linkの個数とすると、2のm乗個のサブグラフの検証が必要となる。しかし新しい必要充分条件では、L-only subgraphとR-only subgraphと呼ばれる2つのサブグラフの検証で充分である。これにより、定理として、marked netがwell-formedとなる必要十分条件は、Gがstrongly planarであり、region conditionを満たし、かつL-only subgraphとR-only subgraphがacyclicかconnectedのどちらか一方であることがわかった。さらに、これからCyclic Linear Logicのmultiplicative fragmentにおけるnon-commutative proof netの新しい特徴づけ定理も得られる。
このように、本年度は研究において大きな前進がみられた。来年度はさらにこれを進め、Non-commutative Linear LogicやLambek Calculusにおける定理の自動証明に適用できるような、具体的なアルゴリズムの研究を行っていきたい。

  • Research Products

    (3 results)

All Other

All Publications (3 results)

  • [Publications] Misao NAGAYAMA Mitsuhiro OKADA: "Characterization Theorems for Multiplicative Fragment of Intuitionistic Non-Commutative Linear Logic(Preliminary Report)" 数解研講究録. 818. 60-69 (1997)

  • [Publications] Misao NAGAYAMA Mitsuhiro OKADA: "A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic" Theoretical Computer Science. (Special issue)(to appear). (1998)

  • [Publications] Misao NAGAYAMA: "A Normalization Theorem for BB'I" Notre Dame Journal of Formal Logic. (to appear). (1998)

URL: 

Published: 1999-03-15   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi