Equational specifications for computable data types: six hidden functions suffice and other sufficiency bounds : (preprint)
Jan Aldert Bergstra, John Vivian Tucker · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1980
The ADJ Group's algebraic theory of data types identifies, semantically, each data type with a many-sorted algebra.In this technical paper, we prove that if A is a computable, infinite but finitely generated, manysorted algebra with n sorts then A possesses a finite equational specification which involves at most n hidden constants and at most 3n+3 hidden functions.Thus in case A is single-sorted we have the bound of 6 mentioned in our title.Simple bounds on the number of equations used in the specifications are also included.