Differential interaction nets (Q860836): Difference between revisions

Differential interaction nets, introduced in this paper, arise naturally as a graphical though formal presentation of commutations satisfied by morphisms associated to modalities of linear logic. Using these nets, the authors provide a linear logic account for their earlier extension of lambda-calculus with differentiation, see [\textit{T. Ehrhard} and \textit{L. Regnier}, ``The differential lambda-calculus'', Theor. Comput. Sci. 309, No.~1--3, 1--41 (2003; Zbl 1070.68020)]. The authors also furnish a criterion for their net to be a correct differential net and prove this criterion to be preserved under reduction. They also show that correct nets are strongly normalizable. As the authors remark, differential nets can be viewed as a nondeterministic extension of multiplicative proof nets of linear logic, with certain exponential operations allowing several ``agents'' to communicate in a common ``broadcast area''.