Logic Programming and Logarithmic Space
Cl\'ement Aubert, Marc Bagnol, Paolo Pistone, Thomas Seiller

TL;DR
This paper introduces an algebraic framework linking logic programming to logspace computation, demonstrating that word acceptance can be decided within logarithmic space and relating observations to two-way multi-head finite automata.
Contribution
It provides a novel algebraic and proof-theoretic characterization of logspace computation using logic programming and geometry of interaction.
Findings
Word acceptance reduces to graph acyclicity within log space.
Observations are as expressive as two-way multi-head finite automata.
The approach offers a new proof-theoretic perspective on logspace complexity.
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 synctactic 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 multi-heads finite automata, a kind of pointer machines that is a standard model of logarithmic space computation.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
