An Explicit Framework for Interaction Nets
Marc de Falco (CNRS)

TL;DR
This paper introduces an explicit, permutation-based framework for interaction nets, leveraging Geometry of Interaction concepts to clarify their structure and reduction, and proves strong confluence within this new formalism.
Contribution
It presents a novel permutation-based formalism for interaction nets, connecting them to proof-net quotients and providing a clearer, more explicit framework.
Findings
Proves strong confluence of reduction in the new framework
Shows interaction nets as quotients of generalized proof-nets
Provides an explicit permutation-based formalism
Abstract
Interaction nets are a graphical formalism inspired by Linear Logic proof-nets often used for studying higher order rewriting e.g. \Beta-reduction. Traditional presentations of interaction nets are based on graph theory and rely on elementary properties of graph theory. We give here a more explicit presentation based on notions borrowed from Girard's Geometry of Interaction: interaction nets are presented as partial permutations and a composition of nets, the gluing, is derived from the execution formula. We then define contexts and reduction as the context closure of rules. We prove strong confluence of the reduction within our framework and show how interaction nets can be viewed as the quotient of some generalized proof-nets.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
