A linear algorithm for MLL proof net correctness and sequentialization (Q534705): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(4 intermediate revisions by 4 users not shown) | |||
Property / review text | |||
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)]. | |||
Property / review text: 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)]. / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Gilda Ferreira / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F52 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F07 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68Q25 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 5886383 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
multiplicative linear logic | |||
Property / zbMATH Keywords: multiplicative linear logic / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
proof nets | |||
Property / zbMATH Keywords: proof nets / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/j.tcs.2010.12.021 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2011228482 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The structure of multiplicatives / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A linear-time algorithm for a special case of disjoint set union / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Linear logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Parsing MELL proof nets / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Correctness of Multiplicative (and Exponential) Proof Structures is NL-Complete / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4842976 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: An Efficient Unification Algorithm / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Fast verification of MLL proof nets via IMLL / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A new correctness criterion for the proof nets of non-commutative multiplicative linear logics / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Efficiency of a Good But Not Linear Set Union Algorithm / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 01:28, 4 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A linear algorithm for MLL proof net correctness and sequentialization |
scientific article |
Statements
A linear algorithm for MLL proof net correctness and sequentialization (English)
0 references
10 May 2011
0 references
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)].
0 references
multiplicative linear logic
0 references
proof nets
0 references
0 references