Rachunek lambda, lato 2019-20

(1)

Rachunek lambda, lato 2019-20

Wykład 9

24 kwietnia 2020

1

W poprzednim odcinku: typy iloczynowe:

Types:

I The constantωis a type.

I Type variablesp, q, . . . are types.

I Ifσandτare types then(σ → τ )is a type.

I Ifσandτare types then(σ ∩ τ )is a type.

2

Subtyping (BCD):

Define≤as the leastquasi-ordersatisfying the axioms:

σ ∩ τ ≤ σ σ ∩ τ ≤ τ σ ≤ σ ∩ σ σ ≤ ω ω ≤ ω → ω

(σ → τ ) ∩ (σ → ρ) ≤ σ → τ ∩ ρ and closed under the rules:

σ ≤ σ⁰ τ ≤ τ⁰ σ ∩ τ ≤ σ⁰∩ τ⁰

σ ≤ σ⁰ τ ≤ τ⁰ σ⁰→ τ ≤ σ → τ⁰

3

“Beta-soundness”

Lemma

Jeśli σ → τ 6≡ ω oraz T

j ∈Jpj ∩ T

i ∈I(σi→ τi) ≤ σ → τ to{i | σ ≤ σ_i} 6= ∅oraz T

σ≤σiτi≤ τ.

4

Intersection type assignment (BCD)

Γ (x : σ) ` x : σ (Var) Γ ` M : ω (ω)

Γ(x : σ) ` M : τ (Abs) Γ ` λx M : σ → τ

Γ ` M : σ → τ Γ ` N : σ (App) Γ ` MN : τ

Γ ` M : τ1 Γ ` M : τ2

Γ ` M : τ1∩ τ2 (∩I)

Γ ` M : τ1∩ τ₂ Γ ` M : τi (∩E)

Γ ` M : σ [σ ≤ τ ] (≤) Γ ` M : τ

5

Generation (Inversion) Lemma

I If Γ ` x : σthenΓ(x ) ≤ σ.

I If Γ ` MN : σthenΓ ` M : τ → σand Γ ` N : τ.

I If Γ ` λx .M : σ 6= ωthenσ =T

i(σi→ τ_i).

(If σ 6≡ ωthenτi6≡ ω.)

I If Γ ` λx .M : σ → τthen Γ(x : σ) ` M : τ.

Proof:

Induction wrt(the number of nodes in)the type derivation. By cases depending on the last rule used.

6

Przypadek aplikacji

I IfΓ ` MN : σthenΓ ` M : τ → σandΓ ` N : τ.

Proof:

Induction wrt type derivation.

Example induction step: Last rule used is (∩I).

We haveσ = σ1∩ σ2andΓ ` MN : σ1, andΓ ` MN : σ2, with smaller derivations. Apply the induction hypothesis:

Γ ` M : τ1→ σ1, Γ ` N : τ1

Γ ` M : τ2→ σ2, Γ ` N : τ2.

Then Γ ` M : (τ1→ σ1) ∩ (τ2→ σ2)and Γ ` N : τ1∩ τ2. But(τ1→ σ1) ∩ (τ2→ σ2) ≤ (τ1∩ τ2→ σ1) ∩ (τ1∩ τ2→ σ2)

≤ τ1∩ τ2→ σ1∩ σ2, whence Γ ` M : τ1∩ τ2→ σ1∩ σ2.

Correctness of substitution

Lemma

IfΓ(x : σ) ` M : τandΓ ` N : σ, thenΓ ` M[x := N] : τ.

Proof.

Induction wrtM. For example, ifM = λy Pandτ = µ → ρ thenΓ(x : σ)(y : µ) ` P : ρ, by the inversion lemma.

By the induction hypothesisΓ(y : µ) ` P[x := N] : ρ, whenceΓ ` λy P[x := N] : µ → ρ.

(2)

Subject Reduction

Theorem:

IfΓ ` M : τandM →βηNthenΓ ` N : τ.

Proof:

Induction wrt definition of→βη. Main cases:

M = (λx .P)Q →βP[x := Q] = N.

By inversionΓ ` λx .P : σ → τ andΓ ` Q : σ.

ThenΓ, x : σ ` P : τ, whenceΓ ` P[x := Q] : τ

M = λx .Nx →ηN.

Thenτ =T

i(σi→ τi)andΓ, x : σi` Nx : τi, alli.

