Inductive and coinductive types are commonly construed as ontological(Church-style) types, denoting canonical data-sets such as natural numbers,lists, and streams. For various purposes, notably the study of programs in thecontext of global semantics, it is preferable to think of types as semanticalproperties (Curry-style). Intrinsic theories were introduced in the late 1990s to provide a purelylogical framework for reasoning about programs and their semantic types. Weextend them here to data given by any combination of inductive and coinductivedefinitions. This approach is of interest because it fits tightly withsyntactic, semantic, and proof theoretic fundamentals of formal logic, withpotential applications in implicit computational complexity as well asextraction of programs from proofs. We prove a Canonicity Theorem, showing thatthe global definition of program typing, via the usual (Tarskian) semantics offirst-order logic, agrees with their operational semantics in the intendedmodel. Finally, we show that every intrinsic theory is interpretable in aconservative extension of first-order arithmetic. This means thatquantification over infinite data objects does not lead, on its own, toproof-theoretic strength beyond that of Peano Arithmetic. Intrinsic theories are perfectly amenable to formulas-as-types Curry-Howardmorphisms, and were used to characterize major computational complexity classesTheir extensions described here have similar potential which has already beenapplied.
展开▼
