Sharing and Linear Logic with Restricted Access

Abstract The two Girard translations provide two different means of obtaining embeddings of Intuitionistic Logic into Linear Logic, corresponding to different lambda-calculus calling mechanisms. The translations, mapping $$A\rightarrow B$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>A</mml:mi> <mml:mo>→</mml:mo> <mml:mi>B</mml:mi> </mml:mrow> </mml:math> respectively to $${!}{A}\multimap B$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mo>!</mml:mo> <mml:mi>A</mml:mi> <mml:mo>⊸</mml:mo> <mml:mi>B</mml:mi> </mml:mrow> </mml:math> and $${!}{(A\multimap B)}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mo>!</mml:mo> <mml:mrow> <mml:mo>(</mml:mo> <mml:mi>A</mml:mi> <mml:mo>⊸</mml:mo> <mml:mi>B</mml:mi> <mml:mo>)</mml:mo> </mml:mrow> </mml:mrow> </mml:math> , have been shown to correspond respectively to call-by-name and call-by-value. In this work, we split the of-course modality of linear logic into two modalities, written “ $${!} $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mo>!</mml:mo> </mml:math> ” and “ $$\bullet $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mo>∙</mml:mo> </mml:math> ”. Intuitively, the modality “ $${!} $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mo>!</mml:mo> </mml:math> ” specifies a subproof that can be duplicated and erased, but may not necessarily be “accessed”, i.e. interacted with, while the combined modality “ $${!}{\bullet }$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mo>!</mml:mo> <mml:mo>∙</mml:mo> </mml:mrow> </mml:math> ” specifies a subproof that can moreover be accessed. The resulting system, called $$\textsf{MSCLL}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>MSCLL</mml:mi> </mml:math> , enjoys cut-elimination and is conservative over $$\textsf{MELL}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>MELL</mml:mi> </mml:math> . We study how restricting access to subproofs provides ways to control sharing in evaluation strategies. For this, we introduce a term-assignment for an intuitionistic fragment of $$\textsf{MSCLL}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>MSCLL</mml:mi> </mml:math> , called the $$\lambda ^{{!}{\bullet }}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mi>λ</mml:mi> <mml:mrow> <mml:mo>!</mml:mo> <mml:mo>∙</mml:mo> </mml:mrow> </mml:msup> </mml:math> -calculus, which we show to enjoy subject reduction, confluence, and strong normalization of the simply typed fragment. We propose three sound and complete translations that respectively simulate call-by-name, call-by-value, and a variant of call-by-name that shares the evaluation of its arguments (similarly as in call-by-need). The translations are extended to simulate the Bang-calculus, as well as weak reduction strategies.