Rachunek lambda, lato 2019-20

(1)

Rachunek lambda, lato 2019-20

Wykład 9

24 kwietnia 2020

(2)

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.

(3)

Subtyping (BCD):

Define≤ as the least quasi-order satisfying the axioms:

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

(σ → τ ) ∩ (σ → ρ) ≤ σ → τ ∩ ρ

and closed under the rules:

σ ≤ σ⁰ τ ≤ τ⁰

0 0

σ ≤ σ⁰ τ ≤ τ⁰

0 0

(4)

“Beta-soundness”

Lemma

Jeśli σ → τ 6≡ ω oraz T

j ∈Jp_j ∩ T

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

σ≤σiτ_i ≤ τ.

(5)

Intersection type assignment (BCD)

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

Γ(x : σ) ` M : τ

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

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

(App) Γ ` MN : τ

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

Γ ` M : τ₁∩ τ₂ (∩E) Γ ` M : τ_i

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

(6)

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 τ_i 6≡ ω.)

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.

(7)

Przypadek aplikacji

Proof:

Induction wrt type derivation.

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

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

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

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

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

≤ τ₁∩ τ₂ → σ₁∩ σ₂, whence Γ ` M : τ₁∩ τ₂ → σ₁∩ σ₂.

(8)

Przypadek aplikacji

Proof:

We haveσ = σ₁ ∩ σ₂ and Γ ` MN : σ₁, and Γ ` MN : σ₂, with smaller derivations.

Apply the induction hypothesis: Γ ` M : τ1 → σ1, Γ ` N : τ1

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

(9)

Przypadek aplikacji

Proof:

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

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

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

(10)

Przypadek aplikacji

Proof:

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

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

Then Γ ` M : (τ₁ → σ₁) ∩ (τ₂ → σ₂)and Γ ` N : τ₁∩ τ₂.

But(τ1 → σ1) ∩ (τ2 → σ2) ≤ (τ1∩ τ2 → σ1) ∩ (τ1∩ τ2 → σ2)

(11)

Przypadek aplikacji

Proof:

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

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

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

(12)

Correctness of substitution

Lemma

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

Proof.

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

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

(13)

Subject Reduction

Theorem:

If Γ ` M : τ and M →_βη N then Γ ` 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, all i. It follows that Γ, x : σ_i ` N : ζ_i → τ_i with σ_i ≤ ζ_i. Butx 6∈ FV (N), so Γ ` N :T

i(ζ_i → τ_i) ≤ τ.

(14)

Subject Reduction

Theorem:

Proof:

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

By inversion Γ ` λx .P : σ → τ and Γ ` Q : σ. ThenΓ, x : σ ` P : τ, whence Γ ` P[x := Q] : τ

i(ζ_i → τ_i) ≤ τ.

(15)

Subject Reduction

Theorem:

Proof:

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

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

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

i(ζ_i → τ_i) ≤ τ.

(16)

Subject Reduction

Theorem:

Proof:

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

M = λx .Nx →_η N.

Thenτ =T

i(ζ_i → τ_i) ≤ τ.

(17)

Subject Reduction

Theorem:

Proof:

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

i(σ_i → τ_i)and Γ, x : σ_i ` Nx : τ_i, all i. It follows that Γ, x : σ_i ` N : ζ_i → τ_i with σ_i ≤ ζ_i.

(18)

Subject Conversion, czyli na odwrót też

Lemma:

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

Proof:

Induction wrt M. In case M = y 6= x take σ = ω. WtedyΓ ` N : ω za darmo, oraz Γ(x : ω) ` y : τ.

JeśliM = x, to x [x := N] = N i jako σ bierzemy τ.

(19)

Subject Conversion, czyli na odwrót też

Lemma:

Proof:

Induction wrt M. In case M = y 6= x take σ = ω.

WtedyΓ ` N : ω za darmo, oraz Γ(x : ω) ` y : τ. JeśliM = x, to x [x := N] = N i jako σ bierzemy τ.

(20)

Subject Conversion, czyli na odwrót też

Lemma:

Proof:

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

(21)

Subject Conversion, czyli na odwrót też

Lemma:

Proof:

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

(22)

Lemma:

Proof:

Induction wrt M. W przypadku M = M₁M₂, z lematu o generowaniu istnieje takieρ, że:

Γ ` M1[x := N] : ρ → τ oraz Γ ` M2[x := N] : ρ. Z zał. ind. mamy takieσ₁, σ₂, że:

Γ ` N : σ1, Γ(x : σ1) ` M1 : ρ → τ, Γ ` N : σ2, Γ(x : σ2) ` M2 : ρ. Można więc przyjąć σ = σ₁∩ σ₂.

(23)

Lemma:

Proof:

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

Z zał. ind. mamy takieσ₁, σ₂, że:

Γ ` N : σ1, Γ(x : σ1) ` M1 : ρ → τ, Γ ` N : σ2, Γ(x : σ2) ` M2 : ρ. Można więc przyjąć σ = σ₁∩ σ₂.

(24)

Lemma:

Proof:

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

Z zał. ind. mamy takieσ₁, σ₂, że:

Γ ` N : σ₁, Γ(x : σ₁) ` M₁ : ρ → τ, Γ ` N : σ2, Γ(x : σ2) ` M2 : ρ.

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

(25)

Lemma:

Proof:

Induction wrt M. Niech M = λy P. Z lematu o generowaniu: τ = T

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

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

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

(26)

Lemma:

Proof:

Induction wrt M. Niech M = λy P.

Z lematu o generowaniu: τ = T

(27)

Lemma:

Proof:

Są σ_i, że Γ(y : α_i) ` N : σ_i oraz Γ(y : α_i)(x : σ_i) ` P : β_i.

Niechσ = T

(28)

Lemma:

Proof:

(29)

Subject Conversion

Theorem:

If M →_β N then in 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

(30)

Subject Conversion

Theorem:

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

Dowód:

(31)

Subject Conversion

Theorem:

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

Dowód:

(32)

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 [[σ]]_ξ⊆ [[τ ]]_ξ.

(33)

Interpreting types in a model

I [[ω]]_ξ= D;

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

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

Easy lemma:

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

(34)

Interpreting types in a model

I [[ω]]_ξ= D;

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

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

Easy lemma:

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

(35)

Semantics of type assignment

Write D, v , ξ |= M : σ when[[M]]_v ∈ [[σ]]_ξ.

Write D, v , ξ |= Γwhen v (x ) ∈ [[Γ(x )]]_ξ, for all x ∈ 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.

(36)

Semantics of type assignment

Write D, v , ξ |= Γwhen v (x ) ∈ [[Γ(x )]]_ξ, for all x ∈ Dom(Γ).

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

Theorem (Soundness)

Proof:

(37)

Semantics of type assignment

Theorem (Soundness)

Proof:

(38)

Semantics of type assignment

Theorem (Soundness)

(39)

Filter model

Definition: A set F of types is a filter when:

I F is not empty;

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

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

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

(40)

Filter model

Definition: A set F of types is a filter when:

I F is not empty;

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

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

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

(41)

Application: F

₁

· F

₂

= {τ | σ → τ ∈ F

₁

, for some σ ∈ F

₂

}

Lemma: If F1 and F2 are filters thenF1 · F2 is a filter.

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

and σ₁, σ₂ ∈ F₂. Then σ₁∩ σ₂ ∈ F₂ and

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

(3) If σ → τ ∈ F₁ and τ ≤ τ⁰ then σ → τ⁰ ∈ F₁.

(42)

Application: F

₁

· F

₂

= {τ | σ → τ ∈ F

₁

, for some σ ∈ F

₂

}

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

(43)

Application: F

₁

· F

₂

= {τ | σ → τ ∈ F

₁

, for some σ ∈ F

₂

}

Proof: (1) Not empty, because ω ≤ ω → ω, and ω ∈ F₁, F₂.

(2) Letτ1, τ2 ∈ F1· F2. There areσ1 → τ1, σ2 → τ2 ∈ F1

(44)

Application: F

₁

· F

₂

= {τ | σ → τ ∈ F

₁

, for some σ ∈ F

₂

}

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

and σ1, σ2 ∈ F2. Then σ1∩ σ2 ∈ F2 and

(45)

Application: F

₁

· F

₂

= {τ | σ → τ ∈ F

₁

, for some σ ∈ F

₂

}

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

and σ1, σ2 ∈ F2. Then σ1∩ σ2 ∈ F2 and

(46)

Filter model F

Application:

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

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

An environment Γ is consistent with object valuation v when Γ(x ) ∈ v (x ), for allx ∈ Dom(Γ).

Interpretation:

(47)

Filter model

F₁· F₂ = {τ | σ → τ ∈ F₁ for some σ ∈ F2}.

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

Lemma:

The filter model F is 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 any F ∈ F; (d) If v |_FV(P)= u|_FV(P), then [[P]]v = [[P]]u.

(e) If [[λx .M]] ≈ [[λx.N]] then [[λx .M]] = [[λx .N]] .

(48)

Filter model

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

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

Lemma:

The filter model F is 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.

(49)

Filter model

Lemma:

Proof:

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

(⊇) Letσ ∈ [[P]]_v · [[Q]]_v, i.e., ζ → σ ∈ [[P]]_v and ζ ∈ [[Q]]_v. ThenΓ₁ ` P : ζ → σ and Γ₂ ` Q : ζ.

TakeΓ₀ = Γ₁&Γ₂ and then Γ₀ ` P : ζ → σ and Γ₀ ` Q : ζ.

AndΓ0(x ) = Γ1(x ) ∩ Γ2(x ) ∈ v (x )so Γ0 consistent with v.

(⊆) 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).

(50)

Filter model

Lemma:

Proof:

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

AndΓ0(x ) = Γ1(x ) ∩ Γ2(x ) ∈ v (x )so Γ0 consistent with v. (⊆) Supposeσ ∈ [[PQ]]v. Then Γ ` PQ : σ, so by inversion

