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