Category-based modularisation for equational logic programming (abstract)
Although modularisation is basic to modern computing, it has been little
studied for logic-based programming. We treat modularisation for equational
logic programming using the institution of category-based equational
logic in three different ways: (1) to provide a generic satisfaction
condition for equational logics; (2) to give a category-based semantics
for queries and their solutions; and (3) as an abstract definition of compilation
from one (equational) logic programming language to another.
Regarding (2), we study soundness and completeness for equational logic
programming queries and their solutions. This can be understood as ordinary
soundness and completeness in a suitable ``non-logical'' institution. Soundness
holds for all module imports, but completeness only holds for conservative
module imports. Category-based equational signatures are seen as modules,
and morphisms of such signatures as module imports. Regarding (3), completeness
corresponds to compiler correctness.
The results of this research applies to languages based on a wide class
of equational logic systems, including Horn clause logic, with or without
equality; all variants of order and many sorted equational logic, including
working modulo a set of axioms; constraint logic programming over arbitrary
user-defined data types; and any combination of the above. Most importantly,
due to the abstraction level, this research gives the possibility to have
semantics and to study modularisation for equational logic programming
developed over non-conventional structures.
back to Selected Publications