Opuszczamy części (c) i (d).

(51)

Filter model

Lemma:

Proof:

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

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

(52)

Lemma:

Proof:

(e) If [[λx .M]]_v ≈ [[λx.N]]_v then [[λx .M]]_v = [[λx .N]]_v.

Niechσ ∈ [[λx .M]]v. Wtedy σ =T

i ∈I(σi → τi), i jest takieΓ, że Γ, x : σ_i ` M : τ_i, dla i ∈ 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 z v [x 7→ σ_i↑], tj.Γ_i(x ) ≥ σ_i.

WtedyΓ_i ` λx N : σ_i → τ_i, skąd σ_i → τ_i ∈ [[λx N]]_v. No toσ ∈ [[λx N]]_v jako iloczyn.

(53)

Lemma:

Proof:

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

i ∈I(σi → τi), i jest takieΓ, że Γ, x : σ_i ` M : τ_i, dla i ∈ 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 z v [x 7→ σ_i↑], tj.Γ_i(x ) ≥ σ_i.

(54)

Lemma:

Proof:

[[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 z v [x 7→ σ_i↑], tj.Γ_i(x ) ≥ σ_i.

(55)

Lemma:

Proof:

[[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 z v [x 7→ σ_i↑], tj. Γ_i(x ) ≥ σ_i.

(56)

Lemma:

Proof:

[[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 z v [x 7→ σ_i↑], tj. Γ_i(x ) ≥ σ_i.

(57)

Lemma:

Letξ(p) = {F | F filter, andp ∈ F }. For all τ: [[τ ]]_ξ = {F | F filter, 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.

(58)

Lemma:

Proof:

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

[[α]]_ξ⇒ [[β]]_ξ =

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

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

(59)

Lemma:

Proof:

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

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

(60)

Lemma:

Proof:

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

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

(61)

Lemma:

Proof:

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

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

(62)

Lemma:

Proof:

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

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

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

We need

(63)

Lemma:

Proof:

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

(64)

Lemma:

Proof:

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

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

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

We need

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

(65)

Lemma:

Proof:

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

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

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

We need

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

(66)

Lemma:

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

Proof:

Przypadek τ = α ∩ β. Teraz [[τ ]]_ξ = [[α]]_ξ∩ [[β]]_ξ, czyli [[τ ]]_ξ= {F | α ∈ F } ∩ {F | β ∈ F } = {F | α ∈ F ∧ β ∈ F }. AleF jest filtrem, więc:

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

(67)

Lemma:

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

Proof:

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

AleF jest filtrem, więc:

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

(68)

Completeness of type assignment

Theorem:

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

Proof:

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

ThenΓ(x ) ∈ v (x ), thus v (x ) ∈ [[Γ(x )]]_ξ. That is, F , v , ξ |= Γ, whence F , v , ξ |= M : σ. Therefore[[M]]v ∈ [[σ]]ξ, i.e., σ ∈ [[M]]v.

There is Γ⁰, consistent with v, such that Γ⁰ ` M : σ. We haveΓ⁰(x ) ∈ v (x ) = Γ(x )↑, whence Γ(x ) ≤ Γ⁰(x ). It follows that Γ ` M : σ.

(69)

Completeness of type assignment

Theorem:

Proof:

ThenΓ(x ) ∈ v (x ), thus v (x ) ∈ [[Γ(x )]]_ξ.

That is, F , v , ξ |= Γ, whence F , v , ξ |= M : σ. Therefore[[M]]v ∈ [[σ]]ξ, i.e., σ ∈ [[M]]v.

(70)

Completeness of type assignment

Theorem:

Proof:

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

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

(71)

Completeness of type assignment

Theorem:

Proof:

(72)

Completeness of type assignment

Theorem:

Proof:

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

We haveΓ⁰(x ) ∈ v (x ) = Γ(x )↑, whence Γ(x ) ≤ Γ⁰(x ). It follows that Γ ` M : σ.

