论文标题
雪松中的单调递归类型和递归数据表示
Monotone recursive types and recursive data representations in Cedille
论文作者
论文摘要
在塔克西（Tarksi）的fixpoint定理的指导下，我们展示了如何在雪松中以恒定的时间滚动和展开操作来得出单调递归类型，这是一种不可思议的，建设性的，逻辑上一致的纯pure pure pure-typed lambda colculus。该推导发生在由类型包含物引起的雪松类型的预订中，这是理论本身中可以表达的概念。作为应用程序，我们使用单调递归类型来普遍得出Lambda微积分，Parigot和Scott编码中数据的两个递归表示。对于这两种编码，我们都证明并检查其破坏者，迭代剂和雪松中原始递归的计算和扩展特性。特别是对于我们的Scott编码，我们将其转化为Cedille A cedille A构造，这是因为Lepigre和Raffalli为Scott Naturals配备了原始递归，然后扩展该结构以得出一般的感应原理。这使我们能够为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.
