Cedille 中的单调递归类型与递归数据表示
Monotone recursive types and recursive data representations in Cedille
AI总结：
本文在 Cedille 中基于 Tarski 不动点定理推导单调递归类型，并应用于 Parigot 和 Scott 编码，证明归纳性质并给出高效唯一的迭代与原始递归方案。
摘要：
在序理论中，受 Tarski 不动点定理的指导，我们展示了如何在 Cedille（一种非直谓的、构造性的且逻辑一致的纯类型化 lambda 演算）中推导出具有常数时间 roll 和 unroll 操作的单调递归类型。这一推导发生在由类型包含（一种可在理论本身内表达的概念）诱导的 Cedille 类型的预序中。作为应用，我们使用单调递归类型来泛型地推导 lambda 演算中数据的两种递归表示：Parigot 编码和 Scott 编码。对于这两种编码，我们都证明了归纳法，并考察了它们在 Cedille 中的消解器、迭代器和原始递归器的计算及外延性质。特别是对于我们的 Scott 编码，我们将 Lepigre 和 Raffalli 的一个构造翻译到 Cedille 中，该构造为 Scott 自然数配备了原始递归，然后扩展此构造以推导出泛型归纳原理。这使我们能够为 Scott 编码数据给出高效且可证明唯一（在函数外延性下）的迭代和原始递归方案解。
英文摘要：
Guided by Tarksi's fixpoint theorem in order theory, we show how to derive monotone recursive types with constant-time roll and unroll operations within Cedille, an impredicative, constructive, and logically consistent pure typed lambda calculus. This derivation takes place within the preorder on Cedille types induced by type inclusions, a notion which is expressible within the theory itself. As applications, we use monotone recursive types to generically derive two recursive representations of data in lambda calculus, the Parigot and Scott encoding. For both encodings, we prove induction and examine the computational and extensional properties of their destructor, iterator, and primitive recursor in Cedille. For our Scott encoding in particular, we translate into Cedille a construction due to Lepigre and Raffalli that equips Scott naturals with primitive recursion, then extend this construction to derive a generic induction principle. This allows us to give efficient and provably unique (up to function extensionality) solutions for the iteration and primitive recursion schemes for Scott-encoded data.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
