Profinite lambda-terms and parametricity
Sam van Gool, Paul-André Melliès, Vincent Moreau
TL;DR
The paper introduces profinite λ-terms as Stone-dual objects to the regular higher-order languages of simply typed λ-terms, unifying Stone duality with Reynolds parametricity. It defines a regular-language lattice reg$A$ and constructs ProLambdaTerms$A$ as a limit, yielding a Stone space dual to reg$A$, with a parametricity-based equivalence (Theorem B) to the classical notions. It builds a cartesian closed category ProLam of profinite λ-terms and proves a faithful embedding of ordinary λ-terms, ensuring compositional interpretation and enabling a Church-type correspondence that identifies ProLambdaTerms$\Churchs$ with profinite words $\widehat{\Sigma^*}$ (Theorem C). The results bridge higher-order automata theory with λ-calculus semantics, providing a principled framework for profinite computation and potential extensions to implicit automata and higher-order models. The constructions include a fixpoint operator $\Omega_A$ and a parametric, natural notion of profinite terms compatible with both duality and parametricity, making profinite λ-terms a robust semantic object for higher-order languages.
Abstract
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.