Published in

Logical Methods in Computer Science ; Volume 14, p. Issue 3 ; 1860-5974, 2018

DOI: 10.23638/lmcs-14(3:6)2018

Springer Verlag, Lecture Notes in Computer Science, p. 77-92

DOI: 10.1007/978-3-319-08918-8_6

Links

Tools

Export citation

Search in Google Scholar

Unification and Logarithmic Space

Journal article published in 2014 by Clément Aubert ORCID, Marc Bagnol
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Question mark in circle
Preprint: policy unknown
Upload
Question mark in circle
Postprint: policy unknown
Upload
Question mark in circle
Published version: policy unknown
Upload

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.