ens-mellies-cours-1

Publié par

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; ...
Publié le : samedi 24 septembre 2011
Lecture(s) : 37
Nombre de pages : 35
Voir plus Voir moins

Lambda calculs et catégories
Paul-André Melliès
Master Parisien de Recherche en Informatique
Ecole Normale Supérieure
1Plan de la séance
1 – Lambda-calcul
2 – Catégories et 2-catégories
2Première partie
Lambda-calcul
Le calcul des fonctions
3Church 1935: invention syntaxique du-calcul
Le-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 ne
saurait pas donner de sens mathématique — jusqu’au modèle dénotationnel de
Dana 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 i
une variable et A est un type simple, pour tout1 i n.i
On appelle séquent un triplet:
x : A ;:::;x : A ‘ P: B1 1 n n
où x : A ;:::;x : A est un contexte de typage, P est un-terme et B est un type1 1 n n
simple.
5Curry 1958: le-calcul simplement typé
Variable
x:A‘ x:A
;x:A‘ P:B
Abstraction
‘x:P:A) B
‘ P:A) B ‘ Q:A
Application
; ‘ PQ:B
‘ P:B
Affaiblissement
;x:A‘ P:B
;x:A;y:A‘ P:B
Contraction
;z:A‘ P[x;y z]:B
;x:A;y:B; ‘ P:C
Permutation
;y:B;x:A; ‘ P:C
6Propriétés remarquables du fragment simplement typé
Un-terme P est appelé simplement typé lorsqu’il existe un contexte de typage
et un type simple A tels que:
‘ P: A
On démontre que l’ensemble des-termes simplement typés est clos par-réduction:
Subject Reduction: Si ‘ P: A et P! Q, alors ‘ Q: A.

Un -terme P est appelé fortement normalisable lorsque tous les chemins de -
réduction:
P! P ! P ! ! P !

Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.