ens-mellies-cours-3

Description

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 finite 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-orderquantification on type variables.Types are simple types extended with second-order variables:A;B::=j A) Bj8 : AA typing context is a finite 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: ...

Informations

• Publié par: Hamoh
• Nombre de lectures: 8
• Langue: English

Extrait

Lambda calculsetcatégories

Paul-André Melliès

Master Parisien de Recherche en Informatique

Paris, Octobre 2010

1

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

2

Second

Part

order

I

lambda

Polymorphism

calculus

3

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 finite listΓ =(x 1 :A 1 , ...,x n :A n )wherex i is a variable andA i is a simple type, for all1≤i≤n.

Aeutnsqeis a triple:

x 1 :A 1 , ...,x n :A n `P:B wherex 1 :A 1 , ...,x n :A n is a typing context,Pis aλ-term andBis a simple type.

4

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

5

Girard 1972: second-orderλ-calculus

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

Types are simple types extended with second-order variables:

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

A typing contextΓis a finite 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.

6

Girard 1972: second-orderλ-calculus

Second order abstraction

Second order application

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

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

7

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−→ β P 1 −→ β P 2 −→ β →−∙∙∙ β P n −→ β ∙ ∙ ∙

Strong normalisation:Every typedλ-termPis strongly normalizing.

8

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

9

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

9

Curry-Howard for second-order logic

Second order abstraction

Second order application

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

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

10