### 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.

Original language | English (US) |
---|---|

Title of host publication | Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings |

Publisher | Springer Verlag |

Pages | 77-92 |

Number of pages | 16 |

ISBN (Print) | 9783319089171 |

DOIs | |

State | Published - Jan 1 2014 |

Event | 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 - Vienna, Austria Duration: Jul 14 2014 → Jul 17 2014 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 8560 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 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 |
---|---|

Country | Austria |

City | Vienna |

Period | 7/14/14 → 7/17/14 |

### Fingerprint

### Keywords

- Geometry of Interaction
- Implicit Complexity
- Logarithmic Space
- Pointer Machines
- Proof Theory
- Unification

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

### Cite this

*Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings*(pp. 77-92). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8560 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-08918-8_6

**Unification and logarithmic space.** / Aubert, Clément; Bagnol, Marc.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings.*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8560 LNCS, Springer Verlag, pp. 77-92, 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, Vienna, Austria, 7/14/14. https://doi.org/10.1007/978-3-319-08918-8_6

}

TY - GEN

T1 - Unification and logarithmic space

AU - Aubert, Clément

AU - Bagnol, Marc

PY - 2014/1/1

Y1 - 2014/1/1

N2 - 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.

AB - 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.

KW - Geometry of Interaction

KW - Implicit Complexity

KW - Logarithmic Space

KW - Pointer Machines

KW - Proof Theory

KW - Unification

UR - http://www.scopus.com/inward/record.url?scp=84958527042&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84958527042&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-08918-8_6

DO - 10.1007/978-3-319-08918-8_6

M3 - Conference contribution

AN - SCOPUS:84958527042

SN - 9783319089171

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 77

EP - 92

BT - Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings

PB - Springer Verlag

ER -