mpri-mellies-cours-1

Description

Modeles` des langages de programmationDomaines, categories,´ jeux` ´Programme de cette premiere seance:Modele` ensembliste du lambda-calcul ;Categor´ ies cartesiennes´ fermees´1´Plan de la seance´1— le-calcul simplement type,` ´2— le modele ensembliste du-calcul simplement type,3— la structure categor´ ique de Ens: categor´ ies et foncteurs,4— la structure categor´ ique de Ens: transformations naturelles et adjonctions,5— la structure categor´ ique de Ens: ccc,6— interpretation´ du-calcul simplement type´ dans une ccc,7— exemples de cccs.2I. Le-calcul simplement type´3´Curry 1958: le-calcul simplement typeIl est possible de typer certaines expressions du-calcul au moyen de types simplesA;Bconstruits par la grammaire:A;B ::=jA)B:On appelle contexte de typage une suite finie = ( x :A ;:::;x :A ) ou` x est unen n1 1 ivariable etA est un type simple, pour tout 1in.iOn appelle sequent´ un triplet:x :A ;:::;x :A ‘P :B1 1 n nou` x : A ;:::;x : A est un contexte de typage, P est un -terme et B est un type1 1 n nsimple.4´Curry 1958: le-calcul simplement typeVariablex :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; ‘P :C5Propriet´ es´ remarquables du fragment simplement type´´ ´Un-termeP est appele simplement type lorsqu’il existe un contexte de typage et untype simpleA tels que:‘P ...

Informations

• Publié par: Vewyur
• Nombre de lectures: 32
• Langue: Français

Extrait

Mod ` elesdeslangagesdeprogrammation

Domaines,cat ´ egories,jeux

Programmedecettepremi ` erese ´ ance:

Mod ` eleensemblistedulambda-calcul;

Cate ´ goriescarte ´ siennesferm ´ ees

1

Plandelase ´ ance

1— leλttnemelpmislucla-c, ´ eyp

2—lemod ` eleensemblisteduλuclamislmelpttneyp ´ e,-c

3—lastructut ´ egoriquedeEns:cat ´ egoriesetfoncteurs, re ca

4— la structure cate´  gorique de Ens: transformations naturelles et adjonctions,

5—lastructurecat ´ egoriquedeEns:ccc,

6— interpre´  tation duλlscual-c,ecccnsune ´ adttpymenemilp

7— exemples de cccs.

2

I.

Le

λ-calcul

simplement

type ´

3

Curry 1958: leλttpye ´ enemplimlscual-c

Il est possible detypercertaines expressions duλ-calcul au moyen de types simplesA, B construits par la grammaire:

A, B::=α|A⇒B.

On appellecontexte de typageΓune suite finieΓ = (x 1 :A 1 , ..., x n :A n )ou`x i est une variable etA i est un type simple, pour tout1≤i≤n.

On appelle ´ sqeuentun triplet:

x 1 :A 1 , ..., x n :A n `P:B o`ux 1 :A 1 , ..., x n :A n est un contexte de typage,Pest unλ-terme etBest un type simple.

4

´ Curry 1958: leλ-calcul simplement type

Variable

Abstraction

Application

Affaiblissement

Contraction

Permutation

x:A`x:A Γ,x:A`P:B Γ`λx.P:A⇒B Γ`P:A⇒BΔ`Q:A Γ,Δ`P Q:B

Γ`P:B Γ,x:A`P:B

Γ,x:A,y:A`P:B Γ,z:A`P[x, y←z] :B

Γ,x:A,y:B,Δ`P:C Γ,y:B,x:A,Δ`P:C

5

Proprie ´ t ´ esremarquablesdufragmentsimplementtyp ´ e Unλ-termeP ´ eatselepp simplement type´ lorsqu’il existe un contexte de typageΓet un type simpleAtels que:

Γ`P:A

