Rachunek lambda, lato 2019-20

Rachunek lambda, lato 2019-20

Wykład 8

17 kwietnia 2020

Typy

Typy: motywacja semantyczna

Typ = podzbiór modelu (własność jego elementów)

I Trivial property – the whole domainD, denoted byω;

I Intersection σ ∩ τ of propertiesσ and τ;

I Function space:

σ ⇒ τ = {a ∈ D | ∀b ∈ D(b ∈ σ → a · b ∈ τ )}.

Subtyping in a model

σ ∩ τ ⊆ σ σ ∩ τ ⊆ τ σ ⊆ σ ∩ σ

σ ⊆ ω ω ⊆ ω ⇒ ω

(σ ⇒ τ ) ∩ (σ ⇒ ρ) ⊆ σ ⇒ τ ∩ ρ

If σ ⊆ σ⁰ and τ ⊆ τ⁰ then

σ ∩ τ ⊆ σ⁰∩ τ⁰ σ⁰ ⇒ τ ⊆ σ ⇒ τ⁰

Subtyping in a model

σ ∩ τ ⊆ σ σ ∩ τ ⊆ τ σ ⊆ σ ∩ σ

σ ⊆ ω ω ⊆ ω ⇒ ω

(σ ⇒ τ ) ∩ (σ ⇒ ρ) ⊆ σ ⇒ τ ∩ ρ

If σ ⊆ σ⁰ and τ ⊆ τ⁰ then

σ ∩ τ ⊆ σ⁰∩ τ⁰ σ⁰ ⇒ τ ⊆ σ ⇒ τ⁰

Subtyping in a model

σ ∩ τ ⊆ σ σ ∩ τ ⊆ τ σ ⊆ σ ∩ σ

σ ⊆ ω ω ⊆ ω ⇒ ω

(σ ⇒ τ ) ∩ (σ ⇒ ρ) ⊆ σ ⇒ τ ∩ ρ

If σ ⊆ σ⁰ and τ ⊆ τ⁰ then

σ ∩ τ ⊆ σ⁰∩ τ⁰ σ⁰ ⇒ τ ⊆ σ ⇒ τ⁰

Subtyping in a model

σ ∩ τ ⊆ σ σ ∩ τ ⊆ τ σ ⊆ σ ∩ σ

σ ⊆ ω ω ⊆ ω ⇒ ω

(σ ⇒ τ ) ∩ (σ ⇒ ρ) ⊆ σ ⇒ τ ∩ ρ

If σ ⊆ σ⁰ and τ ⊆ τ⁰ then σ ∩ τ ⊆ σ⁰∩ τ⁰

σ⁰ ⇒ τ ⊆ σ ⇒ τ⁰

Subtyping in a model

σ ∩ τ ⊆ σ σ ∩ τ ⊆ τ σ ⊆ σ ∩ σ

σ ⊆ ω ω ⊆ ω ⇒ ω

(σ ⇒ τ ) ∩ (σ ⇒ ρ) ⊆ σ ⇒ τ ∩ ρ

If σ ⊆ σ⁰ and τ ⊆ τ⁰ then

σ ∩ τ ⊆ σ⁰∩ τ⁰ σ⁰ ⇒ τ ⊆ σ ⇒ τ⁰

Formal type assignment

Atype assignment system derives judgements of the form Γ ` M : τ,

whereM is a λ-term,τ is a type,

and Γ is a set of type declarations for free variables.

Intersection types (formal system)

Types:

I The constant ω is a type.

I Type variablesp, q, · · · ∈ TV are types. (*)

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

I If σ and τ are types then (σ ∩ τ ) is a type. Klauzule (*) definiujątypy proste.

Assumption:

Intersection is commutative, associative and idempotent. Convention: Arrow is “right-associative”, that is,

τ → (σ → ρ) is written τ → σ → ρ.

Intersection types (formal system)

Types:

I The constant ω is a type.

I Type variablesp, q, · · · ∈ TV are types. (*)

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

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

Klauzule (*) definiujątypy proste.

Assumption:

Intersection is commutative, associative and idempotent. Convention: Arrow is “right-associative”, that is,

τ → (σ → ρ) is written τ → σ → ρ.

Intersection types (formal system)

Types:

I The constant ω is a type.

I Type variablesp, q, · · · ∈ TV are types. (*)

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

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

Klauzule (*) definiujątypy proste.

Assumption:

Intersection is commutative, associative and idempotent.

Convention: Arrow is “right-associative”, that is, τ → (σ → ρ) is written τ → σ → ρ.

Subtyping (BCD)

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

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

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

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

σ ≤ σ⁰ τ ≤ τ⁰ σ⁰ → τ ≤ σ → τ⁰ Przykład: p ∩ (a → b) ∩ (c → d ) ≤ a ∩ c ∩ p → b.

Napisσ ≡ τ oznaczaσ ≤ τ ≤ σ. Takie typy czasem się utożsamia.

Subtyping (BCD)

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

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

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

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

σ ≤ σ⁰ τ ≤ τ⁰ σ⁰ → τ ≤ σ → τ⁰ Przykład: p ∩ (a → b) ∩ (c → d ) ≤ a ∩ c ∩ p → b.

Napisσ ≡ τ oznaczaσ ≤ τ ≤ σ.

Takie typy czasem się utożsamia.

“Beta-soundness”

Lemma

Jeśli σ → τ 6≡ ω oraz T

j ∈Jp_j ∩ T

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

σ≤σiτ_i ≤ τ.

Proof.

Indukcja ze względu na definicję≤.

Environments

Anenvironment (also called “context” or “base” or. . . ) is a finite partial functionΓ : Var → Type, identified with the set of pairs x : Γ(x ), for x ∈ Dom(Γ).

AssumeΓ(x ) = ω, for x 6∈ Dom(Γ).

Write Γ(x : τ ) for the environment Γ⁰ such that Γ⁰(x ) = τ and otherwiseΓ⁰(y ) = Γ(y ). Write Γ1& Γ2 for the environment Γ⁰⁰ such that

Γ⁰⁰(x ) = Γ₁(x ) ∩ Γ₂(x ).

Przykład: Γ1 = {(x : τ ), (y : σ)}, Γ2 = {(x : ρ), (z : τ )}. WtedyΓ₁(x : σ)& Γ₂ = {(x : σ ∧ ρ), (y : σ), (z : τ )}.

Environments

Anenvironment (also called “context” or “base” or. . . ) is a finite partial functionΓ : Var → Type, identified with the set of pairs x : Γ(x ), for x ∈ Dom(Γ).

AssumeΓ(x ) = ω, for x 6∈ Dom(Γ).

Write Γ(x : τ ) for the environment Γ⁰ such that Γ⁰(x ) = τ and otherwiseΓ⁰(y ) = Γ(y ).

Write Γ1& Γ2 for the environment Γ⁰⁰ such that Γ⁰⁰(x ) = Γ₁(x ) ∩ Γ₂(x ).

Przykład: Γ1 = {(x : τ ), (y : σ)}, Γ2 = {(x : ρ), (z : τ )}. WtedyΓ₁(x : σ)& Γ₂ = {(x : σ ∧ ρ), (y : σ), (z : τ )}.

Environments

Anenvironment (also called “context” or “base” or. . . ) is a finite partial functionΓ : Var → Type, identified with the set of pairs x : Γ(x ), for x ∈ Dom(Γ).

AssumeΓ(x ) = ω, for x 6∈ Dom(Γ).

Write Γ(x : τ ) for the environment Γ⁰ such that Γ⁰(x ) = τ and otherwiseΓ⁰(y ) = Γ(y ).

Write Γ1& Γ2 for the environment Γ⁰⁰ such that Γ⁰⁰(x ) = Γ₁(x ) ∩ Γ₂(x ).

Przykład: Γ1 = {(x : τ ), (y : σ)}, Γ2 = {(x : ρ), (z : τ )}. WtedyΓ₁(x : σ)& Γ₂ = {(x : σ ∧ ρ), (y : σ), (z : τ )}.

Environments

Anenvironment (also called “context” or “base” or. . . ) is a finite partial functionΓ : Var → Type, identified with the set of pairs x : Γ(x ), for x ∈ Dom(Γ).

AssumeΓ(x ) = ω, for x 6∈ Dom(Γ).

Write Γ(x : τ ) for the environment Γ⁰ such that Γ⁰(x ) = τ and otherwiseΓ⁰(y ) = Γ(y ).

Write Γ1& Γ2 for the environment Γ⁰⁰ such that Γ⁰⁰(x ) = Γ₁(x ) ∩ Γ₂(x ).

Intersection type assignment (BCD)

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

Γ(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 : τ

BCD = Barendregt, Coppo, Dezani

Example

Γ(x : σ) ` M : τ

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

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

(App) Γ ` MN : τ

z : τ, x : τ, y : σ ` x : τ z : τ, x : τ ` λy x : σ → τ

z : τ ` λxy . x : τ → σ → τ z : τ ` z : τ

Example

Γ(y : σ) ` M : τ

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

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

(App) Γ ` MN : τ

x : τ, y : σ ` x : τ x : τ, y : τ ` λy x : σ → τ

y : τ ` λxy . x : τ → σ → τ y : τ ` y : τ y : τ ` (λxy . x )y : σ → τ

