Exponentials vs fixed points in linear logic

It has been known for a while that the exponential modalities of linear logic may be simulated by least and greatest fixed point operators. However it is apparently not widely known whether this simulation is faithful. In this post we explain that this is not the case, using only first principles of linear logic.

Linear logic

It would not be reasonable to recap all the foundations and motivations of linear logic here, so I will be brief. But let me first give some helpful pointers for further background. A good high-level reference is the SEP article [1]. Unfortunately there is (still!) no textbook on linear logic that I am aware of, but Dale Miller and Roberto Di Cosmo (the authors of the SEP article) each have produced some publicly available lecture notes, here and here respectively. There is always the original TCS paper of Jean-Yves Girard too [2].

Multiplicative additive linear logic

In a nutshell, (exponential-free) linear logic $\mathsf{MALL}$ decomposes the usual conjunction and disjunction connectives of classical propositional logic (CPL) into so-called additive and multiplicative versions:

\dfrac{\vdash\Gamma, A,B}{\vdash \Gamma, A \parr B}

\dfrac{\vdash \Gamma, A \quad \vdash \Delta, B}{\vdash \Gamma,\Delta, A \otimes B}

Each connective also comes with its own unit, $\bot,0,1,\top$ for $\parr,\oplus, \otimes, \&$ respectively. Of course these distinctions only make sense because linear logic is substructural [3]: it does not admit weakening and contraction in general (although exchange is typically permitted). Thus cedents should be construed as multisets, rather than lists or sets. At least one advantage of these sensitivities is that they play well with cut-elimination, admitting a more resource-sensitive analysis of normalisation via the Curry-Howard correspondence.

Note that linear logic is, by default, classical, with the additive connectives and multiplicative connectives respectively enjoying their own De Morgan dualities. In this way negation of a formula $A$ , written $A^\bot$ , can be reduced to atomic formulas by equalities $(A\otimes B)^\bot = A^\bot \parr B^\bot$ and so on; indeed this explains the one-sided presentation of the rules as above.

Exponentials

Now comes the funky part: exponentials! These allow us to recover structural behaviour, weakening and contraction, in a controlled manner:

$!\, \dfrac{\vdash ?\Gamma, A}{\vdash?\Gamma, !A}\qquad?\, \dfrac{\vdash\Gamma,A}{\vdash\Gamma,?A}\qquad\mathsf w \, \dfrac{\vdash \Gamma}{\vdash \Gamma, ?A}\qquad\mathsf c \, \dfrac{\vdash \Gamma, ?A,?A}{\vdash \Gamma, ?A}$

Adding the exponentials to $\mathsf{MALL}$ yields full (first-order, propositional) linear logic $\mathsf{LL}$ .

At first glance the exponentials look an awful lot like modalities [4]. Indeed the laws of the ! and ? are just those of S4 modalities, $\Box$ and $\Diamond$ respectively, along with structural rules. Exponentials also give us a way to relate the multiplicative and additive connectives, just like exponentiation in arithmetic relates addition and multiplication, namely by the ‘exponential isomorphism‘ $!(A \& B) =\, !A \otimes !B$ .

The problem of non-canonicity

One interesting aspect of the exponentials is that they are not canonical: if we introduce copies of the exponentials, say $!',?'$ satisfying the same respective laws as $!,?$ , we cannot prove that necessarily $!=!'$ and $?=?'$ on this basis alone (see Section 6.1 of [1]). This is in stark contrast with the multiplicative and additive connectives, which are indeed canonical in this way.

An interpretation of the exponentials by fixed points

The recovery of structural behaviour by exponentials allows for complex cut-elimination behaviour. For instance, we can embed all of intuitionistic propositional logic (IPL) into $\mathsf{LL}$ by Girard’s embedding, which in particular interprets $A\to B \, :=\, !A \multimap B$ (where $A\multimap B := A^\bot \parr B$ ). However, this is not the only way to recover such behaviours. An alternative is via extremal fixed points.

Least and greatest fixed points

We may expand the syntax of formulas to allow expressions of the form $\mu X A(X)$ and $\nu X A(X)$ , where $X$ is a propositional variable. Very roughly the intended reading is as the least and greatest fixed points, respectively, of $X\mapsto A(X)$ . This is formalised by their inference rules:

$\mu\, \dfrac{\vdash \Gamma, A(\mu X A(X))}{\vdash \Gamma, \mu XA(X)}\qquad\nu\, \dfrac{\vdash\Gamma, B \quad \vdash B^\bot , A(B)}{\vdash \Gamma , \nu X A(X)}$

