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 lambda-项的概念。我们证明，这一概念在每个类型上推广了来自自动机理论的传统profinite词概念。首先，我们将profinite lambda-项的Stone空间定义为通常lambda-项有限集合的投射极限，这些项在基于有限标准模型的等价关系下进行考量。本文的主要贡献之一是证明，出乎意料地，源自Stone对偶性的profinite lambda-项概念与Reynolds参数性原则完美协调。此外，我们通过构造profinite lambda-项的笛卡尔封闭范畴展示了其组合性，并利用Statman有限完备性定理证明了从lambda-项模beta-eta变换到profinite lambda-项的嵌入是忠实的。最后，我们证明，传统上将有限词编码为lambda-项的Church编码可以扩展至profinite词，并导致profinite词空间与对应Church类型的profinite lambda-项空间之间存在同胚关系。