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

geometry of interactiongraph rewritinginteraction netslinear logic

Mathematics Subject Classification ID

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

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

• A categorical model for the geometry of interaction
• Encoding left reduction in the λ-calculus with interaction nets
• 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?)
• 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

(15)

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

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)