It follows thatΓ, x : σi` N : ζi→ τi withσi≤ ζi. Butx 6∈ FV (N), soΓ ` N :T

i(ζi→ τ_i) ≤ τ.

9

Subject Conversion, czyli na odwrót też

Lemma:

Let Γ ` M[x := N] : τ. Then there isσwith Γ ` N : σ and Γ(x : σ) ` M : τ.

Proof:

Induction wrtM. In caseM = y 6= xtakeσ = ω.

WtedyΓ ` N : ωza darmo, orazΓ(x : ω) ` y : τ.

JeśliM = x, tox [x := N] = Ni jakoσbierzemyτ.

10

Lemma:

Proof:

Induction wrtM. W przypadkuM = M1M2, z lematu o generowaniu istnieje takieρ, że:

Γ ` M1[x := N] : ρ → τ oraz Γ ` M2[x := N] : ρ.

Z zał. ind. mamy takieσ1, σ2, że:

Γ ` N : σ1, Γ(x : σ1) ` M1: ρ → τ, Γ ` N : σ2, Γ(x : σ2) ` M2: ρ.

Można więc przyjąćσ = σ1∩ σ2.

11

Lemma:

Proof:

Induction wrtM. NiechM = λy P.

Z lematu o generowaniu:τ =T

i ∈I(αi→ βi), gdzieΓ(y : αi) ` P[x := N] : βi, dlai ∈ I.

Sąσi, żeΓ(y : αi) ` N : σiorazΓ(y : αi)(x : σi) ` P : βi. Niechσ =T

i ∈Iσi. WtedyΓ(y : αi)(x : σ) ` P : βi, skądΓ(x : σ) ` λy P : αi→ βii dobrze.

12

Subject Conversion

Theorem:

IfM →βNthenin system BCD:

Γ ` M : τ iff Γ ` N : τ.

Dowód:

Najważniejszy przypadek wynika z poprzedniego lematu: jeśliΓ ` M[x := N] : τ, to istnieje takieσ, że Γ ` N : σorazΓ(x : σ) ` M : τ. WtedyΓ ` (λx M)N : τ.

N.B.That won’t work for eta: x : p 0 λy . xy : p

13

Interpreting types in a model

Type valuationξ : TV → P(D)assigns sets to type variables.

Interpretation of types:

I [[p]]ξ= ξ(p), for type variablep;

I [[ω]]ξ= D;

I [[σ ∩ τ ]]ξ = [[σ]]ξ∩ [[τ ]]ξ;

I [[σ → τ ]]ξ= [[σ]]ξ⇒ [[τ ]]ξ.

Easy lemma:

Ifσ ≤ τ, then[[σ]]ξ⊆ [[τ ]]_ξ.

14

Semantics of type assignment

WriteD, v , ξ |= M : σwhen[[M]]v∈ [[σ]]ξ.

WriteD, v , ξ |= Γwhenv (x ) ∈ [[Γ(x )]]ξ, for allx ∈ Dom(Γ).

WriteΓ |= M : σwhen, for allD, v , ξ, D, v , ξ |= Γ implies D, v , ξ |= M : σ,

Theorem (Soundness)

If Γ ` M : σ then Γ |= M : σ.

Proof:

Easy induction wrt type derivation.

Filter model

Definition:A setF of types is afilterwhen:

I F is not empty;

I Ifσ, τ ∈ Fthenσ ∩ τ ∈ F;

I Ifσ ∈ F andσ ≤ τthenτ ∈ F.

Example: filtr główny (principal filter) σ↑ = {τ | σ ≤ τ }.

(3)

Application:

F1· F2= {τ | σ → τ ∈ F1, for some σ ∈ F2}

Lemma: IfF1andF2are filters thenF1· F2is a filter.

Proof: (1) Not empty, becauseω ≤ ω → ω, andω ∈ F1, F2. (2) Letτ1, τ2∈ F1· F2. There areσ1→ τ1, σ2→ τ2∈ F1

andσ1, σ2∈ F₂. Thenσ1∩ σ₂∈ F₂and

(σ1→ τ1) ∩ (σ2→ τ2) ≤ σ1∩ σ2→ τ1∩ τ2∈ F1. Henceτ1∩ τ₂∈ F₁· F₂.

(3) Ifσ → τ ∈ F1andτ ≤ τ⁰thenσ → τ⁰∈ F1.

17

Filter model F

Application:

F1· F2= {τ | σ → τ ∈ F1for some σ ∈ F2}.

OtoczenieΓ: zmienne obiektowe −→ typy Wartościowaniev: zmienne obiektowe −→ filtry

An environmentΓisconsistentwith object valuationv when Γ(x ) ∈ v (x ), for allx ∈ Dom(Γ).

Interpretation:

[[M]]v= {σ | Γ ` M : σ, for someΓconsistent withv }.

