Logic in Computer Science (LICS 1992)

Paper: The category of constraint systems is Cartesian-closed (at LICS 1992)

Authors: Saraswat, V.

Abstract

A general definition of constraint systems utilizing Gentzen-style sequents is given. 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. Approximate maps that are generic in all but finitely many variables are taken as morphisms. It is shown that the resulting structure forms a category (called ConstSys). Furthermore, the structure of Scott information systems lifts smoothly to the first-order setting. In particular, it is shown 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

BibTeX

  @InProceedings{Saraswat-Thecategoryofconstr,
    author = 	 {Saraswat, V.},
    title = 	 {The category of constraint systems is Cartesian-closed},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1992},
    year =	 1992,
    editor =	 {Andre Scedrov},
    month =	 {June}, 
    pages =      {341--345},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }