Unification and logarithmic space

Clement Aubert, Marc Bagnol

Research output: Contribution to journalArticle

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 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
Volume14
Issue number3
DOIs
StatePublished - Jul 31 2018

Fingerprint

Unification
Algebra
Logarithmic
Complexity Classes
Proof Theory
Linear Logic
Models of Computation
Syntactics
Permutation
Geometry
Chemical analysis
Interaction

Keywords

  • 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)

Cite this

Unification and logarithmic space. / Aubert, Clement; Bagnol, Marc.

In: Logical Methods in Computer Science, Vol. 14, No. 3, 6, 31.07.2018.

Research output: Contribution to journalArticle

@article{5cf769f3f48346f580386c2520274607,
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 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.",
keywords = "Geometry of interaction, Geometry of interaction, Implicit complexity, Logarithmic space, Pointer machines, Proof theory, Unification",
author = "Clement Aubert and Marc Bagnol",
year = "2018",
month = "7",
day = "31",
doi = "10.23638/LMCS-14(3:6)2018",
language = "English (US)",
volume = "14",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "Technischen Universitat Braunschweig",
number = "3",

}

TY - JOUR

T1 - Unification and logarithmic space

AU - Aubert, Clement

AU - Bagnol, Marc

PY - 2018/7/31

Y1 - 2018/7/31

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

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

KW - Geometry of interaction

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=85055825667&partnerID=8YFLogxK

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

U2 - 10.23638/LMCS-14(3:6)2018

DO - 10.23638/LMCS-14(3:6)2018

M3 - Article

VL - 14

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 3

M1 - 6

ER -