×

Polynomial time in untyped elementary linear logic. (English) Zbl 1481.03067

Summary: We show how to represent polynomial time computation in an untyped version of proofnets for elementary linear logic. This follows previous work by P. Baillot [Inf. Comput. 241, 3–31 (2015; Zbl 1310.03052)] but which was developed in a typed and affine setting. We describe how these two properties can be adapted.

MSC:

03F52 Proof-theoretic aspects of linear logic and other substructural logics
68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.)

Citations:

Zbl 1310.03052
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Girard, J.-Y., Linear logic, Theor. Comput. Sci., 50, 1-102 (1987) · Zbl 0625.03037
[2] Girard, J.-Y., Light linear logic, Inf. Comput., 143, 2, 175-204 (1998) · Zbl 0912.03025
[3] Lafont, Y., Soft linear logic and polynomial time, Theor. Comput. Sci., 318, 1-2, 163-180 (2004) · Zbl 1079.03057
[4] Danos, V.; Joinet, J.-B., Linear logic and elementary time, Inf. Comput., 183, 1, 123-137 (2003) · Zbl 1019.03039
[5] Gaboardi, M.; Marion, J.-Y.; Ronchi Della Rocca, S., An implicit characterization of PSPACE, ACM Trans. Comput. Log., 13, 2, 18:1-18:36 (2012) · Zbl 1351.68107
[6] Baillot, P., Stratified coherent spaces: a denotational semantics for light linear logic, Theor. Comput. Sci., 318, 1-2, 29-55 (2004) · Zbl 1051.03050
[7] Laurent, O.; Tortora de Falco, L., Obsessional cliques: a semantic characterization of bounded time complexity, (Proceedings of the Twenty-First Annual Symposium on Logic in Computer Science, IEEE (2006), IEEE Computer Society Press: IEEE Computer Society Press Seattle), 179-188
[8] Laurent, O., On the categorical semantics of elementary linear logic, Theory Appl. Categ., 22, 10, 269-301 (2009) · Zbl 1201.18003
[9] Baillot, P., On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy, Inf. Comput., 241, 3-31 (2015) · Zbl 1310.03052
[10] Asperti, A., Light affine logic, (Proceedings of the Thirteenth Annual Symposium on Logic in Computer Science, IEEE (1998), IEEE Computer Society Press: IEEE Computer Society Press Indianapolis), 300-308 · Zbl 0945.03533
[11] Girard, J.-Y.; Lafont, Y.; Taylor, P., Proofs and Types, Cambridge Tracts in Theoretical Computer Science, vol. 7 (1989), Cambridge University Press · Zbl 0671.68002
[12] Asperti, A.; Roversi, L., Intuitionistic light affine logic, ACM Trans. Comput. Log., 3, 1, 1-39 (2002) · Zbl 1365.03040
[13] Mairson, H.; Terui, K., On the computational complexity of cut-elimination in linear logic, (Proceedings of the Eighth Italian Conference on Theoretical Computer Science (ICTCS). Proceedings of the Eighth Italian Conference on Theoretical Computer Science (ICTCS), Lecture Notes in Computer Science, vol. 2841 (2003), Springer), 23-36 · Zbl 1257.03091
[14] Terui, K., Proof nets and Boolean circuits, (Proceedings of the Nineteenth Annual Symposium on Logic in Computer Science, IEEE (2004), IEEE Computer Society Press: IEEE Computer Society Press Turku), 182-191
[15] Dal Lago, U.; Baillot, P., On light logics, uniform encodings and polynomial time, Math. Struct. Comput. Sci., 16, 4, 713-733 (2006) · Zbl 1103.03060
[16] Nguyen, L. T.D., Around finite second-order coherence spaces (2019), Available at
[17] de Carvalho, D.; Pagani, M.; Tortora de Falco, L., A semantic measure of the execution time in linear logic, Theor. Comput. Sci., 412, 20, 1884-1902 (2011) · Zbl 1222.03070
[18] Danos, V.; Regnier, L., The structure of multiplicatives, Arch. Math. Log., 28, 181-203 (1989) · Zbl 0689.03013
[19] Danos, V., La Logique Linéaire appliquée à l’étude de divers processus de normalisation (principalement du λ-calcul) (1990), Université Paris VII, Thèse de doctorat
[20] Dal Lago, U., Context semantics, linear logic and computational complexity, ACM Trans. Comput. Log., 10, 4, 25:1-25:32 (2009) · Zbl 1351.03061
[21] Terese, Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, vol. 55 (2003), Cambridge University Press · Zbl 1030.68053
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.