### 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 language | English (US) |
---|---|

Title of host publication | Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Proceedings |

Editors | Jacques Garrigue |

Publisher | Springer Verlag |

Pages | 39-57 |

Number of pages | 19 |

ISBN (Electronic) | 9783319127354 |

State | Published - Jan 1 2014 |

Externally published | Yes |

Event | 12th Asian Symposium on Programming Languages and Systems, APLAS 2014 - Singapore, Singapore Duration: Nov 17 2014 → Nov 19 2014 |

### Publication series

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

Volume | 8858 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 12th Asian Symposium on Programming Languages and Systems, APLAS 2014 |
---|---|

Country | Singapore |

City | Singapore |

Period | 11/17/14 → 11/19/14 |

### Fingerprint

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

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

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

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

}

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

AN - SCOPUS:84910000431

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 -