*J. Loeckx and H.-D. Ehrich*

- Published in print:
- 2001
- Published Online:
- November 2020
- ISBN:
- 9780198537816
- eISBN:
- 9780191916663
- Item type:
- chapter

- Publisher:
- Oxford University Press
- DOI:
- 10.1093/oso/9780198537816.003.0004
- Subject:
- Computer Science, Computer Architecture and Logic Design

It is widely accepted that the quality of software can be improved if its design is systematically based on the principles of modularization and formalization. Modularization consists in replacing ...
More

It is widely accepted that the quality of software can be improved if its design is systematically based on the principles of modularization and formalization. Modularization consists in replacing a problem by several “smaller” ones. Formalization consists in using a formal language; it obliges the software designer to be precise and principally allows a mechanical treatment. One may distinguish two modularization techniques for the software design. The first technique consists in a modularization on the basis of the control structures. It is used in classical programming languages where it leads to the notion of a procedure. Moreover, it is used in “imperative” specification languages such as VDM [Woodman and Heal, 1993]; [Andrews and Ince, 1991], Raise [Raise Development Group, 1995], Z [Spivey, 1989] and B [Abrial, 1996]. The second technique consists in a modularization on the basis of the data structures. While modern programming languages such as Ada [Barstow, 1983] and ML [Paulson, 1991] provide facilities for this modularization technique, its systematic use leads to the notion of abstract data types. This technique is particularly interesting in the design of software for non-numerical problems. Compared with the first technique it is more abstract in the sense that algebras are more abstract than algorithms; in fact, control structures are related to algorithms whereas data structures are related to algebras. Formalization leads to the use of logic. The logics used are generally variants of the equational logic or of the first-order predicate logic. The present chapter is concerned with the specification of abstract data types. The theory of abstract data type specification is not trivial, essentially because the objects considered — viz. algebras — have a more complex structure than, say, integers. For more clarity the present chapter treats algebras, logics, specification methods (“specification-in-the-small”), specification languages (“specification-in-the-large”) and parameterization separately. In order to be accessible to a large number of readers it makes use of set-theoretical notions only. This contrasts with a large number of publications on the subject that make use of category theory [Ehrig and Mahr, 1985; Ehrich et al., 1989; Sannella and Tarlecki, 2001].
Less

It is widely accepted that the quality of software can be improved if its design is systematically based on the principles of modularization and formalization. Modularization consists in replacing a problem by several “smaller” ones. Formalization consists in using a formal language; it obliges the software designer to be precise and principally allows a mechanical treatment. One may distinguish two modularization techniques for the software design. The first technique consists in a modularization on the basis of the control structures. It is used in classical programming languages where it leads to the notion of a procedure. Moreover, it is used in “imperative” specification languages such as *VDM* [Woodman and Heal, 1993]; [Andrews and Ince, 1991], *Raise* [Raise Development Group, 1995], *Z* [Spivey, 1989] and *B* [Abrial, 1996]. The second technique consists in a modularization on the basis of the data structures. While modern programming languages such as *Ada* [Barstow, 1983] and *ML* [Paulson, 1991] provide facilities for this modularization technique, its systematic use leads to the notion of abstract data types. This technique is particularly interesting in the design of software for non-numerical problems. Compared with the first technique it is more abstract in the sense that algebras are more abstract than algorithms; in fact, control structures are related to algorithms whereas data structures are related to algebras. *Formalization* leads to the use of logic. The logics used are generally variants of the equational logic or of the first-order predicate logic. The present chapter is concerned with the specification of abstract data types. The theory of abstract data type specification is not trivial, essentially because the objects considered — viz. algebras — have a more complex structure than, say, integers. For more clarity the present chapter treats algebras, logics, specification methods (“specification-in-the-small”), specification languages (“specification-in-the-large”) and parameterization separately. In order to be accessible to a large number of readers it makes use of set-theoretical notions only. This contrasts with a large number of publications on the subject that make use of category theory [Ehrig and Mahr, 1985; Ehrich *et al*., 1989; Sannella and Tarlecki, 2001].