18

Filter model

[[M]]v= {σ | Γ ` M : σ, for someΓconsistent withv }.

Lemma:

The filter modelFis a lambda-model:

(a) [[x]]v= v (x );

(b) [[PQ]]v= [[P]]v· [[Q]]v;

(c) [[λx.P]]v· F = [[P]]_{v [x 7→a]}, for anyF ∈ F;

(d) Ifv |FV(P)= u|FV(P), then[[P]]v= [[P]]u. (e) If[[λx .M]]v≈ [[λx.N]]_vthen[[λx .M]]v= [[λx .N]]v.

19

Filter model

[[M]]v= {σ | Γ ` M : σ, for some Γ consistent with v }.

Lemma:

The filter modelFis a lambda-model

Proof:

(a) [[x ]]v= v (x ).

(⊆) Supposeσ ∈ [[x ]]v. ThenΓ ` x : σ, withΓ(x ) ∈ v (x ).

By inversion,Γ(x ) ≤ σ, whenceσ ∈ v (x ).

(⊇) Ifσ ∈ v (x )thenΓ = {x : σ}is consistent withv.

20

Filter model

Lemma:

Proof:

(b) [[PQ]]v= [[P]]v· [[Q]]_v.

(⊇) Letσ ∈ [[P]]v· [[Q]]v, i.e.,ζ → σ ∈ [[P]]v andζ ∈ [[Q]]v. ThenΓ1` P : ζ → σandΓ2` Q : ζ.

TakeΓ0= Γ1&Γ2and thenΓ0` P : ζ → σandΓ0` Q : ζ.

AndΓ0(x ) = Γ1(x ) ∩ Γ2(x ) ∈ v (x )soΓ0consistent withv. (⊆) Supposeσ ∈ [[PQ]]v. ThenΓ ` PQ : σ, so by inversion we haveΓ ` P : τ → σandΓ : Q : τ. Thusτ → σ ∈ [[P]]v

andτ ∈ [[Q]]v, whenceσ ∈ [[P]]v· [[Q]]v. Opuszczamy części (c) i (d).

21

Lemma:

Proof:

(e) If[[λx .M]]v≈ [[λx.N]]vthen[[λx .M]]v= [[λx .N]]v. Niechσ ∈ [[λx .M]]v. Wtedyσ =T

i ∈I(σi→ τi), i jest takieΓ, żeΓ, x : σi` M : τi, dlai ∈ I.

Wtedyτi∈ [[M]]_{v [x 7→σ}_i_↑]. Z założenia wynika, że

[[M]]v [x 7→σi↑]= [[λx M]]v· σi↑ = [[λx N]]v· σi↑ = [[N]]v [x 7→σi↑], więcτi∈ [[N]]_{v [x 7→σ}_i_↑], skądΓi` N : τi, dla pewnegoΓi

zgodnego zv [x 7→ σi↑], tj.Γi(x ) ≥ σi.

WtedyΓi` λx N : σi→ τi, skądσi→ τi∈ [[λx N]]v. No toσ ∈ [[λx N]]vjako iloczyn.

22

Lemma:

Letξ(p) = {F | F filter, andp ∈ F }. For allτ: [[τ ]]ξ= {F | Ffilter, andτ ∈ F }.

Inaczej:τ ∈ F ⇔ F ∈ [[τ ]]ξ.

Proof:

Caseτ = α → β. Then[[α → β]]ξ= [[α]]ξ⇒ [[β]]ξ=

= {F | ∀G (G ∈ [[α]]ξ → F · G ∈ [[β]]ξ)}

= {F | ∀G ( α ∈ G → β ∈ F · G )}

= {F | ∀G ( α ∈ G → ∃σ ∈ G (σ → β ∈ F ))}.

We need

α → β ∈ F ⇔ ∀G (α ∈ G → ∃σ ∈ G (σ → β ∈ F )).

Part(⇒)is obvious.

