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参数性思想，我们以清晰且富有原则性的方式提出了概型λ项的概念，并证明该概念在每一类型上推广了自动机理论中传统的概型词概念。我们首先将概型λ项的Stone空间定义为通常λ项有限集合的射影极限，这些项基于有限标准模型的等价关系进行考量。本文的主要贡献在于建立了一个出人意料的结论：源自Stone对偶性的概型λ项概念与Reynolds参数性原则完美契合。此外，通过构造概型λ项的笛卡尔闭范畴，我们证明了概型λ项概念具有组合性，并利用Statman有限完备性定理确立了从模βη变换的λ项到概型λ项的嵌入是忠实的。最后，我们证明有限词的传统Church编码可扩展至概型词，并在概型词空间与对应Church类型的概型λ项空间之间建立了同胚关系。