Conditional Nested Pattern Matching in Interaction Net

TL;DR

This work addresses expressing nested pattern matching within interaction nets while preserving core properties such as one-step confluence. It introduces conditional nested pattern matching on values (nap) and proves that, for pairwise distinct rule sets, reductions remain confluent in one step. A translation, denoted $\mathbf{T}$, converts nested patterns into non-nested conditional rules, demonstrating conservativity and enabling implementation on existing evaluators. Additionally, a case-expression–like notation is proposed to express pattern matches cleanly, supporting practical programming of functional constructs with the parallelism and explicit garbage collection advantages of interaction nets.

Abstract

Interaction nets are a form of restricted graph rewrite system that can serve as a graphical or textual programming language. As such, benefits include one-step confluence, ease of parallelism and explicit garbage collection. However, some of these restrictions burden the programmer, so they have been extended in several ways, notably to include data types and conditional rules. This paper introduces a further extension to allow nested pattern matching and to do so in a way that preserves these benefits and fundamental properties of interaction nets. We also show that by introducing a translation to non-nested matching, this extension is conservative in rewriting. In addition, we propose a new notation to express this pattern matching.

Figures (1)

• Figure 1: An example of rules and rewritings of interaction nets