Category-based Semantics for Equational and Constraint Logic Programming
(abstract)
This thesis proposes a general framework for equational logic programming,
called category-based equational logic by placing the general principles
underlying the design of the programming language Eqlog and formulated
by Goguen and Meseguer into an abstract form. This framework generalises
equational deduction to an arbitrary category satisfying certain natural
conditions; completeness is proved under a hypothesis of quantifier projectivity,
using a semantic treatment that regards quantifiers as models rather than
variables, and regards valuations as model morphisms rather than functions.
This is used as a basis for a model theoretic category-based approach to
a paramodulation-based operational semantics for equational logic programming
languages.
Category-based equational logic in conjunction with the theory of institutions
is used to give mathematical foundations for modularisation in equational
logic programming. We study the soundness and completeness problem for
module imports in the context of a category-based semantics for solutions
to equational logic programming queries.
Constraint logic programming is integrated into the equational logic programming
paradigm by showing that constraint logics are a particular case of category-based
equational logic. This follows the methodology of free expansions of models
for built-ins along signature inclusions as sketched by Goguen and Meseguer
in their papers on Eqlog. The mathematical foundations of constraint logic
programming are based on a Herbrand Theorem for constraint logics; this
is obtained as an instance of a more general category-based version of
Herbrand's Theorem.
The results in this thesis apply to equational and constraint logic programming
languages that are based on a variety of equational logical systems including
many and order sorted equational logics, Horn clause logic, equational
logic modulo a theory, constraint logics, and more, as well as any possible
combination between them. More importantly, this thesis gives the possibility
for developing the equational logic (programming) paradigm over non-conventional
structures and thus significantly extending it beyond its tradition.
back to Selected Publications