Data systems and their intrinsic theories

Given a multi-sorted free algebra A(C) generated by a set C of constructors, the intrinsic theory for C has as axioms just the closure conditions of the types of A(C), and their dual (C-induction). This gets interesting when we consider equational programs as added axioms. For instance, the programs over N that are provably-typed computes exactly the provably-recursive functions of PA.

We generalize matters from free algebras to *data-systems*, a setting where inductive and coinductive definitions can be combined at will, and untyped equational programs can be assigned semantical (= Curry-style) types. The intrinsic theory of a data system has closure conditions for inductive types, with Induction as their dual, and decomposition conditions for coinductive types, with a suitable notion of Coinduction as their dual.

We prove a Data-canonicity Theorem, stating that global program-correctness over all structures, in a Tarskian-semantics sense, is equivalent to program-correctness in the canonical structure, in the denotational-semantics sense. We further show that the intrinsic theory for any non-trivial data-system is mutually interpretable with PA, regardless of the mix of inductive and coinductive types. We establish a strong normalization theorem for all intrinsic theories, and consider its applications. Finally, we discuss the relation between an intrinsic theories based on classical vs constructive logic.