A Natural Data Type with a Finite Equational Final Semantics Specification But No Effective Equational Initial Semantics Specification

摘要

Initial and final algebra semantics are two ways of assigning a unique meaning to an axiomatic specification (sigma, E) of a data type. It is easy to find natural data types with effective specifications with respect to initial algebra semantics, but without effective specifications with respect to final algebra semantics. A natural source of data types for which the opposite is true are those programming systems with undecidable program equivalence problems. The situation when the denotational semantics of a system are the primitive recursive functions is worked out in detail.