An Embedding of the BSS Model of Computation in Light Affine Lambda-Calculus

TL;DR

This paper introduces a light affine lambda-calculus extension that models polynomial time computation over arbitrary rings in the BSS model, bridging implicit complexity and algebraic computation.

Contribution

It extends Light Affine Logic to incorporate ring structures, capturing polynomial time BSS computations over any fixed ring K.

Findings

The calculus can evaluate terms in polynomial time.

It can simulate any polynomial time BSS machine over K.

The approach unifies complexity classes with algebraic computation models.

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.