TY - GEN
T1 - Coalgebraic semantics for derivations in logic programming
AU - Komendantskaya, Ekaterina
AU - Power, John
PY - 2011
Y1 - 2011
N2 - Every variable-free logic program induces a P P -coalgebra on the set of atomic formulae in the program. The coalgebra p sends an atomic formula A to the set of the sets of atomic formulae in the antecedent of each clause for which A is the head. In an earlier paper, we identified a variable-free logic program with a P P -coalgebra on Set and showed that, if C(P P ) is the cofree comonad on P P , then given a logic program P qua P P -coalgebra, the corresponding C(P P )-coalgebra structure describes the parallel and-or derivation trees of P. In this paper, we extend that analysis to arbitrary logic programs. That requires a subtle analysis of lax natural transformations between Poset-valued functors on a Lawvere theory, of locally ordered endofunctors and comonads on locally ordered categories, and of coalgebras, oplax maps of coalgebras, and the relationships between such for locally ordered endofunctors and the cofree comonads on them.
AB - Every variable-free logic program induces a P P -coalgebra on the set of atomic formulae in the program. The coalgebra p sends an atomic formula A to the set of the sets of atomic formulae in the antecedent of each clause for which A is the head. In an earlier paper, we identified a variable-free logic program with a P P -coalgebra on Set and showed that, if C(P P ) is the cofree comonad on P P , then given a logic program P qua P P -coalgebra, the corresponding C(P P )-coalgebra structure describes the parallel and-or derivation trees of P. In this paper, we extend that analysis to arbitrary logic programs. That requires a subtle analysis of lax natural transformations between Poset-valued functors on a Lawvere theory, of locally ordered endofunctors and comonads on locally ordered categories, and of coalgebras, oplax maps of coalgebras, and the relationships between such for locally ordered endofunctors and the cofree comonads on them.
KW - Logic programming
KW - SLD-resolution
KW - Coalgebra
KW - Lawvere theories
KW - Lax natural transformations
KW - Oplax maps of coalgebras
UR - http://www.scopus.com/inward/record.url?scp=80053000115&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-22944-2_19
DO - 10.1007/978-3-642-22944-2_19
M3 - Conference contribution
AN - SCOPUS:80053000115
SN - 9783642229435
T3 - Lecture notes in computer science
SP - 268
EP - 282
BT - Algebra and Coalgebra in Computer Science
A2 - Corradini, Andrea
A2 - Klin, Bartek
A2 - Cirstea, Corina
PB - Springer
CY - Berlin
T2 - 4th Conference on Algebra and Coalgebra in Computer Science
Y2 - 30 August 2011 through 2 September 2011
ER -