Interaction graphs: graphings

DOI10.1016/J.APAL.2016.10.007zbMATH Open1422.03131arXiv1405.6331OpenAlexW332750750MaRDI QIDQ345705FDOQ345705

Thomas Seiller

Publication date: 2 December 2016

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Abstract: In two previous papers, we exposed a combinatorial approach to the program of Geometry of Interaction, a program initiated by Jean-Yves Girard. The strength of our approach lies in the fact that we interpret proofs by simpler structures - graphs - than Girard's constructions, while generalizing the latter since they can be recovered as special cases of our setting. This third paper extends this approach by considering a generalization of graphs named graphings, which is in some way a geometric realization of a graph. This very general framework leads to a number of new models of multiplicative-additive linear logic which generalize Girard's geometry of interaction models and opens several new lines of research. As an example, we exhibit a family of such models which account for second-order quantification without suffering the same limitations as Girard's models.

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

Recommendations

• Interaction graphs: multiplicatives
• Interaction graphs: full linear logic
• Interaction graphs: exponentials
• Towards a typed geometry of interaction
• Interaction graphs: additives

zbMATH Keywords

linear logicmeasurable dynamicsdenotational semanticsgeometry of interactiondynamic semanticsinteraction graphs

Mathematics Subject Classification ID

Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Semantics in the theory of computing (68Q55) Nonsingular (and infinite-measure preserving) transformations (37A40)

Cites Work

• Title not available (Why is that?)
• Linear logic
• Elementary complexity and geometry of interaction
• Logarithmic space and permutations
• Title not available (Why is that?)
• Geometry of interaction. V: Logic in the hyperfinite factor
• Interaction graphs: multiplicatives
• Interaction graphs: additives
• Determinant theory in finite factors
• Cost of equivalence relations and groups
• Unary Resolution: Characterizing Ptime
• The geometry of linear higher-order recursion
• Three lightings of logic (Invited Talk)
• Title not available (Why is that?)
• Interaction graphs: graphings
• Title not available (Why is that?)
• Trees and amenable equivalence relations
• Title not available (Why is that?)
• Title not available (Why is that?)
• A correspondence between maximal abelian sub-algebras and linear logic fragments
• Title not available (Why is that?)
• On the cost of generating an equivalence relation
• Transcendental syntax I: deterministic case
• Title not available (Why is that?)
• Characterizingco-NLby a group action
• CONCUR 2005 – Concurrency Theory
• Typed lambda-calculus in classical Zermelo-Fraenkel set theory

Cited In (8)

• Title not available (Why is that?)
• Interaction graphs: additives
• Zeta functions and the (linear) logic of Markov processes
• Title not available (Why is that?)
• Interaction graphs: graphings
• Unifying lower bounds for algebraic machines, semantically
• Verificationism and Classical Realizability
• Title not available (Why is that?)

This page was built for publication: Interaction graphs: graphings

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