PARAMETERS AND PARAMETRIZATION IN SPECIFICATION, USING DISTRIBUTIVE CATEGORIES

Article type: Research Article

Authors: Jacobs, Bart

Affiliations: CWI, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands

Abstract: A specification, as we shall use it here, consists of a signature together with a collection of (non-conditional) equations; these equations involve terms in the ‘distributive type theory’ which is built on top of the signature. This type theory has finite product (x, 1) and coproduct (+, 0) types. Particular simple examples of such specifications are Hagino specifications, which are used to describe inductively defined types. Models of specifications are described in arbitrary distributive categories. In a more categorical approach, one describes models as structure preserving functors. It enables us to define in general what are (a) models of parametrized spefications (in terms of Kan extensions) and (b) models with parameters (in terms of so-called ‘simple slice’ categories). It is shown that in the special case of Hagino specifications, these general definitions specialize to ones in terms of algebras or coalgebras for associated ‘strong’ polynomial functors. Models with parameters of Hagino specifications were described earlier by Cockett and Spencer.

DOI: 10.3233/FI-1995-2431

Journal: Fundamenta Informaticae, vol. 24, no. 3, pp. 209-250, 1995