摘要
1.线性逻辑和张量理论在古典逻辑的 Gentzen 型矢列演算中Girard 去除弱规则和缩规则,发展起一种新型逻辑系统——线性逻辑(简记为 LL)。它不同于古典逻辑,本质上是一种事态逻辑(logic of situation),或者是一动作逻辑(logic of action),强调系统的动态特征与并发计算紧密相关。结构规则的去除自然在 LL 中导致了两种类型的连接词:乘性连接词和加性连接词,
Curry-Howard isomorphism has proved very fruitful as a methodological tool for exploiting the deep relationship among typed lambda calculus,intuitionistic logic and cartesian closed categories.A direct payoff of this has been the design of functional programming languages with powerful type systems.Linear logic is a logic of actions that seems well suited for concurrent computation.In this paper,we establish a correspondence between Petri nets,linear logic and sym- metric monoidal categories.
出处
《计算机科学》
CSCD
北大核心
1991年第6期17-24,共8页
Computer Science
