A semantic account of strong normalization in linear logic (Q276260)

The present paper further explores the connection between linear logic proofs (proof-nets) and the multiset based relational model of linear logic [\textit{J.-Y. Girard}, Theor. Comput. Sci. 50, 1--102 (1987; Zbl 0625.03037); the first author et al., Theor. Comput. Sci. 412, No. 20, 1884--1902 (2011; Zbl 1222.03070)]. The authors prove that it is possible to determine if the net obtained by cutting two cut-free nets is strongly normalizable, from the relational interpretations of the two cut-free nets. Moreover, being the former net strongly normalizable it is possible to determine the maximum length (i.e.\ the number of cut reduction steps) of its reduction sequences, once more by only referring to the interpretations of the two cut-free nets in the relational model. Similar questions apropos \textit{weakly} normalization and the number of cut reduction steps leading to the normal form were answered in [the first author et al., loc. cit.]. The strongly normalization variant, not surprisingly, raises new challenges addressed in the present paper. As a consequence of the authors' semantic approach an alternative proof of strong normalization for Multiplicative Exponential Linear Logic (MELL) is presented. This alternative proof does not rely on confluence. In [``Linear logic and strong normalization'', in: 24th international conference on rewriting techniques and applications (RTA 2013), Eindhoven, The Netherlands, June 24--26, 2013. Wadern: Schloss Dagstuhl -- Leibniz Zentrum für Informatik. 39--54 (2013; \url{doi:10.4230/LIPIcs.RTA.2013.39})], \textit{B. Accattoli} also gave a proof of strong normalization for MELL which does not use any form of confluence. The novelty of the present proof is that it keeps the structure `weak normalization + conservation theorem', being the conservation theorem an immediate consequence of the semantic approach not relying on the confluence result.