Résumé
Le sixième cours est revenu sur la question de donner une sémantique aux programmes qui ne terminent pas. Cette question a une importance historique (elle a donné un coup d’arrêt à la sémantique dénotationnelle naïve de Strachey), mais aussi pratique (les programmes réactifs comme les serveurs réseau ne doivent pas terminer !)
Une première approche, de nature topologique, voit la sémantique d’un programme comme la limite de ses comportements finis. Nous l’avons illustrée sur le langage IMP, où il suffit d’écrire un interpréteur borné par une profondeur maximale de calcul, puis de faire tendre cette profondeur maximale vers l’infini, pour obtenir une sémantique dénotationnelle d’IMP qui caractérise à la fois terminaison et divergence. Pour des langages manipulant des types de données plus complexes, comme le lambda-calcul, la sémantique dénotationnelle nécessite une structure topologique plus riche, comme les domaines de Scott.
D’autres approches, qui se prêtent mieux à la mécanisation en théorie des types, reposent sur des définitions et des raisonnements coinductifs. Le cours a montré comment définir et mécaniser une sémantique naturelle pour les programmes IMP qui divergent sous forme d’un prédicat coinductif qui structure les suites infinies de réductions. Ensuite, nous avons introduit la monade de partialité, inventée par Capretta en 2005, qui fournit une représentation coinductive et constructive des calculs pouvant terminer ou diverger. Nous avons étudié comment écrire un interpréteur de référence pour IMP dans la monade de partialité. À équivalence observationnelle près, cet interpréteur satisfait les équations de la sémantique opérationnelle d’IMP, fournissant ainsi une alternative constructive aux approches topologiques.
