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 a parametricity theorem for Church encodings of word and ranked tree languages, which states that every parametric family of elements in the finite standard model is the interpretation of a profinite lambda-term. This result shows that our notion of profinite lambda-term conservatively extends the existing notion of profinite word and provides a natural framework for defining and studying profinite trees.

翻译：融合Stone对偶性与Reynolds参数性的思想，我们以简洁且原则化的方式提出了形式化λ-项的概念，并证明该概念在每一类型上推广了自动机理论中传统的形式化词概念。我们从定义形式化λ-项的Stone空间入手，将其作为基于有限标准模型等价关系的通常λ-项有限集合的射影极限。本文主要贡献之一是证明，令人惊讶的是，源自Stone对偶性的形式化λ-项概念与Reynolds参数性原理完美协调。此外，我们通过构造形式化λ-项的笛卡尔闭范畴证明了其组合性，并利用Statman有限完备性定理建立了从模βη-转换的λ-项到形式化λ-项的嵌入的忠实性。最后，我们证明了Church编码词与排序树语言的参数性定理：有限标准模型中每个参数族元素都是形式化λ-项的解释。这一结果表明，我们的形式化λ-项概念保守地扩展了现有的形式化词概念，并为定义和研究形式化树提供了自然框架。