Coalgebraic Semantics for Logic Programming
Ekaterina Komendantskaya, Guy McCusker, John Power · 2010
Logic programming, a class of programming languages based on rst-order logic, provides simple and ecient tools for goal-oriented proof-search. Logic programming supports recursive computations - and some logic programs resemble the inductive or coinductive denitions written in functional programming languages. In this paper, we give a coalgebraic semantics to logic programming. We show that ground logic programs - be it PROLOG language with function symbols or DATALOG language without functions - can be modelled by either PfPf -coalgebras or PfList-coalgebras on Set. We analyse dierent kinds of derivation strategies and derivation trees (proof-trees, SLD-trees, and-or parallel trees) used in logic programming, and show how they can be modelled coalgebraically. We extend these models to non-ground logic programs by incorporating a Lawvere theory into this picture. Namely, a given rst-order signature generates the Lawvere theoryL , and the coalgebraic semantics of non-ground logic programs can be obtained by replacing Set by Lax(L ;Poset) and by allowing countability.