Interaction nets and term-rewriting systems

被引:11
作者
Fernandez, M
Mackie, I
机构
[1] Ecole Normale Super, Liens, DMI, CNRS,URA 1327, F-75005 Paris, France
[2] Ecole Polytech, LIX, CNRS, URA 1439, F-91128 Palaiseau, France
关键词
term rewriting; interaction nets; termination; modularity;
D O I
10.1016/S0304-3975(97)00082-0
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Term-rewriting systems provide a framework in which it is possible to specify and program in a traditional syntax (oriented equations). Interaction nets, on the other hand, provide a graphical syntax for the same purpose, but can be regarded as being closer to an implementation since the reduction process is local and asynchronous, and all the operations are made explicit, including discarding and copying of data. Our aim is to bridge the gap between the above formalisms by showing how to understand interaction nets in a term-rewriting framework. This allows us to transfer results from one paradigm to the other, deriving syntactical properties of interaction nets from the (well-studied) properties of term-rewriting systems; in particular concerning termination and modularity.
引用
收藏
页码:3 / 39
页数:37
相关论文
共 30 条
[1]  
BANACH R, 1995, UMCS9572 U MANCH
[2]  
BARENDREGT HP, 1987, LECT NOTES COMPUT SC, V259, P141
[3]   TERMINATION OF REWRITING [J].
DERSHOWITZ, N .
JOURNAL OF SYMBOLIC COMPUTATION, 1987, 3 (1-2) :69-116
[4]  
Dershowitz N., 1989, HDB THEORETICAL COMP, VB
[5]  
Dershowitz Nachum, 1995, LECT NOTES COMPUTER
[6]  
FERNANDEZ M, 1995, LECT NOTES COMPUTER, V906, P255
[7]  
FERNANDEZ M, 1996, UNPUB TYPE ASSIGNMEN
[8]  
FERNANDEZ M, 1996, LECT NOTES COMPUTER, V1059, P149
[9]  
Fernandez M., 1996, LECT NOTES COMPUTER, V1140, P319
[10]  
Gay S., 1995, Theory and Formal Methods of Computing 94. Proceedings of the Second Imperial College Workshop, P63