Name
Title | ||
|---|---|---|
Erratum to: "A new framework for declarative programming": [Theoret. Comput. Sci. 300 (2003) 91-160] |
Abstract | ||
|---|---|---|
We propose a new framework for the syntax and semantics of Weak Hereditarily Harrop logic programming with constraints, based on resolution over tau-categories: finite product categories with canonical structure. Constraint information is directly built-in to the notion of signature via categorical syntax. Many-sorted equational constraints are a special case of the formalism which combines features of uniform logic programming languages (modules and hypothetical implication) with those of constraint logic programming. Using the canonical structure supplied by tau-categories, we define a diagrammatic generalization of formulas, goals, programs and resolution proofs up to equality (rather than just up to isomorphism). We extend the Kowalski-van Emden fixed point interpretation, a cornerstone of declarative semantics, to an operational, non-ground, categorical semantics based on indexing over sorts and programs. We also introduce a topos-theoretic declarative semantics and show soundness and completeness of resolution proofs and of a sequent calculus over the categorical signature. We conclude with a discussion of semantic perspectives on uniform logic programming. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1016/j.tcs.2003.09.011 | Theoretical Computer Science |
DocType | Volume | Issue |
Journal | 311 | 1 |
ISSN | Citations | PageRank |
0304-3975 | 0 | 0.34 |
References | Authors | |
0 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Stacy E. Finkelstein | 1 | 16 | 1.78 |
| Peter J. Freyd | 2 | 91 | 16.54 |
| James Lipton | 3 | 9 | 0.89 |