For(⇐)takeG = α↑. There isσ ∈ α↑withσ → β ∈ F. Thenσ → β ≤ α → β ∈ F.

Lemma:

Letξ(p) = {F | F filter, andp ∈ F }. Then for allτ [[τ ]]ξ= {F | Ffilter, andτ ∈ F }.

Proof:

Przypadekτ = α ∩ β. Teraz[[τ ]]ξ= [[α]]ξ∩ [[β]]ξ, czyli [[τ ]]ξ= {F | α ∈ F } ∩ {F | β ∈ F } = {F | α ∈ F ∧ β ∈ F }.

AleFjest filtrem, więc:

α ∩ β ∈ F ⇔ α ∈ F ∧ β ∈ F

(4)

Completeness of type assignment

Theorem:

If Γ |= M : σ then Γ ` M : σ.

Proof:

Letξ(p) = {F | p ∈ F }andv (x ) = Γ(x )↑.

ThenΓ(x ) ∈ v (x ), thusv (x ) ∈ [[Γ(x )]]ξ. That is,F , v , ξ |= Γ, whenceF , v , ξ |= M : σ.

Therefore[[M]]v∈ [[σ]]ξ, i.e.,σ ∈ [[M]]v.

There isΓ⁰, consistent withv, such thatΓ⁰` M : σ.

We haveΓ⁰(x ) ∈ v (x ) = Γ(x )↑, whenceΓ(x ) ≤ Γ⁰(x ).

It follows thatΓ ` M : σ.

25

Jeszcze jedno twierdzenie

Następujące warunki są równoważne (dla systemu BCD):

I BT(M) = BT(N);

I TermyMiNmają te same typy w każdym otoczeniu.

26

Scott type assignment

Modify system BCD so that:

I There are two type constantsωandκ;

I There is no other atom (no type variables);

I Subtyping is extended byκ ≡ ω → κ.

The filter model for this type system is isomorphic withD∞, whereD0= {⊥, >}. The isomorphism maps⊥to{ω}, and>to the set of all types.

Scott type assignment is complete forD_∞.

27

Intersection types without omega

Γ (x : σ) ` x : σ (Var)

Γ(x : σ) ` M : τ (Abs) Γ ` λx M : σ → τ

Γ ` M : σ → τ Γ ` N : σ (App) Γ ` MN : τ

Γ ` M : τ1 Γ ` M : τ2

(∩I) Γ ` M : τ1∩ τ2

Γ ` M : τ1∩ τ2

(∩E) Γ ` M : τi

Γ ` M : σ [σ ≤ τ ] Γ ` M : τ (≤)

28

Intersection types without subtyping

Γ (x : σ) ` x : σ (Var)

Γ(x : σ) ` M : τ (Abs) Γ ` λx M : σ → τ

Γ ` M : σ → τ Γ ` N : σ (App) Γ ` MN : τ

Γ ` M : τ1 Γ ` M : τ2

(∩I) Γ ` M : τ1∩ τ₂

Γ ` M : τ1∩ τ2

(∩E) Γ ` M : τi

29

With or without subtyping

Theorem

A type judgment is derivable in the system with rule(≤) if and only if it is derivable in the system with rule

(η) Γ ` M : σ, M →ηN Γ ` N : σ

Example:

x : (α → β) ∩ (α → γ) ` λy . xy : α → (β ∩ γ).

30

No omega and no subtyping

Generation (Inversion) Lemma:

I If Γ ` x : σthenΓ(x ) = σ ∩ τ.

I If Γ ` MN : σthenσ =T

iσi, where Γ ` M :T

i(τi→ σi)and Γ ` N :T

iτi.

I If Γ ` λx .M : σthenσ =T

i(σi→ τi), where Γ(x : σi) ` M : τi.

Lemma:

IfΓ, x : σ ` M : τ andΓ ` N : σ, thenΓ ` M[x := N] : τ.

Subject Reduction (bez ω i ≤)

Theorem:

IfΓ ` M : τandM →βN thenΓ ` N : τ.

Remark:

No more subject conversion, e.g., KIΩ → I.

Remark:

No more subject reduction forη, e.g., x : (α → β) ∩ (α → γ) ` λy . xy : α → (β ∩ γ) x : (α → β) ∩ (α → γ) 0 x : α → (β ∩ γ)

(5)

Silna normalizacja

Termy typowalne nie mają nieskończonych redukcji

33

Strong normalization: Tait’s proof method

