Eqlog: An Equational Logic Programming Language

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.

Two example Eqlog specifications

To Systems index page
To Joseph Goguen homepage
Maintained by Joseph Goguen
Last modified 23 February 1999