Page sem2009/abstracts/vaux

Points fixes et types de données dans le modèle relationnel finitaire

Lionel Vaux (travail avec C. Tasson)

On s'intéresse à la possibilité d'étendre l'interprétation relationnelle du λ-calcul simplement typé à la famille la plus élémentaire de types inductifs, les types algébriques récursifs, tout en préservant la propriété de finitude établie par Ehrhard: le calcul d'un point dans l'interprétation d'une coupure fait seulement intervenir un ensemble fini de points intermédiaires.

Le problème est donc double:

- trouver une interprétation relationnelle des types algébriques récursifs, de leurs constructeurs et de leurs destructeurs (opérateurs de définition par cas);

- établir que l'opérateur de récursion qui se déduit des destructeurs est finitaire, bien que défini par un point fixe.

On commencera par traiter le cas particulier des entiers de Péano, c'est-à-dire le système T. On verra que, comme dans le modèle cohérent, la sémantique fait nécessairement intervenir une version paresseuse des entiers. On verra également que plusieurs solutions conviennent, non seulement à cause de la non uniformité du modèle, mais surtout parce qu'il n'admet pas de coproduit fort.

On esquissera ensuite une solution dans le cas général, en démontrant l'existence de points fixes pour certains foncteurs dans la catégorie des espaces de finitude relationnels.