The Geometry of Interaction of Differential Interaction Nets

TL;DR

This paper develops a Geometry of Interaction framework for Differential Interaction Nets, extending the algebraic and computational understanding of non-deterministic programs within linear logic.

Contribution

It constructs a novel GoI for Differential Interaction Nets, linking it to MELL and providing an equational theory for the Multiplicative Additive fragment.

Findings

Established a GoI for Differential Interaction Nets

Linked the GoI to the one of MELL

Provided an equational theory for the Multiplicative Additive fragment

Abstract

The Geometry of Interaction purpose is to give a semantic of proofs or programs accounting for their dynamics. The initial presentation, translated as an algebraic weighting of paths in proofnets, led to a better characterization of the lambda-calculus optimal reduction. Recently Ehrhard and Regnier have introduced an extension of the Multiplicative Exponential fragment of Linear Logic (MELL) that is able to express non-deterministic behaviour of programs and a proofnet-like calculus: Differential Interaction Nets. This paper constructs a proper Geometry of Interaction (GoI) for this extension. We consider it both as an algebraic theory and as a concrete reversible computation. We draw links between this GoI and the one of MELL. As a by-product we give for the first time an equational theory suitable for the GoI of the Multiplicative Additive fragment of Linear Logic.