A coding theoretic study of MLL proof nets (Q2888855)

In this paper the author presents an original and novel approach for analysing proofs structures of multiplicative linear logic. In some sense, the author considers an abstraction of proof structures: the graphs obtained by forgetting the ``type'' of the multiplicative links (\(\otimes\) or \(\wp\)), and he studies the way to retrieve this information in such a way that one obtains correct proof nets.NEWLINENEWLINEThe methodology he uses is inspired by coding theory. He considers families of all proof structures that are pairwise equal up to some occurrences of \(\otimes/\wp\) links. Then he puts on these families a distance: the one corresponding to the numbers of distinct (\(\otimes\) versus \(\wp\)) multiplicative links. Then he proves: {\parindent=0.5cm\begin{itemize}\item[--] in a given family, the distance between two proof nets is greater to 2. In coding-theoretic terms this means that for such families of proofs structures, the code given by the subset of proof nets is ``one error detecting''; \item[--] in these families, the author considers some elementary transformations between proof structures: the ones consisting in replacing one \(\wp\)-link by one \(\otimes\)-link in the same time that one \(\otimes\)-link is replaced by one \(\wp\)-link.NEWLINENEWLINE\end{itemize}} He proves that between two proof nets belonging to a given family, there is a finite sequence of such elementary transformations in such a way that all terms of this sequence are proof nets belonging to this family. Therefore the minimal distance equal to 2 is reached. In terms of coding theory, this means that, in the code given by the set of proof nets, ``one error correction'' is impossible.NEWLINENEWLINEThen he characterizes the families containing at least one proof net. Its argument uses a particular element of a given family: the one in which all the multiplicative links are \(\otimes\)-links. When the underlying graph of this particular element is connected then the existence of a proof net in the given family is guaranteed. Moreover, the proof is constructive: it enables one to build a proof net belonging to the family when this latter contains indeed proof nets. This is the first step of an algorithm that enumerates all proof nets belonging to a given family. When the continuation of the algorithm uses the elementary transformations (exchanging one \(\otimes\)-link and one \(\wp\)-link) then the enumeration of all proof nets in the given family is realised in polynomial time.