Profinite lambda-项与参数化
Profinite lambda-terms and parametricity
AI总结：
结合Stone对偶与Reynolds参数化思想提出profinite lambda-项概念，证明其推广了传统profinite字，并展示其与参数化原则的完美契合及组合性。
摘要：
结合来自Stone对偶和Reynolds参数化的思想，我们以一种清晰且具有原则性的方式阐述了profinite lambda-项的概念，并证明该概念在所有类型上都推广了源自自动机理论的传统profinite字概念。我们首先将profinite lambda-项的Stone空间定义为通常lambda-项有限集的射影极限，这些有限集被视为基于有限标准模型的等价概念模运算。本文的一个主要贡献是确立了一个令人惊讶的结果：源自Stone对偶的profinite lambda-项概念与Reynolds参数化原则完美契合。此外，我们通过构造profinite lambda-项的笛卡尔闭范畴，证明了profinite lambda-项的概念是组合的，并利用Statman有限完备性定理确立了从beta-eta转换模lambda-项到profinite lambda-项的嵌入是忠实的。最后，我们证明了将有限字的Church编码扩展到lambda-项的传统方法可以推广至profinite字，从而在profinite字空间与相应Church类型的profinite lambda-项空间之间建立了同胚。
英文摘要：
Combining ideas coming from Stone duality and Reynolds parametricity, we formulate in a clean and principled way a notion of profinite lambda-term which, we show, generalizes at every type the traditional notion of profinite word coming from automata theory. We start by defining the Stone space of profinite lambda-terms as a projective limit of finite sets of usual lambda-terms, considered modulo a notion of equivalence based on the finite standard model. One main contribution of the paper is to establish that, somewhat surprisingly, the resulting notion of profinite lambda-term coming from Stone duality lives in perfect harmony with the principles of Reynolds parametricity. In addition, we show that the notion of profinite lambda-term is compositional by constructing a cartesian closed category of profinite lambda-terms, and we establish that the embedding from lambda-terms modulo beta-eta-conversion to profinite lambda-terms is faithful using Statman's finite completeness theorem. Finally, we prove that the traditional Church encoding of finite words into lambda-terms can be extended to profinite words, and leads to a homeomorphism between the space of profinite words and the space of profinite lambda-terms of the corresponding Church type.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