The system $\mu\mathsf{MALL}$ , extending $\mathsf{MALL}$ by the rules above, was introduced and studied by David Baelde and Dale Miller in [5] and [6].

Under duality of $\mu$ and $\nu$ , i.e. $(\nu X A(X))^\bot = \mu X A^\bot(X)$ (and symmetrically), these rules are induced from the ‘least prefixed point’ reading of $\mu$ (dually, ‘greatest postfixed point’ for $\nu$ ), à la Knaster-Tarski. Similar rules and axioms are found across mathematical and computational logic, for instance in extensions of Peano Arithmetic by inductive definitions. In linear logic fixed points are best understood in Curry-Howard style. For instance we can write a type of natural numbers $N:= \mu X (1 \oplus X)$ , and then a type of streams, $S := \nu Y (N \otimes Y)$ . Further examples can be found in [7].

Simulating exponentials with fixed points

More interestingly, we can interpret the exponentials themselves as fixed points!

$\begin{array}{r@{\ := \ }l}?'A & \mu X (\bot \oplus A \oplus (X \parr X)) \\!'A & \nu X (1 \, \& \, A\, \& (X \otimes X))\end{array}$

It is not hard to see that all the rules for exponentials can be derived for the encodings above, crucially using coinduction (i.e. the $\nu$ rule) to simulate promotion (i.e. the ! rule). Writing $\mu\mathsf{LL}$ for the extension of $\mathsf{MALL}$ by both exponentials and fixed points, we have:

Proposition 1. ([6]) If $\mu \mathsf{LL} \vdash \Gamma(!,?)$ then $\mu \mathsf{MALL} \vdash \Gamma(!',?')$ .

Non-faithfulness via non-canonicity

Can we establish a converse to Proposition 1 above? This question was left open by Baelde in [6], and seems to generally have been a curiosity within the community over the last 15 years or so. At least one reason to believe this should not be the case is that fixed points are, in a sense, canonical by their extremal characterisations. It turns out we can make this intuition precise.

An induction principle

$?'A$ does not only satisfy the rules of $?A$ , it is designed to be the least such formula. Write $E_A(Y)$ for, informally, ‘ $Y$ is a ?-exponential of $A$ ‘. Formally:

$E_A(Y)\, := \, ! ((\bot \multimap Y) \& ( A \multimap Y) \& ((Y\parr Y)\multimap Y))$

Since $?'A$ is the ‘least ?-exponential’ of $A$ , we can prove that it implies any other ?-exponential of $A$ :

Proposition 2. $\mu \mathsf{LL} \vdash ?'A \multimap E_A(Y) \multimap Y$ .

Proof. By induction on $?'A$ (equivalently coinduction on $!'A^\bot$ ), with invariant $E_A(Y) \multimap Y$ .

The syntactic proof is below, with principal formulas coloured in pink. Some identities, routine derivations and repeated premisses have been omitted to save horizontal space.

(Note here that $E_A(Y)^\bot =\, ?((\bot \otimes Y^\bot) \oplus (A\otimes Y^\bot) \oplus ((Y\parr Y)\otimes Y^\bot))$ .)

Show further proof details

Hide proof details

Separation via proof search

On the other hand, as one might expect, we cannot prove a similar property for the usual ?:

Proposition 3. $\mathsf{LL} \nvdash ?A \multimap E_A(Y) \multimap Y$ .

Proof. By analysis of cut-free proof search.

Note that any such proof must have $!A^\bot$ (i.e. $?A$ on the left of $\multimap$ ) principal somewhere, by consideration of the : otherwise set $?A = \mathtt{true}$ and $Y=A=\mathtt{false}$ elsewhere for a formula that is classically false. However this can only occur when there are only ?-formulas in the context, by inspection of the !-rule. By the subformula property in $\mathsf{LL}$ such a sequent must be $E_A(Y)^\bot,!A^\bot$ (or just $!A^\bot$ ). Again this has an unprovable projection to classical logic: just set $B=A=\mathtt{true}$ everywhere.

Show further proof details

Hide proof details

So we have identified a separating formula! Indeed, the usual exponentials $!,?$ cannot simulate their fixed point encodings $!',?'$ respectively in linear logic. Note that, though the separation above makes use of the exponentials themselves, as $?A \multimap E_A(Y) \multimap Y$ contains both $!,?$ and their fixed point encodings $!',?'$ , it can be made exponential-free by Proposition 1.

Corollary 4. There is a formula $S(!,?)$ , with all exponentials distinguished, such that $\mu\mathsf{MALL} \vdash S(!',?')$ but $\mathsf{LL}\nvdash S(!,?)$ .

Conclusions

