Interaction nets and term-rewriting systems

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.

Authors

• Maribel Fernández
• Ian Mackie

Keywords

• Term rewriting
• Interaction nets
• Termination
• Modularity