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.

翻译：结合Stone对偶与Reynolds参数性的思想，我们以简洁且具有原则性的方式定义了profinite λ-项的概念。研究表明，该概念在每种类型上推广了来自自动机理论的传统profinite词概念。我们首先将profinite λ-项的Stone空间定义为通常λ-项的有限集合基于有限标准模型等价关系的射影极限。本文的主要贡献之一在于确立了一个令人意外的结果：源于Stone对偶的profinite λ-项概念与Reynolds参数性原则实现了完美协调。此外，通过构造profinite λ-项的笛卡尔闭范畴，我们证明了profinite λ-项概念具有组合性，并利用Statman有限完备性定理建立了从λ-项模βη-转换到profinite λ-项的嵌入是忠实的。最后，我们证明有限词的传统Church编码可扩展至profinite词，并导出profinite词空间与相应Church类型的profinite λ-项空间之间的同胚关系。