*Andrew M. Pitts*

- Published in print:
- 2001
- Published Online:
- November 2020
- ISBN:
- 9780198537816
- eISBN:
- 9780191916663
- Item type:
- chapter

- Publisher:
- Oxford University Press
- DOI:
- 10.1093/oso/9780198537816.003.0002
- Subject:
- Computer Science, Computer Architecture and Logic Design

This chapter provides an introduction to the interaction between category theory and mathematical logic. Category theory describes properties of mathematical structures via their transformations, ...
More

This chapter provides an introduction to the interaction between category theory and mathematical logic. Category theory describes properties of mathematical structures via their transformations, or ‘morphisms’. On the other hand, mathematical logic provides languages for formalizing properties of structures directly in terms of their constituent parts—elements of sets, functions between sets, relations on sets, and so on. It might seem that the kind of properties that can be described purely in terms of morphisms and their composition would be quite limited. However, beginning with the attempt of Lawvere [1964; 1966; 1969; 1970] to reformulate the foundations of mathematics using the language of category theory, the development of categorical logic over the last three decades has shown that this is far from true. Indeed it turns out that many logical constructs can be characterized in terms of relatively few categorical ones, principal among which is the concept of adjoint functor. In this chapter we will see such categorical characterizations for, amongst other things, the notions of variable, substitution, prepositional connectives and quantifiers, equality, and various type-theoretic constructs. We assume that the reader is familiar with some of the basic notions of category theory, such as functor, natural transformation, (co)limit, and adjunction: see Poigné’s [1992] chapter on Basic Category Theory in Vol. I of this handbook, or any of the several available introductions to category theory slanted towards computer science, such as [Barr and Wells, 1990] and [Pierce, 1991]. There are three recurrent themes in the material we present. Categorical semantics. Many systems of logic can only be modelled in a sufficiently complete way by going beyond the usual set-based structures of classical model theory. Categorical logic introduces the idea of a structure valued in a category C, with the classical model-theoretic notion of structure [Chang and Keisler, 1973] appearing as the special case when C is the category of sets and functions. For a particular logical concept, one seeks to identify what properties (or extra structure) are needed in an arbitrary category to interpret the concept in a way that respects given logical axioms and rules. A well-known example is the interpretation of simply typed lambda calculus in cartesian closed categories.
Less

This chapter provides an introduction to the interaction between category theory and mathematical logic. Category theory describes properties of mathematical structures via their transformations, or ‘morphisms’. On the other hand, mathematical logic provides languages for formalizing properties of structures directly in terms of their constituent parts—elements of sets, functions between sets, relations on sets, and so on. It might seem that the kind of properties that can be described purely in terms of morphisms and their composition would be quite limited. However, beginning with the attempt of Lawvere [1964; 1966; 1969; 1970] to reformulate the foundations of mathematics using the language of category theory, the development of categorical logic over the last three decades has shown that this is far from true. Indeed it turns out that many logical constructs can be characterized in terms of relatively few categorical ones, principal among which is the concept of adjoint functor. In this chapter we will see such categorical characterizations for, amongst other things, the notions of variable, substitution, prepositional connectives and quantifiers, equality, and various type-theoretic constructs. We assume that the reader is familiar with some of the basic notions of category theory, such as functor, natural transformation, (co)limit, and adjunction: see Poigné’s [1992] chapter on Basic Category Theory in Vol. I of this handbook, or any of the several available introductions to category theory slanted towards computer science, such as [Barr and Wells, 1990] and [Pierce, 1991]. There are three recurrent themes in the material we present. Categorical semantics. Many systems of logic can only be modelled in a sufficiently complete way by going beyond the usual set-based structures of classical model theory. Categorical logic introduces the idea of a structure valued in a category C, with the classical model-theoretic notion of structure [Chang and Keisler, 1973] appearing as the special case when C is the category of sets and functions. For a particular logical concept, one seeks to identify what properties (or extra structure) are needed in an arbitrary category to interpret the concept in a way that respects given logical axioms and rules. A well-known example is the interpretation of simply typed lambda calculus in cartesian closed categories.