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编程语言中验证任意递归定义的正确性。若直接应用尺寸变化原理检验生产性与终止性，当归纳类型与余归纳类型嵌套时虽操作简便但缺乏可靠性。然而，我们可以通过调整尺寸变化原理来检验“完全性”——该性质恰好对应着相对于相应（余）归纳类型的正确性。