Hostname: page-component-78c5997874-fbnjt Total loading time: 0 Render date: 2024-11-05T03:44:45.506Z Has data issue: false hasContentIssue false
  • English
  • Français

A formalism for the specification of essentially-algebraic structures in 2-categories†

Published online by Cambridge University Press:  04 March 2009

A. J. Power  and
Charles Wells
A. J. Power
Affiliation:
Laboratory for Computer Science, The King's Buildings, University of Edinburgh, Mayfield Road, Edinburgh EH9 3JZ, UK
Charles Wells
Affiliation:
Department of Mathematics, Case Western Reserve University, University Circle, Cleveland, OH 44106, USA
Get access Rights & Permissions [Opens in a new window]

Abstract

A type of higher-order two-dimensional sketch is defined which has models in suitable 2-categories. It has as special cases the ordinary sketches of Ehresmann and certain previously defined generalizations of one-dimensional sketches. These sketches allow the specification of constructions in 2-categories such as weighted limits, as well as higher-order constructions such as exponential objects and subobject classifiers, that cannot be sketched by limits and colimits. These sketches are designed to be the basis of a category-based methodology for the description of functional programming languages, complete with rewrite rules giving the operational semantics, that is independent of the usual specification methods based on formal languages and symbolic logic. A definition of ‘path grammar’, generalizing the usual notion of grammar, is given as a step towards this goal.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 2 , Issue 1 , March 1992 , pp. 1 - 28
Copyright
Copyright © Cambridge University Press 1992

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

Barr, M. and Wells, C. (1985) Toposes, Triples and Theories. Grundlehren der math. Wissenschaften 278, Springer-Verlag. (Errata are available from either author.)CrossRefGoogle Scholar
Barr, M. and Wells, C. (1990a) Category Theory for Computing Science. Prentice-Hall.Google Scholar
Barr, M. and Wells, C. (1990b) On the limitations of sketches. To appear.Google Scholar
Bastiani, A. and Ehresmann, C. (1968) Categories of sketched structures. Cahiers de Topologie et Géométrie Différentielle 10 104–213.Google Scholar
Beierle, C. and Voss, A. (1985) Implementation specifications. In: Kreowski, H.-H., ed., Recent Trends in Data Type Specifications. Springer-Verlag pp. 39–52.CrossRefGoogle Scholar
Bird, G. J., Kelly, G. M., Power, A. J. and Street, R. H. (1989) Flexible limits for 2-categories. J. Pure Appl. Algebra 61 1–27.CrossRefGoogle Scholar
Blackwell, R., Kelly, G. M. and Power, A. J. (1989) Two-dimensional monad theory. J. Pure Appl. Algebra 59 1–41.CrossRefGoogle Scholar
Freyd, P. (1973) Aspects of topoi. Bull. Austral. Math. Soc. 7, 1–72 and Corrections. Ibid., 8 (1973), 467–480.CrossRefGoogle Scholar
Goguen, J. and Burstall, R. (1980) CAT, a system for the structured elaboration of correct programs from structured specifications. Technical Report CSL–118, SRI Computer Science Lab.Google Scholar
Goguen, J. and Meseguer, J. (1982) Universal realization, persistent interconnection and implementation of abstract modules. In: Nielsen, M. and Schmidt, E. M., eds, Proc. 9th Int. Conf. Automata, Languages and Programming. Springer Lecture Notes in Computer Science 140, pp. 265–281.Google Scholar
Guitart, R. and Lair, C. (1982) Limites et co-limites pour representer les formules. Diagrammes 7.Google Scholar
Hopcroft, J. E. and Ullman, J. D. (1979) Introduction to Automata Theory, Languages and Computation. Addison-Wesley.Google Scholar
Hyland, J. M. E. and Pitts, A. M. (1989) The theory of constructions: Categorical semantics and topos-theoretic models. In: Gray, J. W. and Scedrov, A., eds, Categories in Computer Science and Logic. Contemp. Math. 92, pp. 137–201.Google Scholar
Johnson, M. (1989) The combinatorics of n-categorical pasting. J. Pure Appl. Algebra 62 211–225.CrossRefGoogle Scholar
Kelly, G. M. (1982) Basic Concepts of Enriched Category Theory. Cambridge University Press, Cambridge.Google Scholar
Kelly, G. M. (1989) Elementary observations on 2-categorical limits. Bull. Australian Math. Soc. 39 301–317.CrossRefGoogle Scholar
Kelly, G. M. and Power, A. J. (1988) Algebraic structure in the enriched context. Preprint, Pure Mathematics Department, University of Sydney, N.S.W. 2006, AustraliaGoogle Scholar
Kelly, G. M. and Street, R. (1973) Review of the elements of 2-categories. In: Proc. Sydney Category Theory Seminar 1972/1973. Springer Lecture Notes in Mathematics 420.Google Scholar
Lair, C. (1987) Trames et semantiques catégoriques des systèmes de trames. Diagrammes 18.Google Scholar
Lawvere, F. W. (1989) Qualitative distinctions between some toposes of generalized graphs. In: Gray, J. W. and Scedrov, A., eds, Categories in Computer Science and Logic. Contemp. Math. 92 pp. 261–300.Google Scholar
Mac Lane, S. (1971) Categories for the Working Mathematician. Springer Graduate Texts in Mathematics 5.CrossRefGoogle Scholar
Power, A. J. (1990a) A 2-categorical pasting theorem. J. Algebra 129 439–445.CrossRefGoogle Scholar
Power, A. J. (1990b) An abstract formulation for rewrite systems. In: Category Theory and Computer Science, Pitt, D. H., Rydeheard, D. E., Dybjer, P., Pitts, A. M. and Poigné, A. eds Springer Lecture Notes in Computer Science 389.Google Scholar
Sannella, D. and Tarlecki, A. (1988) Building specifications in an arbitrary institution. Information and Control 76 165–210.Google Scholar
Seely, R. (1987) Modelling computations: a 2-categorical framework. In: Proc. Conf on Logic in Computer Science. IEEE.Google Scholar
Street, R. (1976) Limits indexed by category-valued 2-functors. J. Pure Appl. Algebra 8 149–181.CrossRefGoogle Scholar
Street, R. (1987) The algebra of oriented simplexes. J. Pure Appl. Algebra 49 283–335.CrossRefGoogle Scholar
Wells, C. (1990) A generalization of the concept of sketch. Theoret. Comput. Sci. 70 159–178.CrossRefGoogle Scholar
Wells, C. and Barr, M. (1988) The formal description of data types using sketches. In: Mathematical Foundations of Programming Language Semantics. Main, M., Melton, A., Mislove, M. and Schmidt, D., eds Springer Lecture Notes in Computer Science 298.CrossRefGoogle Scholar