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 条
[11]  
Girard J.Y., 1989, LOGIC C, V88
[12]   LINEAR LOGIC [J].
GIRARD, JY .
THEORETICAL COMPUTER SCIENCE, 1987, 50 (01) :1-102
[13]  
Gonthier G., 1992, P 19 ACM S PRINC PRO, P15, DOI DOI 10.1145/143165.143172
[14]  
JOUANNAUD JP, 1995, PROOF COMPUTATION CO, V139, P173
[15]   ON THE ADEQUACY OF GRAPH REWRITING FOR STIMULATING TERM REWRITING [J].
KENNAWAY, JR ;
KLOP, JW ;
SLEEP, MR ;
DEVRIES, FJ .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (03) :493-523
[16]   TRANSFINITE REDUCTIONS IN ORTHOGONAL TERM REWRITING-SYSTEMS [J].
KENNAWAY, R ;
KLOP, JW ;
SLEEP, R ;
DEVRIES, FJ .
INFORMATION AND COMPUTATION, 1995, 119 (01) :18-38
[17]  
KLOP JW, 1980, COMBINATORY REDUCTIO, V127
[18]  
KLOP JW, 1992, HDB LOGIC COMPUTER S, V2
[19]   MODULARITY IN NONCOPYING TERM REWRITING [J].
KURIHARA, M ;
OHUCHI, A .
THEORETICAL COMPUTER SCIENCE, 1995, 152 (01) :139-169
[20]  
Lafont Y., 1995, LONDON MATH SOC LECT, P225