ens-mellies-cours-4

Lambda calculs et catégoriesPaul-André MellièsMaster Parisien de Recherche en InformatiqueParis, Novembre 20091Plan de la séance1 – Lambda-calcul simplement typé2 – Catégories cartésiennes fermées2Première partieLambda-calcul simplement typéUn calcul fonctionnel au cœur de la logique3Interprétation de Brouwer-Heyting-KolmogorovUne démonstration de la formuleA ^ Best une paire(’; )constituée d’une démonstration’de la formule A et d’une démonstration de la formule B.4Interprétation de Brouwer-Heyting-KolmogorovUne démonstration de la formuleA ) Best un fonction qui transforme toute démonstration’de la formule A en une démonstration (’)de la formule B.5Church 1935: invention syntaxique du-calculLe-calcul est le calcul syntaxique ou formel des fonctions.Les expressions du-calcul sont appelés des-termes.Le-calcul est un calcul plutôt bizarre où tout-terme P est à la fois: une fonction qui s’applique à tous les-termes, y compris lui-même, un argument de n’importe quel-terme, y compris lui-même.On a longtemps cru que le -calcul n’était qu’un jeu d’écriture, auquel on nesaurait pas donner de sens mathématique — jusqu’au modèle dénotationnel deDana Scott (1976).6Church 1935: une syntaxe pure du calcul fonctionnelSupposons donné un ensemble infini de variables.Il y a trois formes de-termes:Variable: Toute variable x définit un-terme,Abstraction: Toute expression x:P définit un -terme lorsque x est une variableet P est ...