Coalgebraic Semantics for Parallel Derivation Strategies in Logic Programming

John Power

(Bath University)

Logic Programming consists of a class of programming languages based on first-order logic, with simple and efficient tools for goal-oriented proof search. We start by making the simplifying assumption that all logic programs are ground, which is essentially as traditional denotational semantics for logic programming does. We give coalgebraic semantics for ground logic programs in terms of P_fP_f-coalgebras and in terms of ListList-coalgebras on Set. The cofree comonads on these endofunctors yield the and-or parallel trees generated by a logic program, with trees being understood either combinatorially or as embedded in the plane respectively. We then extend the analysis to arbitrary logic programs, with substitution on terms modelled by a Lawvere theory and substitution on formulae modelled by a lax natural transformation between Poset-valued functors.
Thursday 28th October 2010, 14:00
Board Room
Department of Computer Science