ens-mellies-cours-1

Lambda calculs et catégoriesPaul-André MellièsMaster Parisien de Recherche en InformatiqueEcole Normale Supérieure1Plan de la séance1 – Lambda-calcul2 – Catégories et 2-catégories2Première partieLambda-calculLe calcul des fonctions3Church 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).4Curry 1958: le-calcul simplement typéIl est possible de typer certaines expressions du-calcul au moyen de types sim-ples A;B construits par la grammaire:A;B::=j A) B:On appelle contexte de typage une suite finie = (x : A ;:::;x : A ) où x est1 1 n n iune variable et A est un type simple, pour tout1 i n.iOn appelle séquent un triplet:x : A ;:::;x : A ‘ P: B1 1 n noù x : A ;:::;x : A est un contexte de typage, P est un-terme et B est un type1 1 n nsimple.5Curry 1958: le-calcul simplement typéVariablex:A‘ x:A;x:A‘ P:BAbstraction‘x:P:A) B‘ P:A) B ‘ Q:AApplication; ‘ PQ:B‘ P:BAffaiblissement;x:A‘ P:B;x:A;y:A‘ P:BContraction;z:A‘ P[x;y z]:B;x:A;y:B; ‘ P:CPermutation;y:B;x:A; ...