CATEGORY-BASED MODULARISATION FOR EQUATIONAL LOGIC PROGRAMMING

Although modularisation is basic to modern computing, it has been litt le studied for logic-based programming. We treat modularisation for eq uational logic programming using the institution of category-based equ ational logic in three different ways: (1) to provide a generic satisf action condition for equational logics; (2) to give a category-based s emantics for queries and their solutions; and (3) as an abstract defin ition of compilation from one (equational) logic programming language to another. Regarding (2), we study soundness and completeness for equ ational logic programming queries and their solutions. This can be und erstood as ordinary soundness and completeness in a suitable ''non-log ical'' institution. Soundness holds for all module imports, but comple teness only holds for conservative module imports. Category-based equa tional signatures are seen as modules, and morphisms of such signature s as module imports. Regarding (3), completeness corresponds to compil er correctness. The results of this research applies to languages base d on a wide class of equational logic systems, including Horn clause l ogic, with or without equality; all variants of order and many sorted equational logic, including working module a set of axioms; constraint logic programming over arbitrary user-defined data types; and any com bination of the above. Most importantly, due to the abstraction level, this research gives the possibility to have semantics and to study mo dularisation for equational logic programming developed over non-conve ntional structures.