An Explicit Framework for Interaction Nets

DOI10.1007/978-3-642-02348-4_15MaRDI QIDQ5902126zbMATH OpenOpenAlexFDO

Authors Marc de Falco

Publication date 30 June 2009

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1010.1066

zbMATH Keywords

linear logicgeometry of interactiongraph rewritinginteraction nets

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

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.

Recommendations

• An explicit framework for interaction nets
• Interaction nets and term-rewriting systems
• scientific article; zbMATH DE number 1487844
• A calculus for interaction nets based on the linear chemical abstract machine
• Interaction nets for linear logic

Cites work

• scientific article; zbMATH DE number 1479606 (Why is no real title available?)
• scientific article; zbMATH DE number 1487844 (Why is no real title available?)
• scientific article; zbMATH DE number 1512623 (Why is no real title available?)
• scientific article; zbMATH DE number 786499 (Why is no real title available?)
• A categorical model for the geometry of interaction
• Encoding left reduction in the λ-calculus with interaction nets
• New foundations for the geometry of interaction
• On full abstraction for PCF: I, II and III
• Towards an algebraic theory of Boolean circuits.
• Traced monoidal categories
• YALE: yet another lambda evaluator based on interaction nets

Cited in

(14)

• On context semantics and interaction nets
• scientific article; zbMATH DE number 1487844 (Why is no real title available?)
• Interaction nets for linear logic
• Operational equivalence for interaction nets.
• The conservation theorem for differential nets
• An explicit framework for interaction nets
• Interaction graphs: multiplicatives
• The structure of interaction
• scientific article; zbMATH DE number 860037 (Why is no real title available?)
• Interaction nets and term-rewriting systems
• Structured Co-spans: An Algebra of Interaction Protocols
• In-place graph rewriting with interaction nets
• Interaction nets and term rewriting systems (extended abstract)
• Interaction Net Implementation of Additive and Multiplicative Structures

This page was built for publication: An Explicit Framework for Interaction Nets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5902126)