On an interpretation of safe recursion in light affine logic

Journal article

We introduce a subalgebra BC⁻ of Bellantoni and Cook's safe-recursion function algebra BC. Functions of the subalgebra have safe arguments that are non-contractible (i.e non-duplicable). We propose a definition of safe and normal variables in light affine logic (LAL), and show that BC⁻ is the largest subalgebra that is interpretable in LAL, relative to that definition. Though BC⁻ itself is not PF complete, there are extensions of it (by additional schemes for defining functions with safe arguments) that are, and are still interpretable in LAL and so preserve PF closure. We focus on one such which is BC⁻ augmented by a definition-by-cases construct and a restricted form of definition-by-recursion scheme over safe arguments. As a corollary we obtain a new proof of the PF completeness of LAL.

Authors: Murawski, A; Ong, C

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Elsevier
• Journal: Theoretical Computer Science
• Volume: 318
• Issue: 1-2
• Pages: 197–223
• Publication date: 2004-06-01
• Edition: Publisher's version
• DOI: 10.1016/j.tcs.2003.10.017
• ISSN: 0304-3975
• Language: English
• Keywords: computational complexity; light affine logic; polynomial-time computability
• Subjects: Computer science (mathematics)