Nested Sketches

Horst Reichel

From the introduction:

Since the fundamental work of Lawvere in 1963 it is common to understand a theory as category with additional structure, to understand a model of the theory as a functor preserving the additional structure, and to represent homomorphisms by natural transformations. The resulting model category becomes a suitable subcategory of a functor category. Many different classes of mathematical structures have been described and investigated in this way. The aim of this paper is, to find a functorial model theory for those classes of algebras that appear naturally as semantics of algebraic specifications of parameterized data types, using initial respectively more general free functor semantics, and to extend the functorial model theory to specifications that use as well inductively defined data types as coinductively defined patterns of behavior and their systematic combinations.

The final result is a categorical model theory of discrete mathematical structures whose basic operations may have arbitrarily structured domains and codomains. Such kind of structures have been first systematically investigated by T. Hagino in his PhD thesis. The basic idea to achieve this generalized categorical model theory is the use of combined left and right Kan extensions in order to constrain iteratively functor categories.

The resulting categorical model theory generalizes algebraic and essentially algebraic theories, since algebras are structures whose basic operations have a structured domain, being a product or finite limit, and the codomain is one of the basic types (usually called sorts in algebra). The approach also generalizes coalgebras, for which dually the codomains of the basic operations are structured and the domain is one of the basic types.


This report is available in the following formats:

Previous | Index | Next