Verification of Ptime Reducibility for system F Terms: Type Inference in Dual Light Affine Logic

Vincent Atassi; Patrick Baillot; Kazushige Terui

doi:10.2168/LMCS-3(4:10)2007

Vincent Atassi ; Patrick Baillot ; Kazushige Terui - Verification of Ptime Reducibility for system F Terms: Type Inference in<br> Dual Light Affine Logic

lmcs:1234 - Logical Methods in Computer Science, November 15, 2007, Volume 3, Issue 4 - https://doi.org/10.2168/LMCS-3(4:10)2007

Verification of Ptime Reducibility for system F Terms: Type Inference in<br> Dual Light Affine LogicArticle

Authors: Vincent Atassi ; Patrick Baillot ; Kazushige Terui

In a previous work Baillot and Terui introduced Dual light affine logic (DLAL) as a variant of Light linear logic suitable for guaranteeing complexity properties on lambda calculus terms: all typable terms can be evaluated in polynomial time by beta reduction and all Ptime functions can be represented.
In the present work we address the problem of typing lambda-terms in second-order DLAL. For that we give a procedure which, starting with a term typed in system F, determines whether it is typable in DLAL and outputs a concrete typing if there exists any. We show that our procedure can be run in time polynomial in the size of the original Church typed system F term.

Comment: 32 pages, 8 figures

https://doi.org/10.2168/LMCS-3(4:10)2007

Source: arXiv.org:0710.1153

Volume: Volume 3, Issue 4

Published on: November 15, 2007

Imported on: January 6, 2007

Keywords: Computer Science - Logic in Computer Science, Computer Science - Computational Complexity, F.4.1, F.2.2, D.1.1

Licence: arXiv.org - Assumed non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

12 Documents citing this article

U. Dal Lago, 2022, Implicit computation complexity in higher-order programming languages, Mathematical Structures in Computer Science, 32, 6, pp. 760-776, 10.1017/s0960129521000505, https://doi.org/10.1017/s0960129521000505.

Emmanuel Hainry;Damiano Mazza;Romain Péchoux, 2020, Polynomial Time over the Reals with Parsimony, Lecture notes in computer science, pp. 50-65, 10.1007/978-3-030-59025-3_4.

Matthieu Perrinel, 2018, Paths-based criteria and application to linear logic subsystems characterizing polynomial time, Information and Computation, 261, pp. 23-54, 10.1016/j.ic.2018.05.004.

D. Canavese;E. Cesena;R. Ouchary;M. Pedicini;L. Roversi, 2015, Light combinators for finite fields arithmetic, Institutional Research Information System University of Turin (University of Turin), 111, pp. 365-394, 10.1016/j.scico.2015.04.001, http://www.sciencedirect.com/science/article/pii/S0167642315000672.

Olha Shkaravska;Marko van Eekelen;Alejandro Tamalet, 2014, Collected Size Semantics for Strict Functional Programs over General Polymorphic Lists, MPG.PuRe (Max Planck Society), pp. 143-159, 10.1007/978-3-319-12466-7_9, http://hdl.handle.net/11858/00-001M-0000-0024-60C9-5.

Loris D'Antoni;Marco Gaboardi;Emilio Jesús Gallego Arias;Andreas Haeberlen;et al., 2013, Sensitivity analysis using type-based constraints, pp. 43-50, 10.1145/2505351.2505353.

Emanuele Cesena;Marco Pedicini;Luca Roversi, 2012, Typing a Core Binary-Field Arithmetic in a Light Logic, Lecture notes in computer science, pp. 19-35, 10.1007/978-3-642-32495-6_2.

Olha Shkaravska;Marko van Eekelen;Alejandro Tamalet, 2011, Collected Size Semantics for Functional Programs over Lists, Lecture notes in computer science, pp. 118-137, 10.1007/978-3-642-24452-0_7.

Patrick Baillot;Paolo Coppola;Ugo Dal Lago, 2010, Light logics and optimal reduction: Completeness and complexity, Information and Computation, 209, 2, pp. 118-142, 10.1016/j.ic.2010.10.002.

Ugo Dal Lago;Ulrich Schöpp, 2010, Type Inference for Sublinear Space Functional Programming, Lecture notes in computer science, pp. 376-391, 10.1007/978-3-642-17164-2_26.

Olha Shkaravska;Marko van Eekelen;Ron van Kesteren, 2009, Polynomial Size Analysis of First-Order Shapely Functions, Logical Methods in Computer Science, Volume 5, Issue 2, 10.2168/lmcs-5(2:10)2009, https://doi.org/10.2168/lmcs-5(2:10)2009.

Patrick Baillot;Kazushige Terui, 2008, Light types for polynomial time computation in lambda calculus, Information and Computation, 207, 1, pp. 41-62, 10.1016/j.ic.2008.08.005.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3135 times.

This article's PDF has been downloaded 575 times.