La notion d'indéfini en lambda calcul

• Main Author: Bertini, Yves
• Language: FRE
• Published: 2005
• Subjects: [MATH] Mathematics; facilité; indéfini; consistance; lambda-calcul infini; arbres de Berarducci; classes confinantes A
• Online Access: http://tel.archives-ouvertes.fr/tel-00415825; http://tel.archives-ouvertes.fr/docs/00/41/58/25/PDF/these_full.pdf

La facilité compte parmi les notions les plus fines de l'indéfini en lambda-calcul. Un terme est dit facile s'il peut être identifié à tout autre terme clos arbitraire sans soulever de contradiction. Introduite en 1975 par Jacopini, elle fait depuis l'objet de recherches qui visent à caractériser la forme des termes faciles. Aujourd'hui, de tous les travaux entrepris il se dégage qu'un tel terme doit posséder une périodicité. Être périodique, c'est être équivalent à un sous-terme propre de l'un de ses réduits. Ici, la périodicité apparaîtra sous les traits de l'auto-similarité. Sont auto-similaires les termes dont l'arbre de Berarducci réapparaît comme sous-arbre propre à lui-même. La facilité de tels termes demeure un mystère. À ce jour, nous n'en connaissons que peu d'exemples. Le terme "Y omega_3" constitue un exemple typique dont la question de la facilité reste ouverte. Dans cette thèse, nous étendrons la connaissance de l'ensemble des termes m identiables à Y Omega_3. Nous montrerons que dans un cas critique où lambda-beta +{Y Omega_3 = m} implique m = delta_3, sous certaines hypothèses, m est lui-même auto-similaire. Ils s'en suit une description possible de toutes les équations dérivées de {Y Omega_3= m} sous la forme de classes confinantes.