一句话：为混合归纳/共归纳类型全性检查器建立 parity game 语义，将正确值解释为获胜策略。
论文研究基于类型论的证明助手（如 Agda）中，混合归纳与共归纳代数数据类型的全性判定。作者提出类 ML/Haskell 的语言 Chariot，支持嵌套的归纳与共归纳数据类型，并设计全性检查器以标记可能不良行为的递归定义。证明该检查器正确性非平凡，其基础包括：将类型解释为 parity game，将正确值解释为这些游戏的获胜策略，再借助 Lee、Jones 与 Ben Amram 的 size-change principle 检验递归定义诱导的策略是否获胜。本文发展前两个语义解释步骤，最后一步留待后续；并实现原型以实验该全性检查器，为这一原理提供实践支持。
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.