Retour à la page du séminaire

28/05/99: René David (Chambéry)
Tout lambda terme non resoluble admet une decoration.

résumé

Dans sa thèse, R Kerth a émis une conjecture (l'existence d'une décoration, i.e. une certaine regularité) sur le comportement de la réduction de tête des lambda termes non résolubles. Cette conjecture était utile pour prouver que les $2 ^{\aleph_{0}}$ modèles de graphes (ayant des théories différentes) qu'il construisait étaient sensibles, i.e. égalaient tous les termes non résolubles. Dans cet exposé je donnerai les idées essentielles de la preuve de cette conjecture. Ce genre d'idées peut etre utile pour la solution d'autres problèmes ouverts par exemple sur les termes "faciles". Le background nécessaire se limite à : arbres de Bohm (je rappellerai rapidement ce que c'est) et réduction de tête en lambda calcul.