An Explicit Framework for Interaction Nets
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...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2010-12-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1108/pdf |
| Summary: | 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. |
|---|---|
| ISSN: | 1860-5974 |