Logic programming and logarithmic space

Clement Aubert, Marc Bagnol, Paolo Pistone, Thomas Seiller

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

4 Citations (Scopus)

Abstract

We present an algebraic view on logic programming, related to proof theory and more specifically linear logic and geometry of interaction. Within this construction, a characterization of logspace (deterministic and non-deterministic) computation is given via a syntactic restriction, using an encoding of words that derives from proof theory.

We show that the acceptance of a word by an observation (the counterpart of a program in the encoding) can be decided within logarithmic space, by reducing this problem to the acyclicity of a graph. We show moreover that observations are as expressive as two-ways multihead finite automata, a kind of pointer machine that is a standard model of logarithmic space computation.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 12th Asian Symposium, APLAS 2014, Proceedings
EditorsJacques Garrigue
PublisherSpringer Verlag
Pages39-57
Number of pages19
ISBN (Electronic)9783319127354
StatePublished - Jan 1 2014
Externally publishedYes
Event12th Asian Symposium on Programming Languages and Systems, APLAS 2014 - Singapore, Singapore
Duration: Nov 17 2014Nov 19 2014

Publication series

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

Other

Other12th Asian Symposium on Programming Languages and Systems, APLAS 2014
CountrySingapore
CitySingapore
Period11/17/1411/19/14

Fingerprint

Proof Theory
Logic programming
Logic Programming
Logarithmic
Encoding
Acyclicity
Linear Logic
Finite Automata
Finite automata
Syntactics
Standard Model
Restriction
Geometry
Graph in graph theory
Interaction
Observation
Syntax

Keywords

  • Automata
  • Geometry of interaction
  • Implicit complexity
  • Logarithmic space
  • Logic programming
  • Pointer machines
  • Proof theory
  • Unification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Aubert, C., Bagnol, M., Pistone, P., & Seiller, T. (2014). Logic programming and logarithmic space. In J. Garrigue (Ed.), Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Proceedings (pp. 39-57). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8858). Springer Verlag.

Logic programming and logarithmic space. / Aubert, Clement; Bagnol, Marc; Pistone, Paolo; Seiller, Thomas.

Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Proceedings. ed. / Jacques Garrigue. Springer Verlag, 2014. p. 39-57 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8858).

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

Aubert, C, Bagnol, M, Pistone, P & Seiller, T 2014, Logic programming and logarithmic space. in J Garrigue (ed.), Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8858, Springer Verlag, pp. 39-57, 12th Asian Symposium on Programming Languages and Systems, APLAS 2014, Singapore, Singapore, 11/17/14.
Aubert C, Bagnol M, Pistone P, Seiller T. Logic programming and logarithmic space. In Garrigue J, editor, Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Proceedings. Springer Verlag. 2014. p. 39-57. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Aubert, Clement ; Bagnol, Marc ; Pistone, Paolo ; Seiller, Thomas. / Logic programming and logarithmic space. Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Proceedings. editor / Jacques Garrigue. Springer Verlag, 2014. pp. 39-57 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{17c095efd34e4f9aab368626045ef8a9,
title = "Logic programming and logarithmic space",
abstract = "We present an algebraic view on logic programming, related to proof theory and more specifically linear logic and geometry of interaction. Within this construction, a characterization of logspace (deterministic and non-deterministic) computation is given via a syntactic restriction, using an encoding of words that derives from proof theory.We show that the acceptance of a word by an observation (the counterpart of a program in the encoding) can be decided within logarithmic space, by reducing this problem to the acyclicity of a graph. We show moreover that observations are as expressive as two-ways multihead finite automata, a kind of pointer machine that is a standard model of logarithmic space computation.",
keywords = "Automata, Geometry of interaction, Implicit complexity, Logarithmic space, Logic programming, Pointer machines, Proof theory, Unification",
author = "Clement Aubert and Marc Bagnol and Paolo Pistone and Thomas Seiller",
year = "2014",
month = "1",
day = "1",
language = "English (US)",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "39--57",
editor = "Jacques Garrigue",
booktitle = "Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Proceedings",

}

TY - GEN

T1 - Logic programming and logarithmic space

AU - Aubert, Clement

AU - Bagnol, Marc

AU - Pistone, Paolo

AU - Seiller, Thomas

PY - 2014/1/1

Y1 - 2014/1/1

N2 - We present an algebraic view on logic programming, related to proof theory and more specifically linear logic and geometry of interaction. Within this construction, a characterization of logspace (deterministic and non-deterministic) computation is given via a syntactic restriction, using an encoding of words that derives from proof theory.We show that the acceptance of a word by an observation (the counterpart of a program in the encoding) can be decided within logarithmic space, by reducing this problem to the acyclicity of a graph. We show moreover that observations are as expressive as two-ways multihead finite automata, a kind of pointer machine that is a standard model of logarithmic space computation.

AB - We present an algebraic view on logic programming, related to proof theory and more specifically linear logic and geometry of interaction. Within this construction, a characterization of logspace (deterministic and non-deterministic) computation is given via a syntactic restriction, using an encoding of words that derives from proof theory.We show that the acceptance of a word by an observation (the counterpart of a program in the encoding) can be decided within logarithmic space, by reducing this problem to the acyclicity of a graph. We show moreover that observations are as expressive as two-ways multihead finite automata, a kind of pointer machine that is a standard model of logarithmic space computation.

KW - Automata

KW - Geometry of interaction

KW - Implicit complexity

KW - Logarithmic space

KW - Logic programming

KW - Pointer machines

KW - Proof theory

KW - Unification

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

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

M3 - Conference contribution

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

SP - 39

EP - 57

BT - Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Proceedings

A2 - Garrigue, Jacques

PB - Springer Verlag

ER -