Algebraic specifications for parametrized data types with minimal parameter and target algebras

Abstract

We conceive a parametrized data type as a partial functor φ: ALG (∑) --> ALG (Δ), where Δ is a signature extending ∑ and ALG (∑) is the class of minimal ∑-algebras which serve as parameters. We focus attention on one particular method of algebraically specifying parametrized data types: finite specifications with conditional equations using auxiliary sorts and functions provided with initial algebra semantics. We introduce the concept of an effective parametrized data type. A satisfactory adequacy result is then obtained: each effective parametrized data type possesses a finite algebraic specification under initial semantics.