ens-mellies-cours-4

Description

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 ...

Informations

• Publié par: Zodaj
• Nombre de lectures: 36
• Langue: Catalan

Extrait

Lambda calculsetcatégories

Paul-André Melliès

Master Parisien de Recherche en Informatique

Paris, Novembre 2009

1

1

2

–

–

Lambda-calcul

Catégories

Plan

de

simplement typé

cartésiennes

fermées

la

séance

2

Première partie

Lambda-calcul

Un calcul fonctionnel

simplement

typé

au cœur de la logique

3

Interprétation de Brouwer-Heyting-Kolmogorov

Une démonstration de la formule

est une paire

constituée d’une démonstration

A∧B

(ϕ, ψ)

de la formuleAet d’une démonstration

de la formuleB.

ϕ

ψ

4

Interprétation de Brouwer-Heyting-Kolmogorov

Une démonstration de la formule

est un fonction

qui transforme toute démonstration

A⇒

de la formuleAen une démonstration

de la formuleB.

ψ

ϕ

ψ(ϕ)

B

5

Church 1935: invention syntaxique duλ-calcul

Leλluaccl-est le calculquetaxisynouformeldes fonctions.

Les expressions duλ-calcul sont appelés desλ-termes.

Leλ-calcul est un calculplutôt bizarreoù toutλ-termePest à la fois:

∗uneonnctifoqui s’applique à tous lesλs,meer-ty compris lui-même,

∗uneumgtrnade 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).

6

Church 1935: une syntaxe pure du calcul fonctionnel

Supposons donné un ensemble infini de variables.

Il y a trois formes deλtermes:-

Variable:Toute variablexdéfinit unλ-mret,e

Abstraction:Toute expressionλx.Pdéfinit unλ-terme lorsquexest une variable etPest unλ la variable-terme. Attention:xrapptiaaoun’apparait pasdans le λ-termeP.

λx.Pest une notation pour la fonctionx7→P.

Application:Toute expressionPQdéfinit unλ-terme lorsquePetQsont desλ- termes.

PQest une notation pour l’application de la fonctionPà l’argumentQ.

Convention sur les variables liées:on identifie deuxλ-termes commeλx.xetλy.y.

7

Church 1935: définition de laβr-cudénoit

Pourcalculerunλ-terme, on utilise laβleèg-r:

(λx.P)Q−→ β P[x←Q]

qui transforme la fonction(λx.P)appliquée à l’argumentQen leλ-termeP[x←Q] obtenu enalaçtnerpmdansPtoutes les instances de la variablexpar leλ-terme Q.

On utilise aussi laηgle:-rè

P−→ η λx.(Px)

Remarque:on fait attention d’éviter ce qu’on appellela capture de variable... par exemple laβr-décuitno:

(λx.λy.x)y−→ β λz.y nécessite de renommer(λx.λy.x)en(λx.λz.x)pour éviter tout malentendu.

8

Church 1935: quelques exemples deλ-termes

L’identitéI=λx.xtransforme toutλ-termePen lui-même: IP−→ β P. La première projectionK=λx.λy.xefface le secondλ-terme parmiPetQ: KPQ−→ β (λy.P)Q−→ β P. Le duplicateurΔ =λx.xxréplique toutλ-termeP: ΔP−→ β PP. Le duplicateurΔappliqué à lui-mêmecloue:b ΔΔ−→ β ΔΔ−→ β ΔΔ−→ β ∙ ∙ ∙

9

Church& confluenceRosser 1936: et standardisation

En mêlant un effaceur et un duplicateur, on obtient unλ-termeKz(ΔΔ)quiclebou si on commence par calculer l’argument:

Kz(ΔΔ)−→ β Kz(ΔΔ)−→ β Kz(ΔΔ)−→ β ∙ ∙ ∙ et quienitermsi on commence par calculer la fonction:

Kz(ΔΔ)−→ β (λy.z)(ΔΔ)−→ β z Théorème de Church-Rosser Toutλ-termePpeut être transformé en unatlutsér(=λ-terme sansβ-réduction) au plus.

Théorème de standardisation La stratégie d’évaluationdndarsatqui calcule toujours la fonction avant l’argument, atteint le résultat duλ-termePsi ce résultat existe.

10

Kleene 1936: leλ-calcul est universel

Entiers de Church p0q=(λf.λx.x)p1q=(λf.λx.f x)p2q=(λf.λx.f(f(x))) Plus généralement:

pnq=λf.λx.f(...f(x))))).

Une fonction (totale)f:N k −→Nest diteλsiaslbe-édnfilorsqu’il existe unλ-terme Ptel que:

∀(n 1 , ...,n k )∈N k ,Ppn 1 q∙ ∙ ∙pn k q− ∗ → β pf(n 1 , ...,n k )q.

Théorème:Toute fonction récursive estλ-définissable (et réciproquement.)

Remarque:on utilise le combinateur de point fixeY=λf.(λx.f(xx))(λx.f(xx))pour coder la récursion.

11