An Embedding of the BSS Model of Computation in Light Affine Lambda-Calculus
Logic in Computer Science
2007-05-23 v1
Abstract
This paper brings together two lines of research: implicit characterization of complexity classes by Linear Logic (LL) on the one hand, and computation over an arbitrary ring in the Blum-Shub-Smale (BSS) model on the other. Given a fixed ring structure K we define an extension of Terui's light affine lambda-calculus typed in LAL (Light Affine Logic) with a basic type for K. We show that this calculus captures the polynomial time function class FP(K): every typed term can be evaluated in polynomial time and conversely every polynomial time BSS machine over K can be simulated in this calculus.
Cite
@article{arxiv.cs/0608040,
title = {An Embedding of the BSS Model of Computation in Light Affine Lambda-Calculus},
author = {Patrick Baillot and Marco Pedicini},
journal= {arXiv preprint arXiv:cs/0608040},
year = {2007}
}
Comments
11 pages. A preliminary version appeared as Research Report IAC CNR Roma, N.57 (11/2004), november 2004