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 |
DOIs | |
State | Published - 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/Territory | Singapore |
City | Singapore |
Period | 11/17/14 → 11/19/14 |
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)