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