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

点击翻译按钮获取中文摘要

現在注目されている分野の中に、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についての応用も調べてみる価値があり、そのような研究は多くの関心を集めると思う。