A linear algorithm for MLL proof net correctness and sequentialization (Q534705): Difference between revisions

The paper presents in full detail a linear algorithm for verifying the correctness of proof nets for multiplicative linear logic without units. It extends a previous paper of the same author [\textit{S. Guerrini}, ``Correctness of multiplicative proof nets is linear'', in: 14th symposium on logic in computer science, Trento, 1999. Los Alamitos, CA: IEEE Computer Society Press. 454--463 (1999)], where the linear algorithm (a pioneer in the literature on implementing a correctness criterion for multiplicative proof structures in linear time) was first introduced. The algorithm, which is linear when executed on sequential RAMs, is essentially a reformulation of Danos' contractibility criterion in terms of a sort of unification [\textit{V. Danos}, Une application de la logique linéaire à l'étude des processus de normalisation (principalement du lambda-calcul). Ph.D. Thesis, Université Paris 1 (1990); \textit{S. Guerrini} and \textit{A. Masini}, Theor. Comput. Sci. 254, No. 1--2, 317--335 (2001; Zbl 0974.68077); \textit{Y. Lafont}, Lond. Math. Soc. Lect. Note Ser. 222, 225--247 (1995; Zbl 0830.03028)]. A direct implementation of the unification criterion, which can be formulated as a disjoint-set union-find problem, leads to a quasi-linear algorithm. The solution results essentially from an efficient implementation of parsing as a sort of unification. Linearity was achieved after observing that the disjoint-set union-find at the basis of the unification criterion is a special case of union-find with a real linear-time solution. For related work in the area see [\textit{A. S. Murawski} and \textit{C.-H. L. Ong}, ``Dominator trees and fast verification of proof nets'', in: 15th annual IEEE symposium on logic in computer science, Santa Barbara, CA, 2000. Los Alamitos, CA: IEEE Computer Society Press. 181--191 (2000); \textit{A. S. Murawski} and \textit{C.-H. L. Ong}, ``Fast verification of MLL proof nets via IMLL'', ACM Trans. Comput. Log. 7, No. 3, 473--498 (2006)].