1993 Fiscal Year Annual Research Report
数学基礎論による代数のプログラミング言語理論への応用
| Project/Area Number |
05740143
|
|---|
| Research Institution | Tokyo Woman's Christian University |
|---|
Principal Investigator |
永山 操 東京女子大学, 文理学部, 助手 (30237557)
|
|---|
| Keywords | Substructural logic / P-W問題 / Relevant Logic |
|---|
| Research Abstract |
現在注目されている分野の中に、substructural logicsと呼ばれる非古典理論がある。その中でも、implicational logicsについての考察を主として行ったが、今年の成果はまずP-W問題のsyntacticなsolutionを与えることができたと言うことである。この問題は1960年代後半からrelevant logicianのだれもが取り組んだと言う難関であった。一応1984年に肯定的な解決を見たものの、その証明は難解であった。私はこのP-W問題について、normalization theoremと呼ばれる定理を用い、syntacticで、かつ明解な証明を与えることに成功した。このようにnormalization theoremは、syntaxを解明する方法としてとても有用であることがわかり、liniear logic,situation theoryといったコンピュータサイエンスの分野からも興味を持たれ始めている。
だが、一方でその定理の限界も明らかになった。Wと呼ばれるcontractionがある論理に対してはうまく働かないのである。とくに非可換な論理については、decidabilityといった基本的な問題すらまったく手つかずの状態である。わたしは今BIWと呼ばれるについて研究を進めているが、問題が山積しており、normalization theoremに変わる有力な定理もみつかっていないのが現状で、semanticsを用いた考察も行っている。M.DunnのGaggle theoryなどは興味深く、finite model propertyについての応用も調べてみる価値があり、そのような研究は多くの関心を集めると思う。
|
Research Products
(4 results)
-
[Publications] Misao,Nagayama: "On BCK-identities" Studia Logica. (1994)
-
[Publications] 永山 操: "ブール代数と分割について" 数解研講究録. 818. 60-69 (1992)
-
[Publications] Misao Nagayama: "Boolean Algebras and Commutative Regular Rings" Journal of Symbolic Logic. 57. 1305-1318 (1992)
-
[Publications] Misao Nagayama,C.Talcott: "An NQTHM Mechanization of“An Exercise in the Verification of Multi-Process Programs"" Report,Dept,of Computer Science,STAN-CS-91. 1370. 1-33 (1991)
