通过大尺寸构造（co）归纳类型
Constructing (Co)inductive Types via Large Sizes
AI总结：
本文提出通过引入大尺寸类型和参数量化符来构造（co）归纳类型，解决了传统方法在一致性和模块性上的限制，并通过不可预测的现实模型证明了理论的一致性。
摘要：
为了确保其类型理论的可判定性和一致性，证明助手只能接受终止的递归函数和产生性的共递归函数。大多数证明助手通过语法条件来强制这一点，这可能过于严格且非模块化。尺寸类型是一种基于类型的替代方法，其中（co）归纳类型被注释附加的尺寸信息。基于尺寸的well-founded归纳可以用来证明终止性和生产性。Agda中已存在尺寸类型的实现，但目前由于添加了最大的尺寸而变得不一致。我们研究了一种替代方法，即在intensional类型理论中扩展一个大类型来表示尺寸，并添加参数量化符。我们显示在该理论中可以构造归纳和共归纳类型，这优于先前的工作，其中只有有限分支的归纳类型才能被构造。该理论的一致性由一个不可预测的现实模型证明，该模型将尺寸类型解释为一个不可数序数。
英文摘要：
To ensure decidability and consistency of its type theory, a proof assistant should only accept terminating recursive functions and productive corecursive functions. Most proof assistants enforce this through syntactic conditions, which can be restrictive and non-modular. Sized types are a type-based alternative where (co)inductive types are annotated with additional size information. Well-founded induction on sizes can then be used to prove termination and productivity. An implementation of sized types exists in Agda, but it is currently inconsistent due to the addition of a largest size. We investigate an alternative approach, where intensional type theory is extended with a large type of sizes and parametric quantifiers over sizes. We show that inductive and coinductive types can be constructed in this theory, which improves on earlier work where this was only possible for the finitely-branching inductive types. The consistency of the theory is justified by an impredicative realisability model, which interprets the type of sizes as an uncountable ordinal.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
