16/03/2006
Damiano Mazza (IML)
Une étude sémantique des combinateurs d'interaction

Les combinateurs d'interaction, introduits par Yves Lafont, sont un modèle du calcul déterministe distribué, dérivé des réseaux de preuve de MLL. Ils admettent une sémantique algébrique (définie aussi par Lafont) dans le style de la géométrie de l'interaction ; contrairement au cas de MELL, cette sémantique correspond parfaitement à la réduction syntaxique. On verra qu'il est également possible de définir une sémantique dénotationelle pour les combinateurs, dans le style de la sémantique cohérente/relationelle de la logique linéaire. Après avoir analysé plus en détail les propriétés de ces deux sémantiques et les rapports entre les deux, on les utilisera pour construire un calcul logique pour les combinateurs polarisés (déjà considerés aussi par Lafont). Un aspect interessant de cette logique est que la duplication, qui en logique linéaire requiert l'introduction de connecteurs exponentiels, devient accessible (dans certains cas) à travers la quantification au second ordre.