Global semantic typing for inductive and coinductive computing

摘要

Common data-types, such as N, can be identified with term algebras. Thus each type can be construed as a global set; e.g. for N this global set is instantiated in each structure S to the denotations in S of the unary numerals. We can then consider each de