(73)

Completeness of type assignment

Theorem:

Proof:

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

It follows that Γ ` M : σ.

(74)

Completeness of type assignment

Theorem:

Proof:

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

It follows that Γ ` M : σ.

(75)

Jeszcze jedno twierdzenie

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

I BT(M) = BT(N);

I Termy M i N mają te same typy w każdym otoczeniu.

(76)

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

(77)

Intersection types without omega

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

Γ(x : σ) ` M : τ

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

(App) Γ ` MN : τ

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

Γ ` M : τ₁∩ τ₂ (∩E) Γ ` M : τ_i

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

(78)

Intersection types without subtyping

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

Γ(x : σ) ` M : τ

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

(App) Γ ` MN : τ

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

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

Γ ` M : τ1∩ τ2

(∩E) Γ ` M : τ_i

(79)

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 : α → (β ∩ γ).

(80)

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] : τ.

(81)

Subject Reduction (bez ω i ≤)

Theorem:

If Γ ` M : τ and M →_β 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 : α → (β ∩ γ)

(82)

Subject Reduction (bez ω i ≤)

Theorem:

Remark:

(83)

Subject Reduction (bez ω i ≤)

Theorem:

Remark:

(84)

Silna normalizacja

Termy typowalne nie mają nieskończonych redukcji

(85)

Strong normalization: Tait’s proof method

Definition:

Stable (computable,reducible. . . ) terms:

I [[p]] := SN;

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

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

Lemma:

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

(86)

Lemma:

1) [[τ ]] ⊆ SN;

2) If N₁, . . . , N_k ∈ SNthen xN₁. . . N_k ∈ [[τ ]].

In particular, variables are stable for every type.

Proof:

Induction wrt τ. If τ = p then (1) is immediate.

Also (2), because xN1. . . N_k ∈ SN.

Forτ = σ ∩ ρ apply induction. Let τ = σ → ρ. (1) TakeM ∈ [[σ → ρ]]. By the ind. hyp. (2), we have x ∈ [[σ]], so that Mx ∈ [[ρ]]. Thus Mx ∈ SN, by the ind. hyp. (1). Hence M ∈ SN.

(2) We wantxN₁. . . N_kP ∈ [[ρ]], whenever P ∈ [[σ]]. ButP ∈ SN by the ind. hyp. (1), and we can apply ind. hyp. (2) toρ.

(87)

Lemma:

1) [[τ ]] ⊆ SN;

Proof:

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

(1) TakeM ∈ [[σ → ρ]]. By the ind. hyp. (2), we have x ∈ [[σ]], so that Mx ∈ [[ρ]]. Thus Mx ∈ SN, by the ind. hyp. (1). Hence M ∈ SN.

(88)

Lemma:

1) [[τ ]] ⊆ SN;

Proof:

(89)

Lemma:

1) [[τ ]] ⊆ SN;

Proof:

(2) We wantxN₁. . . N_kP ∈ [[ρ]], wheneverP ∈ [[σ]].

ButP ∈ SN by the ind. hyp. (1), and we can apply