Unification and logarithmic space

Clément Aubert, Marc Bagnol

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

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 languageEnglish (US)
Title of host publicationRewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
PublisherSpringer Verlag
Pages77-92
Number of pages16
ISBN (Print)9783319089171
DOIs
StatePublished - Jan 1 2014
Event25th 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 2014Jul 17 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8560 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other25th 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
CountryAustria
CityVienna
Period7/14/147/17/14

Fingerprint

Unification
Algebra
Logarithmic
Complexity Classes
Geometry
Chemical analysis
Proof Theory
Linear Logic
Models of Computation
Permutation group
Subalgebra
Intuitive
Finite Group
Computing
Interaction

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

Aubert, C., & Bagnol, M. (2014). Unification and logarithmic space. In 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.

Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, 2014. p. 77-92 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8560 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Aubert, C & Bagnol, M 2014, Unification and logarithmic space. in 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
Aubert C, Bagnol M. Unification and logarithmic space. In Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag. 2014. p. 77-92. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-08918-8_6
Aubert, Clément ; Bagnol, Marc. / Unification and logarithmic space. Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, 2014. pp. 77-92 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@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",
year = "2014",
month = "1",
day = "1",
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",

}

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 -