Résumé
Au début de ce cours, nous avons repris et approfondi la notion de relation logique introduite au 6e cours, tout d’abord en les reformulant de manière purement opérationnelle : au lieu de se reposer sur une sémantique dénotationnelle du langage, on peut tout définir en termes d’une relation de réduction entre termes.
L’étape suivante consiste à étendre les relations logiques à des traits délicats de langages comme OCaml : les types récursifs généraux et les références (structures de données mutables) pouvant contenir des fonctions. Dans les deux cas, la définition usuelle des relations logiques n’est plus bien fondée par récurrence sur les types. En 2001, Appel et McAllester contournent brillamment ce problème en utilisant un autre critère de bonne fondation : le nombre d’étapes de réduction que l’on se donne pour observer les propriétés des termes. Cette technique, connue sous le nom de step-indexing (comptage de pas), est étendue aux relations logiques binaires par Ahmed en 2006.
Dans cette présentation des relations logiques, les démonstrations nécessitent une comptabilité minutieuse et lourde des étapes de réduction. Appel et al. (2007) puis Dreyer et al. (2011) développent une présentation plus élégante dans une logique modale ayant la modalité ▷ P (« P est vraie plus tard ») et satisfaisant la loi de Löb (▷ P ⇒ P) ⇒ P. Cette logique n’est autre que la logique interne du topos des arbres que nous avons obtenue au 7e cours par forcing intuitionniste sur les entiers.
