Unification and logarithmic space

Clément Aubert, Marc Bagnol

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish (US)
Article number6
JournalLogical Methods in Computer Science
Issue number3
StatePublished - Jul 31 2018


  • Geometry of interaction
  • Geometry of interaction
  • Implicit complexity
  • Logarithmic space
  • Pointer machines
  • Proof theory
  • Unification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Unification and logarithmic space'. Together they form a unique fingerprint.

Cite this