Eqlog is a programming and specification language which combines constraint logic programming with equational programming. Its default operational semantics is order sorted narrowing, but particular cases can be computed by efficient built in algorithms over suitable data structures, with their functions and relations, including equality, disequality, and the usual orderings for numbers and lists. Initiality in Horn clause logic with equality provides a rigorous semantics for functional programming, logic programming, and their combination, as well as for the full power of constraint programming, allowing queries with logical variables over combinations of user-defined and built in data types.

Eqlog has a powerful type system that allows subtypes, based on order
sorted algebra. The method of *retracts*, a mathematically rigorous
form of runtime type checking and error handling, gives Eqlog a syntactic
flexibility comparable to that of untyped languages, while preserving all the
advantages of strong typing. The order sortedness of Eqlog not only greatly
increases expressivity and the efficiency of unification, but it also provides
a rigorous framework for multiple data representations and automatic coercions
among them. Uniform methods of conversion among multiple data representations
are essential for reusing already programmed constraint solvers, because they
will represent data in various ways. Order sorted algebra provides a precise
and systematic equational theory for this, based on initial semantics.

Eqlog also supports loose specifications through its so-called
*theories*, and provides *views* for asserting the satisfaction
of theories by programs as well as relationships of refinement among
specifications and/or programs. This relates directly to Eqlog's powerful form
of modularity, with generic (i.e., parameterised) modules and views, based on
the same principles as the OBJ language. Theories
specify both syntactic structure and semantic properties of modules and module
interfaces. Modules can be parameterised, where actual parameters are
modules. Modules can also import other modules, thus supporting multiple
inheritance at the module level. For parameter instantiation, a view binds the
formal entities in an interface theory to actual entities in a module.
*Module expressions* allow complex combinations of already defined
modules, including sums, instantiations and transformations; moreover,
evaluating a module expression actually builds a software system from the
given components. Thus parameterised programming in Eqlog gives significant
support for large programs through module composition. The semantics of
module importation is given by conservative extensions of theories in Horn
clause logic with equality. The stronger notion of persistent extension
underlies generic modules.

To Systems index page

To Joseph Goguen homepage

Maintained by Joseph Goguen

Last modified 23 February 1999