Proof Nets and the Linear Substitution Calculus

TL;DR

This paper demonstrates the isomorphism between the linear substitution calculus with sharing and proof nets in linear logic, providing insights into their relationship and a new abstract notion of proof net.

Contribution

It establishes an operational isomorphism between the linear substitution calculus and proof nets, and characterizes proof net equality over sharing terms.

Findings

Linear substitution calculus is isomorphic to proof nets at the operational level.

Different sharing terms can have the same proof net representation.

Proposes a new abstract notion of proof net based on rewriting, not graphical representation.

Abstract

Since the very beginning of the theory of linear logic it is known how to represent the $\lambda$-calculus as linear logic proof nets. The two systems however have different granularities, in particular proof nets have an explicit notion of sharing---the exponentials---and a micro-step operational semantics, while the $\lambda$-calculus has no sharing and a small-step operational semantics. Here we show that the \emph{linear substitution calculus}, a simple refinement of the $\lambda$-calculus with sharing, is isomorphic to proof nets at the operational level. Nonetheless, two different terms with sharing can still have the same proof nets representation---a further result is the characterisation of the equality induced by proof nets over terms with sharing. Finally, such a detailed analysis of the relationship between terms and proof nets, suggests a new, abstract notion of proof net, based on rewriting considerations and not necessarily of a graphical nature.