This paper shows how to use Lee, Jones and Ben Amram's size-change principle to check correctness of arbitrary recursive definitions in an ML / Haskell like programming language with inductive and coinductive types. Naively using the size-change principle to check productivity and termination is straightforward but unsound when inductive and coinductive types are nested. We can however adapt the size-change principle to check ``totality'', which corresponds exactly to correctness with respect to the corresponding (co)inductive type.

翻译：本文展示了如何利用Lee、Jones和Ben Amram提出的大小变化原理，在支持归纳与余归纳类型的类ML/Haskell编程语言中验证任意递归定义的正确性。直接运用该原理检查生产性与终止性在嵌套归纳/余归纳类型时虽简便但不可靠。我们通过调整大小变化原理以验证“完全性”，该性质精确对应了递归定义相对于相应（余）归纳类型的正确性。