Hostname: page-component-586b7cd67f-vdxz6 Total loading time: 0 Render date: 2024-11-28T19:47:16.915Z Has data issue: false hasContentIssue false
  • English
  • Français

Sketches and computation – I: basic definitions and static evaluation

Published online by Cambridge University Press:  04 March 2009

Dominique Duval  and
Jean-Claude Reynaud
Dominique Duval
Affiliation:
Laboratoire d'Arithmétique, Calcul formel et Optimisation 123 Avenue Albert Thomas, 87060 LIMOGES cedex (France)
Jean-Claude Reynaud
Affiliation:
LGI-IMAG-CNRS, B.P.53, 38041 GRENOBLE cedex 9 (France)
Get access Rights & Permissions [Opens in a new window]

Abstract

We define a categorical framework, based on the notion of sketch, for specification and evaluation in the senses of algebraic specifications and algebraic programming. This framework goes far beyond our initial motivation, which was to specify computation with algebraic numbers. We begin by redefining sketches in order to deal explicitly with programs. Expressions and terms are carefully defined and studied, then quasi-projective sketches are introduced. We describe static evaluation in these sketches: we propose a rigorous basis for evalution in the corresponding structures. These structures admit an initial model, but are not necessarily equational. In Part II (Duval and Reynaud 1994), we study a more general process, called dynamic evaluation, for structures that may have no initial model.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 4 , Issue 2 , June 1994 , pp. 185 - 238
Copyright
Copyright © Cambridge University Press 1994

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Ageron, P. (1991) Structure des logiques et logique des structures, Thése, Université de Paris 7.Google Scholar
Barr, M. and Wells, C. (1985) Toposes, triples and theories, Springer.Google Scholar
Barr, M. and Wells, C. (1988) The formal description of data types using sketches. Springer-Verlag Lecture Notes in Computer Science 298 1–42.Google Scholar
Bastiani, A., and Ehresmann, C. (1972) Categories of sketched structures. Cahiers de topologie et géométrie différentielle 13 (2).Google Scholar
Cockett, J. R. B.Introduction to Distributive Categories. Preprints, University of Calgary.Google Scholar
Coppey, L. and Lair, C. (1984) Leçons de théorie des esquisses (I). Diagrammes 12, Paris.Google Scholar
Coppey, L. and Lair, C. (1988) Leçons de théorie des esquisses (II). Diagrammes 19, Paris.Google Scholar
Davenport, J., Siret, Y. and Tournier, E. (1987) Calcul formel, Masson.Google Scholar
Dershowitz, N. and Jouannaud, J.-P. (1989) Rewrite systems. Handbook of Theoretical Computer Science B ch.15, North-Holland.Google Scholar
Della Dora, J., Dicrescenzo, C. and Duval, D. (1985) About a new method for computing in algebraic number fields. Proceedings Eurocal’85. Springer-Verlag Lecture Notes in Computer Science 204 289–290.Google Scholar
Dicrescenzo, C. and Duval, D. (1989) Algebraic extensions and algebraic closure in Scratchpad. Symbolic and algebraic computation (ISSAC’88). Springer-Verlag Lecture Notes in Computer Science 358 440–446.Google Scholar
Duval, D. (1989) Simultaneous computations in fields of arbitrary characteristic. In: Kaltofen, E. and Watt, S. M. (eds.) Computers and Mathematics, Springer 321–326.Google Scholar
Duval, D. and Gonzalez-Vega, L. (1993) Dynamic evaluation and real closure. Proceedings of IMACS’93.Google Scholar
Duval, D. and Reynaud, J.-C. (1989, 1990) Esquisses et Calcul. In: Dehornoy, P. (ed.) Annales Université de Caen VII 15–83,Google Scholar
Duval, D. and Reynaud, J.-C. (1991) Sketches and computation. Rapport de recherche RR871-I-IMAG-123-LIFIA, Institut National Polytechnique de Grenoble.Google Scholar
Duval, D. and Reynaud, J.-C. (1994) Sketches and computation - Part II: Dynamic Evaluation and Applications. MSCS 4 239–271.Google Scholar
Duval, D. and Sénéchaud, P. (to appear) Sketches and parametrization. Theoretical Computer Science.Google Scholar
Ehresmann, C. (1968) Esquisses et types de structures algébriques. Bulletin de l’lnstitut Polytechnique, Iasi 14.Google Scholar
Ehrig, H. and Mahr, B. (1985) Fundamentals of algebraic specification, Springer.Google Scholar
Goguen, J. A. and Burstall, R. M. (1984) Introducing institutions. Proc. Logics of Programming Workshop. Springer-Verlag Lecture Notes in Computer Science 164 221–256.Google Scholar
Gomez-Diaz, T. (1993) Examples of using dynamic constructible closure. Proceedings of IMACS’93.Google Scholar
Guitart, R. and Lair, C. (1980) Calcul syntaxique des modéles et calcul des formules internes. Diagrammes 4, Paris.Google Scholar
Guitart, R. and Lair, C. (1982) Limites et colimites pour représenter les formules. Diagrammes 7, Paris.Google Scholar
Lair, C. (1983) Diagrammes localement libres, extensions de corps et théorie de Galois. Diagrammes 10, Paris.Google Scholar
Lair, C. (1986) Cours de troisiéme cycle, Multigraphié, Paris.Google Scholar
Lawvere, F. W. (1968) Some algebraic problems in the context of functional semantics of algebraic theories. Springer-Verlag Lecture Notes in Mathematics 61.Google Scholar
Lellahi, S. K. (1989) Categorical abstract data type. Diagrammes 21, Paris.Google Scholar
Mac Lane, S. (1971) Categories for the working mathematician, Springer.Google Scholar
Makkai, M. and Paré, R. (1987) Accessible categories: The foundations of categorical model theory. Report from the department of mathematics and statistics, McGill University.Google Scholar
Perm wall, O. (1991) A Bibliography on Sketches from the Computer Science Point of View. Bulletin of the European Association for Theoretical Computer Science 45 238–255.Google Scholar