This paper introduces an ML / Haskell like programming language with nested inductive and coinductive algebraic datatypes called \chariot. Functions are defined by arbitrary recursive definitions and can thus lead to non-termination and other ``bad'' behavior. \chariot comes with a totality checker that tags possibly ill-behaved definitions. Such a totality checker is mandatory in the context of proof assistants based on type theory like Agda. Proving correctness of this checker is far from trivial and relies on - an interpretation of types as parity games, - an interpretation of correct values as winning strategies for those games, - the Lee, Jones and Ben Amram's size-change principle, used to check that the strategies induced by recursive definitions are winning. This paper develops the first two points, the last step being the subject of an upcoming paper. A prototype has been implemented and can be used to experiment with the resulting totality checker, giving a practical argument in favor of this principle.

翻译：本文介绍了一种名为\chariot的类ML/Haskell编程语言，该语言支持嵌套的归纳与余归纳代数数据类型。函数可通过任意递归定义实现，因此可能导致非终止及其他"不良"行为。\chariot配备了可标记潜在异常定义的全性检查器。在基于类型论（如Agda）的证明辅助工具中，此类全性检查器是必需的。证明该检查器的正确性极具挑战性，其理论基础包括：将类型解释为奇偶博弈、将正确值解释为这些博弈的必胜策略，以及运用Lee、Jones和Ben Amram提出的尺寸变化原理来验证递归定义所导出的策略是否必胜。本文重点阐述前两个理论要点，最后一步将留待后续论文探讨。目前已实现原型系统，可用于验证所得全性检查器的实际效果，为该原理的有效性提供实践依据。