交互作用网理论分析

ON THEORETICAL ISSUES OF INTERACTION NETS

交互作用网是Lafont于1990年在POPL会议上提出的一种程序设计语言.本文我们从证明和程序的关系出发,使用线性逻辑作为一种集成逻辑讨论交互作用网的理论性质,得到下述结论:·网上结点辅助端口的划分可表示成相应类型的张量积;·网上的计算等价于线性矢列演算中Principal-Cut的消去;·对于任何一个交互作用网,如果存在一个线性矢列演算与之对应,则该网是简单的.

Using linear logic as an integrated logic, this paper deals with the theoretical issues of interaction nets. The result shows:partition of auxiliary ports of a symbol can be described by tensor product;computation on nets equals principal-cut elimination;a net is simple when there is some coreesponding linear sequent calculus.