ens-mellies-cours-3

pages

English

Documents

Lire

Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres

pages

English

Documents

Lire

Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres

Publié par

Hamoh

Langue

English

Lambda calculs et catégoriesPaul-André MellièsMaster Parisien de Recherche en InformatiqueParis, Octobre 20101Plan de la séance1 – Lambda-calcul typé du second ordre2 – Une sémantique opérationnelle3 – Une topologie4 – Les variétés comme type sémantique5 – Théorème fondamental6 – Application: théorème de normalisation2Part ISecond order lambda calculusPolymorphism3Curry 1958: the simply typed-calculusIt is possible to type the-terms by simple typesA;B constructed by the grammar:A;B::=j A) B:A typing context is a ﬁnite list = (x : A ;:::;x : A ) where x is a variable and A1 1 n n i iis a simple type, for all1 i n.A sequent is a triple:x : A ;:::;x : A ‘ P: Bn n1 1where x : A ;:::;x : A is a typing context, P is a-term and B is a simple type.1 1 n n4Curry 1958: the simply-typed-calculusVariablex: A‘ x: A;x: A‘ P: BAbstraction‘x:P: A) B‘ P: A) B ‘ Q: AApplication; ‘ PQ: B‘ P: BWeakening;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: C5Girard 1972: second-order-calculusThe idea is to extend the usual simply typed lambda-calculus with second-orderquantiﬁcation on type variables.Types are simple types extended with second-order variables:A;B::=j A) Bj8 : AA typing context is a ﬁnite list constructed by the grammar= nil j ;x: A j ;where:o nil is the empty listo x is a term variable and A is a type,o is a type variable.6Girard 1972: ...

Voir

Publié par

Hamoh

Langue

English

Lambda calculsetcatégories

Paul-André Melliès

Master Parisien de Recherche en Informatique

Paris, Octobre 2010

Plan de la séance

1 – Lambda-calcul typé du second ordre

2 – Une sémantique opérationnelle

3 – Une topologie

4 – Les variétés comme type sémantique

5 – Théorème fondamental

6 – Application: théorème de normalisation

Second

Part

order

lambda

Polymorphism

calculus

Curry 1958: the simply typedλ-calculus It is possible totypetheλ-terms by simple typesA,Bconstructed by the grammar: A,B::=α|A⇒B.

Atyping contextΓis a ﬁnite listΓ =(x1:A1, ...,xn:An)wherexiis a variable andAi is a simple type, for all1≤i≤n.

Aeutnsqeis a triple:

x1:A1, ...,xn:An`P:B wherex1:A1, ...,xn:Anis a typing context,Pis aλ-term andBis a simple type.

Curry 1958: the simply-typedλ-calculus

Variable

Abstraction

Application

Weakening

Contraction

Permutation

x:A`x:A

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

Γ`P:A⇒BΔ`Q:A Γ,Δ`PQ: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

Girard 1972: second-orderλ-calculus

The idea is to extend the usual simply typed lambda-calculus with second-order quantiﬁcation on type variables.

Types are simple types extended with second-order variables:

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

A typing contextΓis a ﬁnite list constructed by the grammar

where:

onilis the empty list

Γ =nil|Γ,x:A|Γ, α

oxis a term variable andAis a type,

oαis a type variable.

Girard 1972: second-orderλ-calculus

Second order abstraction

Second order application

Γ,α`P:A Γ`P:∀α.A

Γ`P:∀α.A Γ`P:A[α:=B]

Properties of second-order polymorphism

Aλ-termPistpydewhen there exists a typing contextΓand a second-order type Asuch that:

Γ`P:A

One establishes that the set of typedλ-terms is closed underβn:ioctdu-ér

Subject Reduction:IfΓ`P:AandP−→βQ, thenΓ`Q:A.

Aλ-termPisstrongly normalizingwhen all the rewriting paths based onβon:ucti-red

terminate.

P−→βP1−→βP2−→β→−∙∙∙βPn−→β∙ ∙ ∙

Strong normalisation:Every typedλ-termPis strongly normalizing.

Curry-Howard (1)

Variable

Abstraction

Application

Weakening

Contraction

Permutation

Minim.al intuitionistic logic

x:A`x:A Γ,x:A`P:B Γ`λx.P:A⇒B Γ`P:A⇒BΔ`Q:A Γ,Δ`PQ: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

Curry-Howard (1)

Variable

Abstraction

Application

Weakening

Contraction

Permutation

sim.pedy-tylpλsculu-cal

x:A`x:A Γ,x:A`P:B Γ`λx.P:A⇒B Γ`P:A⇒BΔ`Q:A Γ,Δ`PQ: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

Curry-Howard for second-order logic

Second order abstraction

Second order application

Γ, α`P:A Γ`P:∀α.A

Γ`P:∀α.A Γ`P:A[α:=B]

Voir