Classes of finite relations as initial abstract data types I

The aim of this paper is to give axiomatizations for sixteen types of finite relations. These classes of relations are obtained as intersections of the following basic classes of relations: total relations, surjective relations, partial functions, and injective relations.

A normal form for all relations is given and each of the sixteen types of relations is (syntactically) characterized by certain additional conditions on this normal form.

For each of the sixteen types T, a set of identities E_T is singled out. The class of relations of type T forms an initial algebra in the category of all algebras which satisfy E_T. In the first part of this paper, for each type T the involved algebras are symmetric strict monoidal categories (in the sense of MacLane), enriched with certain specific constants.