一句话：为严格正嵌套高阶（共）归纳类型提出基于重写的操作语义，用极限刻画无限归约并给出类型正确性准则。
本文研究严格正嵌套高阶（共）归纳类型的操作语义，旨在刻画惰性高阶函数式语言中无限归约序列的“极限”行为。作者提出基于重写的解释：将惰性数据解释为可能无限的完全展开项，从而把项重写中的生产性（productivity）概念推广到含高阶函数与嵌套（共）归纳定义的情形。核心结果是近似定理：若项可归约到共归纳类型解释中无限对象的任意大有限近似，则它在极限意义下归约到该类型解释中的无限对象。论文还引入一个类型系统作为有限项的充分语法正确性准则，并借助近似定理证明每个良类型项在该语义中都有良定义解释。
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.