Unification and Logarithmic Space

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