Initial and Final Algebra Semantics for Data Type Specifications: Two Characterization Theorems

摘要

It is proved that those data types which may be defined by conditional equation specifications and final algebra semantics are exactly the cosemicomputable data types those data types which are effectively computable, but whose inequality relations are recursively enumerable. Also the computable data types are characterized as those data types which may be specified by conditional equation specifications using both initial algebra semantics and final algebra semantics. Numerical bounds for the number of auxiliary functions and conditional equations required are included in both theorems.