Algebraic Theories, Data Types, and Control Constructs

Article type: Research Article

Authors: Wagner, Eric G.

Affiliations: Exploratory Computer Science, IBM T.J. Watson Research Center, Yorktown Heights, N.Y. 10598, U.S.A.

Abstract: The aim of this paper is to model recursive types, equational types, and elementary programming control constructs (such as conditionals and while-do) in one, comparatively simple, algebraic framework, that can be used for theoretical studies and as a basis for data type and program specification. To this end we introduce a new kind of algebraic theory, the RV-theory. We give simple examples of the use of such theories for data type specification. We provide a mathematical semantics for these specifications that extends the initial algebra semantics for equational specification to include recursive types.

DOI: 10.3233/FI-1986-9305

Journal: Fundamenta Informaticae, vol. 9, no. 3, pp. 343-370, 1986