Profinite lambda-terms and parametricity
Date(s) : 01/06/2023 iCal
11h00 - 12h30
This talk will present a definition of profinite lambda-terms of
any simple type. Profinite structures naturally appear in automata theory
as a way to speak about limiting behavior of finite words, giving rise to
the notion of profinite word. At the same time, the Church encoding
establishes a one-to-one correspondence between finite words and
simply-typed lambda-terms, taken modulo beta and eta, of a type given by
their finite alphabet. Our definition extends this correspondence between
profinite lambda-terms of a Church type and profinite words over the
associated alphabet. We start by introducing the set 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. We show that this resulting notion of profinite lambda-term, coming
from Stone duality, lives in perfect harmony with the principles of
Reynolds parametricity. Indeed, we prove a parametricity theorem for Church
encodings of words, stating that every parametric family of elements in the
finite standard model is the interpretation of a profinite lambda-term.
Emplacement
I2M Luminy - Ancienne BU, Salle Séminaire2 (RdC)
Catégories
