Interaction graphs: additives
From MaRDI portal
Publication:892169
Abstract: Geometry of Interaction (GoI) is a kind of semantics of linear logic proofs that aims at accounting for the dynamical aspects of cut-elimination. We present here a parametrized construction of a Geometry of Interaction for Multiplicative Additive Linear Logic (MALL) in which proofs are represented by families of directed weighted graphs. Contrarily to former constructions dealing with additive connectives, we are able to solve the known issue of obtaining a denotational semantics for MALL by introducing a notion of observational equivalence. Moreover, our setting has the advantage of being the first construction dealing with additives where proofs of MALL are interpreted by finite objects. The fact that we obtain a denotational model of MALL relies on a single geometric property, which we call the trefoil property, from which we obtain, for each value of the parameter, adjunctions. We then proceed to show how this setting is related to Girard's various constructions: particular choices of the parameter respectively give a combinatorial version of his latest GoI, a refined version of older Geometries of Interaction based on nilpotency. This shows the importance of the trefoil property underlying our constructions since all known GoI construction to this day rely on particular cases of it.
Recommendations
- Additive compound graphs
- Interaction graphs: multiplicatives
- Interaction graphs: graphings
- Interaction graphs: exponentials
- Additive and multiplicative models and interactions
- Additive operations on flow graphs
- A class of additive multiplicative graph functions
- scientific article; zbMATH DE number 639414
- Additively graceful graphs
- Additive graph spanners
Cites work
- Characterizingco-NLby a group action
- Determinant theory in finite factors
- Geometry of Interaction and linear combinatory algebras
- Geometry of interaction. V: Logic in the hyperfinite factor
- scientific article; zbMATH DE number 4179372 (Why is no real title available?)
- scientific article; zbMATH DE number 4099289 (Why is no real title available?)
- scientific article; zbMATH DE number 194205 (Why is no real title available?)
- scientific article; zbMATH DE number 4123722 (Why is no real title available?)
- scientific article; zbMATH DE number 2134919 (Why is no real title available?)
- scientific article; zbMATH DE number 1841811 (Why is no real title available?)
- scientific article; zbMATH DE number 786499 (Why is no real title available?)
- scientific article; zbMATH DE number 786500 (Why is no real title available?)
- scientific article; zbMATH DE number 5038458 (Why is no real title available?)
- Interaction graphs: multiplicatives
- Linear logic
- New foundations for the geometry of interaction
- Normativity in logic
- Typed lambda-calculus in classical Zermelo-Fraenkel set theory
Cited in
(13)- Logarithmic space and permutations
- Interaction graphs: graphings
- scientific article; zbMATH DE number 6917940 (Why is no real title available?)
- A correspondence between maximal abelian sub-algebras and linear logic fragments
- Geometry of interaction for MALL via Hughes-Van Glabbeek proof-nets
- Interaction graphs: full linear logic
- A \(\mathsf{MALL}\) geometry of interaction based on indexed linear logic
- Coherent interaction graphs
- Interaction graphs: exponentials
- Computer Science Logic
- Zeta functions and the (linear) logic of Markov processes
- Interaction graphs: multiplicatives
- Linear realisability over nets: multiplicatives
This page was built for publication: Interaction graphs: additives
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q892169)
