In-place Graph Rewriting with Interaction Nets

TL;DR

This paper explores how interaction nets can be used to visually and formally verify whether algorithms are in-place, introducing annotations and an analysis method to identify in-place operations.

Contribution

It presents a formalism using interaction nets to identify and verify in-place algorithms, including an annotation system and an automatic analysis algorithm.

Findings

Interaction nets allow visual verification of in-place algorithms.

An annotation system indicates which parts of an algorithm run in-place.

An algorithm for automatic analysis of interaction rules to detect in-place operations.

Abstract

An algorithm is in-place, or runs in-situ, when it does not need any additional memory to execute beyond a small constant amount. There are many algorithms that are efficient because of this feature, therefore it is an important aspect of an algorithm. In most programming languages, it is not obvious when an algorithm can run in-place, and moreover it is often not clear that the implementation respects that idea. In this paper we study interaction nets as a formalism where we can see directly, visually, that an algorithm is in-place, and moreover the implementation will respect that it is in-place. Not all algorithms can run in-place however. We can nevertheless still use the same language, but now we can annotate parts of the algorithm that can run in-place. We suggest an annotation for rules, and give an algorithm to find this automatically through analysis of the interaction rules.