
arXiv: 1405.6331
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.
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, F.3.2; F.4.1, Measurable dynamics, Semantics in the theory of computing, Linear logic, Proof-theoretic aspects of linear logic and other substructural logics, linear logic, Geometry of interaction, FOS: Mathematics, dynamic semantics, Interaction graphs, Denotational semantics, Logic in computer science, Nonsingular (and infinite-measure preserving) transformations, geometry of interaction, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Mathematics - Logic, Logic in Computer Science (cs.LO), [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], measurable dynamics, F.3.2, F.4.1, 03B70, 03F52, 28E15, interaction graphs, Logic (math.LO), Dynamic semantics, denotational semantics
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, F.3.2; F.4.1, Measurable dynamics, Semantics in the theory of computing, Linear logic, Proof-theoretic aspects of linear logic and other substructural logics, linear logic, Geometry of interaction, FOS: Mathematics, dynamic semantics, Interaction graphs, Denotational semantics, Logic in computer science, Nonsingular (and infinite-measure preserving) transformations, geometry of interaction, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Mathematics - Logic, Logic in Computer Science (cs.LO), [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], measurable dynamics, F.3.2, F.4.1, 03B70, 03F52, 28E15, interaction graphs, Logic (math.LO), Dynamic semantics, denotational semantics
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 5 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