Ond ´ emontrequel’ensembledesλctolsesepsrampleessityp ´ ment-mretβontiuced- ´ r:

Subject Reduction:SiΓ`P:AetP−→ β Q, alorsΓ`Q:A.

Unλ-termeP est appele´ fortement normalisablelorsque tous les chemins deβ -re´ duction: P−→ β P 1 −→ β P 2 −→ β ∙−→∙∙ β P n −→ β ∙ ∙ ∙

terminent.

Normalisa

Normalisation forte:SiPsimplementtyp ´ eaolsrtsePest fortement normalisable.

En particulier, leλ-termeΔΔyttn.e ´ pqucleuiboptsa’nseelemispm

6

Curry-Howard (1)

Variable

Abstraction

Application

Affaiblissement

Contraction

Permutation

Logique . minimale intuitioniste

x:A`x:A Γ,x:A`P:B Γ`λx.P:A⇒B Γ`P:A⇒BΔ`Q:A Γ,Δ`P Q:B

Γ`P:B Γ,x:A`P:B

Γ,x:A,y:A`P:B Γ,z:A`P[x, y←z] :B

Γ,x:A,y:B,Δ`P:C Γ,y:B,x:A,Δ`P:C

7

Curry-Howard (1)

Variable

Abstraction

Application

Affaiblissement

Contraction

Permutation

λ-c . alcul simplement type´

x:A`x:A Γ,x:A`P:B Γ`λx.P:A⇒B Γ`P:A⇒BΔ`Q:A Γ,Δ`P Q:B

Γ`P:B Γ,x:A`P:B

Γ,x:A,y:A`P:B Γ,z:A`P[x, y←z] :B

Γ,x:A,y:B,Δ`P:C Γ,y:B,x:A,Δ`P:C

7

Isomorphisme de Curry-Howard (2)

λlpmeslmipye ´ nettcual-c'logique minimale intuitioniste

Uneremarquequipourraitn’avoirqu’uneport ´ eemineure...pourtant:

Logique constructive: monstration L’assistant de de´ CoQevd ´´ p ` elepoRNAIlaI’as ´ eestb sur un langage de type extreˆ  mement  raffine´  , avec des typespolymoprehset de´ pendants. Permet dectiereicfir monstration et d’en une de´ extriaerun programme OCaml.

Logique classique: La logique classique est aussi constructive! a`  condition d’ajouter un ´ teur de controˆ  lecc-llactaynasalduxe ` λmetdrpertreemetL.o’cllutaue ´ preca-opera enm ´ emoirel’environnementduλ(= la pile, la continuation) et d’y revenir plus tard-terme dans l’e´  valuation.

Th ´ eoriedesensembles:(ePPvinietpr)Snietour ` etaxioslesaledsemsirKL-uoeJna the ´ oriedesensembles(saufl’axiomeduchoix)dansunmod ` eledelae ´ basitilie ´ r ´ endrsuof leλle.tr ˆ occonlave-ccual

Encore, et encore, et encore...

8

II.

L’inter

´ etatio pr n

ensembliste

du

λ-calcul

9

Interpre´ tation  ensembliste On associe un ensembleX α moqieuuetypeat ` achaqα. Ensuite,one ´ tendl’interpr ´ etation ` atouslestypes: [α]=X α [A⇒B]=[B] [A] =Hom Ens ([A],[B])

Uns ´ equent

x 1 :A 1 , ..., x n :A n `M:B

estinterpre ´ t ´ ecommeunefonction[A 1 ] × ∙ ∙× ∙[A n ]−→[B]

Proprie ´ t ´ eremarquable:“soundness”pourlesre ` glesβetη

— SiΓ`(λx.M) :A⇒BetΔ`N:A, alors [Γ,Δ`(λx.M)N:B]=[Γ,Δ`M[x:=N] :B]

— SiΓ`M:A⇒Balors [Γ`(λx.M x) :A⇒B]=[Γ`M:A⇒B]

10