In hindsight, the separation above is quite natural and hardly seems surprising. This is a good thing! It is reassuring when something turns out to be ‘obvious’ all along, not least as it emphasises the correct intuitions, which were certainly clear from various previous works, e.g. [5], [6], [8], [9].

The argument for non-provability of $S(!,?)$ in $\mathsf{LL}$ was via cut-free proof search, but it would be nice to construct an appropriate countermodel by way of phase semantics [10] (see also the recent [9] for phase semantics of variations of $\mu\mathsf{MALL}$ ). In a more proof relevant direction, it would be interesting to further examine this separation from a Curry-Howard viewpoint: what are the inhabitants of $?'A$ and $!'A$ , that are not typed by $?A$ and $!A$ , respectively? I understand that these last two directions are the subject of ongoing investigations by Abhishek De, Farzad Jafarrahmani and Alexis Saurin.

Acknowledgements

I would like to thank David Baelde, Eben Blaisdell, Kostia Chardonnet, Gianluca Curzi, Abhishek De, Dale Miller and Alexis Saurin for several interesting conversations leading to the observations in this post, in particular during LICS ’23 in Boston.

References

[1] R. Di Cosmo and D. Miller, “Linear Logic,” in The Stanford Encyclopedia of Philosophy, Fall 2023 ed., E. N. Zalta and U. Nodelman, Eds., Metaphysics Research Lab, Stanford University, 2023.
[Bibtex]

