Call-by-Name and Call-by-Value as Token-Passing Interaction Nets

Two common misbeliefs about encodings of the λ-calculus in interaction nets (INs) are that they are good only for strategies that are not very well understood (e.g. optimal reduction) and that they always have to deal in a complex way with boxes. In brief, the theory of interaction nets is more or less disconnected from the standard theory: we can do things in INs that we cannot do with terms, which is true [5, 10]; and we cannot do in INs things that can easily be done with terms. This paper contributes to fighting this misbelief by showing that the standard call-by-name and call-by-value strategies of the λ-calculus are encoded in interaction nets in a very simple and extensible way, and in particular that these encodings do not need any notion of box. This work can also be seen as a first step towards a generic approach to derive graph-based machines.

• Type: Conference
• Year: 2005
• Where: TLCA
• Authors: François-Régis Sinot
• Keywords: Common Misbeliefs, Interaction Nets, Optimal Reduction, Theoretical Computer Science, TLCA 2005