Flavien Breuvart (Université Paris Diderot), Une bien étrange caractérisation de l'adéquation complète dans les domaines de Scott

Programme

Résumé

Il existe une vaste littérature traitant de résultats d'adéquation complète (c'est à dire la correspondance entre la congruence dénotationnelle et la congruence observationnelle) pour une multitude de couple modèle-langage. Mais l'adéquation complète en tant qu'objet a rarement été étudiée, à l'exception notable du langage PCF, pour lequel Milner a caractérisé la classe des modèles complétement adéquats, qui sont ceux dont les éléments compacts sont définissables. Même dans le cas du lambda-calcul, s'il existe des conditions nécessaires (extensionnalité) ou suffisantes (stratification), aucune caractérisation n'a été donnée. Je vais donc expliquer comment, dans une classe de modèle suffisamment restreinte, la caractérisation de l'adéquation complète pour le lambda-calcul se trouve être surprenamment complexe.

Pièces jointes