Definition:

Stable (computable,reducible. . . ) terms:

I [[p]] := SN;

I [[τ → σ]] := {M | ∀N(N ∈ [[τ ]] ⇒ MN ∈ [[σ]])};

I [[τ ∩ σ]] := [[τ ]] ∩ [[σ]].

Lemma:

Ifτ ≤ σ, then[[τ ]] ⊆ [[σ]].

34

Lemma:

1) [[τ ]] ⊆ SN;

2) IfN1, . . . , Nk∈ SNthenxN1. . . Nk∈ [[τ ]].

In particular, variables are stable for every type.

Proof:

Induction wrtτ. Ifτ = pthen (1) is immediate.

Also (2), becausexN1. . . Nk∈ SN.

Forτ = σ ∩ ρapply induction. Letτ = σ → ρ.

(1) TakeM ∈ [[σ → ρ]]. By the ind. hyp. (2), we havex ∈ [[σ]], so thatMx ∈ [[ρ]]. ThusMx ∈ SN, by the ind. hyp. (1). HenceM ∈ SN.

(2) We wantxN1. . . NkP ∈ [[ρ]], wheneverP ∈ [[σ]].

ButP ∈ SNby the ind. hyp. (1), and we can apply ind. hyp. (2) toρ.

35

Lemma:

LetM[x :=N0]N1. . . Nk∈ SNandN0∈ SN.

Then also(λx .M)N0N1. . . Nk∈ SN.

Proof:

Ciąg redukcji postaci

(λx .M)N0N1. . . Nk (λx.M⁰)N₀⁰N₁⁰. . . N_k⁰ musi być skończony. No to wreszcie:

(λx .M)N0N1. . . Nk M⁰[x := N₀⁰]N₁⁰. . . N_k⁰. Ale ponieważ

SN 3 M[x :=N0]N1. . . Nk M⁰[x := N₀⁰]N₁⁰. . . N_k⁰, więc i to się skończy.

36

Lemma:

LetM[x :=N0]N1. . . Nk∈ SNandN0∈ SN.

Then also(λx .M)N0N1. . . Nk∈ SN.

Lemma:

LetM[x :=N0]N1. . . Nk∈ [[τ ]]orazN0∈ SN.

Then also(λx .M)N0N1. . . Nk∈ [[τ ]].

Proof:

Induction wrtτ. Base case above.

Forτ = σ ∩ ρapply induction. Letτ = σ → ρ.

LetM[x := N0]N1. . . Nk∈ [[σ → ρ]] = [[σ]] ⇒ [[ρ]]

andP ∈ [[σ]]. We want(λx .M)N0N1. . . NkP ∈ [[ρ]].

ThenM[x := N0]N1. . . NkP ∈ [[ρ]].

Apply induction toρwithNk+1= P.

37

Lemma:

LetΓ ` M : τandNi∈ [[Γ(x_i)]], fori ≤ n.

ThenM[x1:=N1, . . . , xn:=Nn] ∈ [[τ ]].

Proof:

Induction wrt derivation ofΓ ` M : τ.

Example case: Γ ` λy P : σ → ρ, becauseΓ(y : σ) ` P : ρ.

We want(λy P)[~x := ~N] ∈ [[σ → ρ]]. LetQ ∈ [[σ]].

By ind. hyp.,P[~x := ~N][y := Q] = P[~x := ~N, y := Q] ∈ [[ρ]], so(λy .P[~x := ~N])Q ∈ [[ρ]], by the previous lemma.

That’s what we need.

38

Strong Normalization

Theorem:

IfΓ ` M : τthenM ∈ SN.

Proof:

LetFV(M) = ~x. Variables are stable, so we have M = M[~x := ~x ] ∈ [[τ ]] ⊆ SN.

Dygresja: sens moralny numeracji gödlowskiej

Natural number– prototype of finite object.

Peano Arithmetic– prototype of finitary reasoning.

Gödel’s Incompleteness Theorem:There are arithmetical statements unprovable in Peano Arithmetic.

(6)

Strong Normalization

For every typable lambda-termM, every reduction sequence ofMis finite.

Using König’s Lemma:

For every typable lambda-termM, there existsksuch that every reduction sequence ofMhas at mostksteps.

Arithmetization:

For every numbernof a type derivation for a lambda-termM there existsmsuch that every number of a finite reduction sequence ofMis less thanm.

41