权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

数理逻辑在编程语言理论中的应用

基本信息

批准号：
07740171
负责人：
永山操
金额：
$ 0.64万
依托单位：
Tokyo Woman's Christian University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
1995
资助国家：
日本
起止时间：
1995 至无数据
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-07740171/
关键词：
線型論理非可換論理 Characterization Theorem Strong planarity stack condition Type Theory higher order predicate logic

项目摘要

今年度の最初の成果としては、現在プログラム言語理論や並列アルゴリズムといった分野から注目されている線型論理(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の交差を取り除く方法を分析し、その結果として得られた概念である。現在進めている研究では、linear logicにおける計算モデルについて調べている。従来型の関数型プログラミング言語の理論的な基礎となるtype theoryのframe workに対し、linear logicよるtype-freeな推論をさらに付け加えて、higher order predicate logicより強力で無矛盾な体系が作れないかと言うことに興味をもっている。1989年の古森の論文にChurchのIntuitionistic Simple Type Theoryとtype-free affine ligicを含む体系を紹介したものがあり、その無矛盾性がopen problemであった。しかし、その体系が矛盾していることがGirard paradoxを埋め込むことにより証明できた。従って、そのparadoxを導くために使われた推論法則を分析し、無矛盾な体系に改良できないか検討中である。その結果、できるだけtype-freeの集合論に近いframe workの中で関数型プログラミング言語の基礎が作れないかということについて調べていきたい。

This year's initial results have been completed, and now the paper on the study of linear logic and non-commutative systems has been completed. Okada Mitsuhiro (Keio Daiichi) and his joint research on the Characterization Theorem of Non-communicative proof net were obtained. The characteristics of Non-communicative Linear Logic were determined by the stack condition and the concept of marked Danos-regnier graph was defined. strong planarity concept, knot theory, Ridemeister Move, analysis method, result, concept Now we are studying linear logic. The basic theory of speech is based on the type theory of frame work, linear logic, type-free inference, high order predicate logic, strong and non-contradictory system. The Intuitive Simple Type Theory of the Church and the Type-free affine ligic are introduced in 1989. The system is contradictory, and the Girard paradox is proof. The law of inference is analyzed and the system is improved without contradiction. As a result, type-free set theory is used in the framework of work related to the number of types of speech.