@inproceedings{37d8633874e949e9b1b36c2edea13430,
title = "Unification and logarithmic space",
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 inspired from proof theory and more specifically linear logic and Geometry of Interaction. We show how unification can be used to build a model of computation by means of specific subalgebras associated to finite permutation groups. We then prove that whether an observation (the algebraic counterpart of a program) accepts a word can be decided within logarithmic space. We also show that the construction can naturally encode pointer machines, an intuitive way of understanding logarithmic space computing.",
keywords = "Geometry of Interaction, Implicit Complexity, Logarithmic Space, Pointer Machines, Proof Theory, Unification",
author = "Cl{\'e}ment Aubert and Marc Bagnol",
note = "Funding Information: This work was partly supported by the ANR-10-BLAN-0213 Logoi and the ANR-11-BS02-0010 R{\'e}cr{\'e}.; 25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 ; Conference date: 14-07-2014 Through 17-07-2014",
year = "2014",
doi = "10.1007/978-3-319-08918-8_6",
language = "English (US)",
isbn = "9783319089171",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "77--92",
booktitle = "Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings",
}