Aspects logiques

Jean Goubault-Larrecq

Abstract: Ceci est la version 6 de la deuxième partie du cours de lambda-calcul, datant du 05 avril 2016 (merci à Nathanaël Courant et à David Baelde). La version 5 datait du 02 juin 2014. La version 4 datait du 28 janvier 2011. (Bizarrement, je n’avais pas remarqué quelques erreurs présentes depuis dix ans dans la démonstration des théorèmes de normalisation forte. Merci à Hang Zhou et à Arthur Milchior.) La version 3 datait du 07 avril 2010. La version 2 datait du 13 mars 2009. La première version datait du 31 août 1999.

Dans la partie précédente, il nous est arrivé de mentionner des équations aux domaines, et de demander que certains objets appartiennent à tel ou tel domaine. En général, on peut avoir envie de considérer un langage comme le λ-calcul, ou plus compliqué, mais avec une discipline de types qui assure que les objets manipulés sont bien dans les bons domaines de valeurs. Une discipline de types statique sera donnée par un certain nombre de règles de typage, qu’un algorithme de vérification de types pourra appliquer pour s’assurer que les programmes donnés sont bien typés.

L’intérêt en programmation d’une telle discipline est qu’aucune erreur de types à l’exécution ne pourra avoir lieu: c’est notamment la philosophie du typage à la ML [HMT90]. En ML, par exemple, si f est une fonction de type int → string, alors dans tout programme bien typé, toute application f u sera nécessairement telle que u s’évalue en un entier, et le corps de la fonction f n’aura jamais à vérifier que son argument est bien un entier, car cette propriété sera garantie par typage. De plus, la valeur de retour de f u sera toujours une chaîne de caractères (le type string).

Le système de typage de ML est particulièrement élégant et pratique. D’autres langages proposent d’autres systèmes de types, souvent moins élégants: Pascal propose un système de types presque aussi strict que celui de ML, tout en étant moins souple; C propose un système de types laxiste (les casts permettent toujours de faire croire n’importe quoi au typeur); et des langages comme Scheme ou Lisp en général utilisent des mécanismes de vérification des types à l’exécution, mais pas à la compilation.

Nous verrons quelques systèmes de types à la ML, et les étudierons sous un angle logique. Il existe en effet une correspondance remarquable entre systèmes de types à la ML et systèmes de preuve, appelée correspondance de Curry-Howard, dans laquelle les notions de programmation suivantes (colonne de gauche) sont identifiées avec les notions de théorie de la démonstration correspondantes (colonne de droite):

Discipline de types∼Logique
Type∼Formule
Programme, terme∼Preuve
Réduction, calcul∼Élimination des coupures

Nous la découvrirons et en développerons les conséquences dans plusieurs disciplines de types dans la suite. Nous commencerons par la plus simple des disciplines de types utiles, celle des types simples, en section 1, et sa relation avec la logique minimale intuitionniste. Le passage à la logique classique propositionnelle sera examiné en section 2, où nous verrons réapparaître les opérateurs de capture de continuation. Nous explorerons des systèmes logiques de plus en plus expressifs par la suite, à commencer par l’arithmétique de Peano-Heyting du premier ordre HA1 en section 3, pour aller vers la logique et l’arithmétique d’ordre deux et le système F de Girard-Reynolds en section 4. Nous présenterons ensuite une application non triviale de ces techniques en section 5, en l’occurrence le théorème de Kreisel-Friedman.

This document was translated from LATEX by HEVEA.