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 的尺寸变化原则，用于检查递归定义所导出的策略是否为获胜策略。本文阐述了前两点，最后一步将是后续论文的主题。已实现的原型可用于实验验证所得完全性检查器的效果，为该原则提供了实践依据。