The category of constraint systems is Cartesian-closed

Vijay A. Saraswat

Abstract

The development of constraint programming has brought to the forefront the notion of constraint systems as certain first-order systems of partial information. Connections between such systems and domain theory have seemed apparent for some time, but have not yet been explored in depth. The need for such a study becomes unavoidable, however, when one considers the development of higher-order constraint programming languages. To give semantics to such languages, it becomes necessary to find mathematical structures in which recursive ``domain equations'' involving constraint systems can be solved.

In this paper we give a general definition of constraint systems utilizing Gentzen-style sequents. Constraint systems can be regarded as enriching the propositional Scott information systems with minimal first-order structure: the notion of variables, existential quantification and substitution. Reflecting the computational reality that an agent ``has access'' to only finitely many free variables, we take as morphisms approximable maps that are generic in all but finitely many variables. We show that the resulting structure forms a category (called ConstSys). Furthermore, the structure of Scott information systems lifts smoothly to the first-order setting - we show that the category is Cartesian-closed, and other usual functors over Scott information systems (lifting, sums, Smyth power-domain) are also definable and recursive domain equations involving these functors can be solved. This makes it possible to use this category to define the semantics of higher-order, concurrent constraint programming languages.

Postscript file