Abstract
Higher - Order Linear Ramified Recurrence (HOLRR) is a linear (affine) α-calculus -every variable occurs at most once -extended with a recursive scheme on free algebras. Two simple conditions on type derivations enforce both polytime completeness and a strong notion of polytime soundness on typeable terms. Completeness for PTIME holds by embedding Leivant's ramified recurrence on words into HOLRR. Soundness is established at all types -and not only for first order terms. Type connectives are limited to tensor and linear implication. Moreover, typing rules are given as a simple deductive system. © Springer - Verlag 2004.
Cite
CITATION STYLE
Lago, U. D., Martini, S., & Roversi, L. (2004). Higher - Order linear ramified recurrence. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3085, 178–193. https://doi.org/10.1007/978-3-540-24849-1_12
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
