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

Autor:	Atassi, Vincent, Baillot, Patrick, Terui, Kazushige
Rok vydání:	2007
Předmět:	Computer Science - Logic in Computer Science Computer Science - Computational Complexity F.4.1 F.2.2 D.1.1
Zdroj:	Logical Methods in Computer Science, Volume 3, Issue 4 (November 15, 2007) lmcs:1234
Druh dokumentu:	Working Paper
DOI:	10.2168/LMCS-3(4:10)2007
Popis:	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
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/0710.1153 Zobrazit plný text záznamu View this record from Arxiv