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

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

Research Project

Project/Area Number 08740160
Research Category

Grant-in-Aid for Encouragement of Young Scientists (A)

Allocation TypeSingle-year Grants
Research Field General mathematics (including Probability theory/Statistical mathematics)
Research InstitutionTokyo Woman's Christian University

Principal Investigator

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

Project Period (FY) 1996 – 1997
Project Status Completed (Fiscal Year 1996)
Budget Amount *help
¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 1996: ¥1,000,000 (Direct Cost: ¥1,000,000)
Keywords線形論理 / 非可換論理 / characterization Theorem / Strong planarity / Stack Condition
Research Abstract

今年度の最初の成果としては、現在プログラム言語理論や並列アルゴリズムといった分野から注目されている線型論理(linear logic)の、非可換な体系についての研究をさらに進めたことである。昨年度の岡田光弘(慶應大)との共同研究によってNon-commutative proof netのCharacterization Theoremを得たが、この研究においては、Non-commutative Linear logicの特徴づけとしてStrong Planarityとstack conditionによって定められるmarked Danos-regnier graphのサブクラスという新しい概念を定義した。strong planarityという概念は、結び目理論におけるRidemeister Moveを用いてplanar graphの交差を取り除く方法を分析し、その結果として得られた概念である。これらの結果をさらにAbrusciのNon-commutative Linear LogicやIntuitionistic Linear LogicのCharacterization Theoremへと応用することができた。
現在進めている研究では、より計算量の少ないNon-commutative Linear Logicの特徴づけを与えようとしている。今まで得られていたNon-commutative proof netの特徴づけは、全てCommutative proof netであることが条件であり、Non-commutative proof netの方がgraphとしては単純になっているにもかかわらず、最良の場合でも、少なくともCommutative proof netの判定に使われる計算量が必要であった。今、取り組んでいる定理では、交差のないgraph(plane graph)が与えられたとして、Commutative proof netであることを条件とせず、graphのlinkの位置関係と、L-only subgraphとR-only subgraphという二つのsubgraphから、直接Non-commutative proof netであるかどうか判定できる。今後このCharacterization Theormの理論的な計算量についてさらに考察を進めていくつもりである。

Report

(1 results)
  • 1996 Annual Research Report
  • Research Products

    (4 results)

All Other

All Publications (4 results)

  • [Publications] Misao Nagayama: "Syntactic Solution to the P-W problem" Notre Dame Journal of Formal Logic. (1997)

    • Related Report
      1996 Annual Research Report
  • [Publications] M.Nagayama and M.Okada: "A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-commutative Ligear Logic (Extended Abstract)" Electric Notes in Theoretical Computer Science. 3. (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] M.Nagayama and M.Okada: "Characterization theorems for Multiplicative Fragment of Intuitionistic Non-Commutative Linear Logic (Prelimirary Report)" 数理解析研究所講究録. (1997)

    • Related Report
      1996 Annual Research Report
  • [Publications] M.Nagayama and M.Okada: "A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic (Full version)" Theoretical Computer Science. (1997)

    • Related Report
      1996 Annual Research Report

URL: 

Published: 1996-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi