Clément Aubert ; Marc Bagnol - Unification and Logarithmic Space

lmcs:4552 - Logical Methods in Computer Science, July 31, 2018, Volume 14, Issue 3 - https://doi.org/10.23638/LMCS-14(3:6)2018
Unification and Logarithmic SpaceArticle

Authors: Clément Aubert ORCID; Marc Bagnol

    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.

    https://doi.org/10.23638/LMCS-14(3:6)2018
    Source: arXiv.org:1805.11988
    Volume: Volume 14, Issue 3
    Published on: July 31, 2018
    Accepted on: June 26, 2018
    Submitted on: May 31, 2018
    Keywords: Computer Science - Logic in Computer Science,03D15, 68N17,F.1.3,F.4.1
    Licence: Attribution 4.0 International (CC BY 4.0)
    Funding:
      Source : OpenAIRE Graph
    • Realizability for classical logic, concurrency, references and rewriting; Funder: French National Research Agency (ANR); Code: ANR-11-BS02-0010
    • Logic and Geometry of Interaction; Funder: French National Research Agency (ANR); Code: ANR-10-BLAN-0213
    • Programming reversible recoverable systems; Funder: French National Research Agency (ANR); Code: ANR-11-INSE-0007

    Publications

    Has review
    • 1 zbMATH Open

    2 Documents citing this article

    Share and export

    Consultation statistics

    This page has been seen 1818 times.
    This article's PDF has been downloaded 333 times.