@InCollection{sep-logic-linear,
author =  {Di Cosmo, Roberto and Miller, Dale},
title =  {{Linear Logic}},
booktitle =  {The {Stanford} Encyclopedia of Philosophy},
editor =  {Edward N. Zalta and Uri Nodelman},
howpublished =  {\url{https://plato.stanford.edu/archives/fall2023/entries/logic-linear/}},
year =  {2023},
edition =  {Fall 2023},
publisher =  {Metaphysics Research Lab, Stanford University}
}

[2]

J. Girard, “Linear Logic,” Theor. Comput. Sci., vol. 50, p. 1–102, 1987.
[Bibtex]

@article{Girard87,
author = {Jean-Yves Girard},
title = {Linear Logic},
journal = {Theor. Comput. Sci.},
volume = {50},
pages = {1--102},
year = {1987},
url = {https://doi.org/10.1016/0304-3975(87)90045-4},
doi = {10.1016/0304-3975(87)90045-4},
timestamp = {Wed, 17 Feb 2021 22:00:41 +0100},
biburl = {https://dblp.org/rec/journals/tcs/Girard87.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

[3] G. Restall, “Substructural Logics,” in The Stanford Encyclopedia of Philosophy, {S}pring 2018 ed., E. N. Zalta, Ed., Metaphysics Research Lab, Stanford University, 2018.
[Bibtex]

@InCollection{sep-logic-substructural,
author =  {Restall, Greg},
title =  {{Substructural Logics}},
booktitle =  {The {Stanford} Encyclopedia of Philosophy},
editor =  {Edward N. Zalta},
howpublished =  {\url{https://plato.stanford.edu/archives/spr2018/entries/logic-substructural/}},
year =  {2018},
edition =  {{S}pring 2018},
publisher =  {Metaphysics Research Lab, Stanford University}
}

[4] J. Garson, “Modal Logic,” in The Stanford Encyclopedia of Philosophy, {S}pring 2024 ed., E. N. Zalta and U. Nodelman, Eds., Metaphysics Research Lab, Stanford University, 2024.
[Bibtex]

@InCollection{sep-logic-modal,
author =  {Garson, James},
title =  {{Modal Logic}},
booktitle =  {The {Stanford} Encyclopedia of Philosophy},
editor =  {Edward N. Zalta and Uri Nodelman},
howpublished =  {\url{https://plato.stanford.edu/archives/spr2024/entries/logic-modal/}},
year =  {2024},
edition =  {{S}pring 2024},
publisher =  {Metaphysics Research Lab, Stanford University}
}

[5]

D. Baelde and D. Miller, “Least and Greatest Fixed Points in Linear Logic,” in Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings, 2007, p. 92–106.
[Bibtex]

@inproceedings{BaeldeMiller07,
author = {David Baelde and
Dale Miller},
editor = {Nachum Dershowitz and
Andrei Voronkov},
title = {Least and Greatest Fixed Points in Linear Logic},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 14th
International Conference, {LPAR} 2007, Yerevan, Armenia, October 15-19,
2007, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4790},
pages = {92--106},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-75560-9\_9},
doi = {10.1007/978-3-540-75560-9\_9},
timestamp = {Sat, 09 Apr 2022 12:44:41 +0200},
biburl = {https://dblp.org/rec/conf/lpar/BaeldeM07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

[6]

D. Baelde, “Least and Greatest Fixed Points in Linear Logic,” ACM Trans. Comput. Log., vol. 13, iss. 1, p. 2:1–2:44, 2012.
[Bibtex]

@article{Baelde12,
author = {David Baelde},
title = {Least and Greatest Fixed Points in Linear Logic},
journal = {{ACM} Trans. Comput. Log.},
volume = {13},
number = {1},
pages = {2:1--2:44},
year = {2012},
url = {https://doi.org/10.1145/2071368.2071370},
doi = {10.1145/2071368.2071370},
timestamp = {Tue, 06 Nov 2018 12:51:53 +0100},
biburl = {https://dblp.org/rec/journals/tocl/Baelde12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

[7]

D. Baelde, A. Doumane, and A. Saurin, “Infinitary Proof Theory: the Multiplicative Additive Case,” in 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), Dagstuhl, Germany, 2016, p. 42:1–42:17.
[Bibtex]

@InProceedings{BDS16,
author =  {Baelde, David and Doumane, Amina and Saurin, Alexis},
title =  {{Infinitary Proof Theory: the Multiplicative Additive Case}},
booktitle =  {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages =  {42:1--42:17},
series =  {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN =  {978-3-95977-022-4},
ISSN =  {1868-8969},
year =  {2016},
volume =  {62},
editor =  {Talbot, Jean-Marc and Regnier, Laurent},
publisher =  {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address =  {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.42},
URN = {urn:nbn:de:0030-drops-65825},
doi = {10.4230/LIPIcs.CSL.2016.42},
annote =  {Keywords: Infinitary proofs, linear logic}
}

[8]

A. Saurin, “A Linear Perspective on Cut-Elimination for Non-wellfounded Sequent Calculi with Least and Greatest Fixed-Points,” in Automated Reasoning with Analytic Tableaux and Related Methods – 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings, 2023, p. 203–222.
[Bibtex]

@inproceedings{Saurin23,
author = {Alexis Saurin},
editor = {Revantha Ramanayake and
Josef Urban},
title = {A Linear Perspective on Cut-Elimination for Non-wellfounded Sequent
Calculi with Least and Greatest Fixed-Points},
booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 32nd
International Conference, {TABLEAUX} 2023, Prague, Czech Republic,
September 18-21, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14278},
pages = {203--222},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-43513-3\_12},
doi = {10.1007/978-3-031-43513-3\_12},
timestamp = {Wed, 01 Nov 2023 08:59:02 +0100},
biburl = {https://dblp.org/rec/conf/tableaux/Saurin23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

[9]

A. De, F. Jafarrahmani, and A. Saurin, “Phase Semantics for Linear Logic with Least and Greatest Fixed Points,” in 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022), Dagstuhl, Germany, 2022, p. 35:1–35:23.
[Bibtex]

@InProceedings{DJS22,
author =  {De, Abhishek and Jafarrahmani, Farzad and Saurin, Alexis},
title =  {{Phase Semantics for Linear Logic with Least and Greatest Fixed Points}},
booktitle =  {42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
pages =  {35:1--35:23},
series =  {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN =  {978-3-95977-261-7},
ISSN =  {1868-8969},
year =  {2022},
volume =  {250},
editor =  {Dawar, Anuj and Guruswami, Venkatesan},
publisher =  {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address =  {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.35},
URN = {urn:nbn:de:0030-drops-174272},
doi = {10.4230/LIPIcs.FSTTCS.2022.35},
annote =  {Keywords: Linear logic, fixed points, phase semantics, closure ordinals, cut elimination}
}

[10] J. Girard, “Linear logic: its syntax and semantics,” in Proceedings of the workshop on Advances in linear logic, 1995, p. 1–42.
[Bibtex]

@inproceedings{Girard95,
title={Linear logic: its syntax and semantics},
author={Girard, Jean-Yves},
booktitle={Proceedings of the workshop on Advances in linear logic},
pages={1--42},
year={1995}
}

	Disjunction	Conjunction
Multiplicative	$\dfrac{\vdash\Gamma, A,B}{\vdash \Gamma, A \parr B}$	$\dfrac{\vdash \Gamma, A \quad \vdash \Delta, B}{\vdash \Gamma,\Delta, A \otimes B}$
Additive	$\dfrac{\vdash \Gamma, A_i}{\vdash \Gamma, A_0 \oplus A_1}$	$\dfrac{\vdash \Gamma , A \quad \Gamma , B}{\vdash \Gamma, A \& B}$