Unification and Logarithmic Space

TL;DR

This paper introduces an algebraic framework based on unification to characterize Logspace and Nlogspace complexity classes, connecting proof theory, linear logic, and geometry of interaction to model logarithmic space computations.

Contribution

It provides a novel algebraic model of computation that captures Logspace and Nlogspace classes using unification algebra and syntactic permutations.

Findings

Decides word acceptance within logarithmic space

Builds a model of computation in unification algebra

Corresponds to pointer machines for Logspace

Abstract

We present an algebraic characterization of the complexity classes Logspace and Nlogspace, using an algebra with a composition law based on unification. This new bridge between unification and complexity classes is rooted in proof theory and more specifically linear logic and geometry of interaction. We show how to build a model of computation in the unification algebra and then, by means of a syntactic representation of finite permutations in the algebra, we prove that whether an observation (the algebraic counterpart of a program) accepts a word can be decided within logarithmic space. Finally, we show that the construction naturally corresponds to pointer machines, a convenient way of understanding logarithmic space computation.