| Summary: | We introduce an operational rewriting-based semantics for strictly positive
nested higher-order (co)inductive types. The semantics takes into account the
"limits" of infinite reduction sequences. This may be seen as a refinement and
generalization of the notion of productivity in term rewriting to a setting
with higher-order functions and with data specified by nested higher-order
inductive and coinductive definitions. Intuitively, we interpret lazy data
structures in a higher-order functional language by potentially infinite terms
corresponding to their complete unfoldings.
We prove an approximation theorem which essentially states that if a term
reduces to an arbitrarily large finite approximation of an infinite object in
the interpretation of a coinductive type, then it infinitarily (i.e. in the
"limit") reduces to an infinite object in the interpretation of this type. We
introduce a sufficient syntactic correctness criterion, in the form of a type
system, for finite terms decorated with type information. Using the
approximation theorem, we show that each well-typed term has a well-defined
interpretation in our semantics.
|
|---|