de Falco, Marc - An Explicit Framework for Interaction Nets

lmcs:1108 - Logical Methods in Computer Science, December 12, 2010, Volume 6, Issue 4
An Explicit Framework for Interaction Nets

Authors: de Falco, Marc

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.


Source : oai:arXiv.org:1010.1066
DOI : 10.2168/LMCS-6(4:6)2010
Volume: Volume 6, Issue 4
Published on: December 12, 2010
Submitted on: November 6, 2009
Keywords: Computer Science - Logic in Computer Science,F.1.1


Share

Consultation statistics

This page has been seen 50 times.
This article's PDF has been downloaded 38 times.