ens-mellies-cours-1

Informations

• Publié par: Erzo
• Nombre de lectures: 29
• Langue: Français

Extrait

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 !