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提出的尺寸变化原理，用于验证递归定义所导出的策略是否必胜。本文重点阐述前两个要点，最后一步将留待后续论文探讨。目前已实现原型系统，可用于实验验证该完全性检查器的效果，从而为这一原理提供实践依据。