Explanation: {(x : τ, y : τ )}(y : σ) = {(x : τ, y : σ)}

Example

Γ(y : σ) ` M : τ

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

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

(App) Γ ` MN : τ

x : τ, y : σ ` x : τ x : τ, y : τ ` λy x : σ → τ

y : τ ` λxy . x : τ → σ → τ y : τ ` y : τ y : τ ` (λxy . x )y : σ → τ

Example

Γ ` M : τ<sub>1</sub> Γ ` M : τ₂ (∩I) Γ ` M : τ₁∩ τ₂

Γ ` M : τ<sub>1</sub>∩ τ<sub>2</sub> (∩E) Γ ` M : τ_i

x : p ∩ (p → q) ` x : p ∩ (p → q) x : p ∩ (p → q) ` x : p

x : p ∩ (p → q) ` x : p ∩ (p → q) x : p ∩ (p → q) ` x : p → q x : p ∩ (p → q) ` xx : q

` λx. xx : p ∩ (p → q) → q

Examples

I ` I : t ∩ s → t;

I ` I : t → t;

I ` 2 : (t → s) ∩ (s → r ) → (t → r );

I ` 2 : (t → t) → t → t;

I ` K : t → s → t;

I ` S : (t⁰ → s → r ) → (t⁰⁰ → s) → (t⁰∩ t⁰⁰) → r;

I ` S : (t → s → r ) → (t → s) → t → r.

Examples

I ` I : t ∩ s → t;

I ` I : t → t;

I ` 2 : (t → s) ∩ (s → r ) → (t → r );

I ` 2 : (t → t) → t → t;

I ` K : t → s → t;

I ` S : (t⁰ → s → r ) → (t⁰⁰ → s) → (t⁰∩ t⁰⁰) → r;

I ` S : (t → s → r ) → (t → s) → t → r.

Examples

I ` I : t ∩ s → t;

I ` I : t → t;

I ` 2 : (t → s) ∩ (s → r ) → (t → r );

I ` 2 : (t → t) → t → t;

I ` K : t → s → t;

I ` S : (t⁰ → s → r ) → (t⁰⁰ → s) → (t⁰∩ t⁰⁰) → r;

I ` S : (t → s → r ) → (t → s) → t → r.

Examples

I ` I : t ∩ s → t;

I ` I : t → t;

I ` 2 : (t → s) ∩ (s → r ) → (t → r );

I ` 2 : (t → t) → t → t;

I ` K : t → s → t;

I ` S : (t⁰ → s → r ) → (t⁰⁰ → s) → (t⁰∩ t⁰⁰) → r;

I ` S : (t → s → r ) → (t → s) → t → r.

Examples

I ` I : t ∩ s → t;

I ` I : t → t;

I ` 2 : (t → s) ∩ (s → r ) → (t → r );

I ` 2 : (t → t) → t → t;

I ` K : t → s → t;

I ` S : (t⁰ → s → r ) → (t⁰⁰ → s) → (t⁰∩ t⁰⁰) → r;

I ` S : (t → s → r ) → (t → s) → t → r.

Examples

I ` I : t ∩ s → t;

I ` I : t → t;

I ` 2 : (t → s) ∩ (s → r ) → (t → r );

I ` 2 : (t → t) → t → t;

I ` K : t → s → t;

I ` S : (t⁰ → s → r ) → (t⁰⁰ → s) → (t⁰∩ t⁰⁰) → r;

I ` S : (t → s → r ) → (t → s) → t → r.

Examples

I ` I : t ∩ s → t;

I ` I : t → t;

I ` 2 : (t → s) ∩ (s → r ) → (t → r );

I ` 2 : (t → t) → t → t;

I ` K : t → s → t;

I ` S : (t⁰ → s → r ) → (t⁰⁰ → s) → (t⁰∩ t⁰⁰) → r;

Example

Aksjomat: Γ ` M : ω

...

x : p ` K : p → ω → p x : p ` x : p

x : p ` Kx : ω → p x : p ` Ω : ω

x : p ` Kx Ω : p

Example

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

LetΓ = {y : (p ∩ q → r ) → r , x : p → r ∩ s}.

Γ ` y : (p ∩ q → r ) → r Γ ` y : (p → r ) → r

Γ ` x : p → r ∩ s Γ ` x : p → r Γ ` yx : r

Example

...

` K : (p → q → p) → r → p → q → p

...

` K : p → q → p

` KK : r → p → q → p

Generation (Inversion) Lemma

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

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

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

i(σ_i → τ_i).

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

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

Proof: