Rachunek lambda, lato 2019-20

Rachunek lambda, lato 2019-20

Wykład 14

5 czerwca 2020

1

Silna normalizacja

Twierdzenie (Jean-Yves Girard, 1972)

System F ma własność SN.

Wniosek

Zdaniowa logika intuicjonistyczna drugiego rzędu jest niesprzeczna.

Silna normalizacja

Twierdzenie (Jean-Yves Girard, 1972)

System F ma własność SN.

Wniosek

Zdaniowa logika intuicjonistyczna drugiego rzędu jest niesprzeczna.

2

Silna normalizacja dla typów prostych

Termy stabilne (obliczalne):

I [[p]] := SN;

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

Naiwne uogólnienie:

I [[∀p τ ]] =T{[[τ [p := σ]]] | σ — dowolny typ}.

To nie jest dobrze ufundowana definicja.

Silna normalizacja dla typów prostych

Termy stabilne (obliczalne):

I [[p]] := SN;

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

Naiwne uogólnienie:

I [[∀p τ ]] =T{[[τ [p := σ]]] | σ — dowolny typ}.

To nie jest dobrze ufundowana definicja.

3

Silna normalizacja dla typów prostych

Termy stabilne (obliczalne):

I [[p]] := SN;

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

Naiwne uogólnienie:

I [[∀p τ ]] =T{[[τ [p := σ]]] | σ — dowolny typ}.

To nie jest dobrze ufundowana definicja.

Girarda metoda kandydatów

Zbiór nasycony (Candidat de reductibilité)

to taki zbiór termów (Curry’ego), który ma trzy własności:

1) X ⊆ SN.

2) Jeśli N₁, . . . , N_k ∈ SN, to xN₁. . . N_k ∈ X . 3) Jeśli M[x := N₀]N₁. . . N_k ∈ X, oraz N₀ ∈ SN,

to (λx .M)N₀N₁. . . N_k ∈ X.

G – rodzina wszystkich kandydatów (uwaga: SN ∈ G).

4

Interpretacja Girarda

Wartościowanie ξ : TV → G wyznacza interpretację typu:

[[p]]_ξ = ξ(p);

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

[[∀p.σ]]ξ = T

X ∈G[[σ]]_{ξ(p7→X )}.

Fakt: Zawsze[[τ ]]_ξ ∈ G.

Silna normalizacja (Curry)

Główny lemat: Niech Γ ` M : τ, FV(M) = {x1, . . . , xk}.

JeśliN_i ∈ [[Γ(x_i)]]_ξ, dla i = 1, . . . , k,

to M[x₁ := N₁, . . . , x_k := N_k] ∈ [[τ ]]_ξ.

Dowód twierdzenia:

JeśliΓ ` M : τ, to M ∈ [[τ ]]_ξ, bo x ∈ [[Γ(x )]]_ξ. Teza wynika więc stąd, że[[τ ]]_ξ ⊆ SN.

6

Silna normalizacja (Curry)

Główny lemat: Niech Γ ` M : τ, FV(M) = {x1, . . . , xk}.

JeśliN_i ∈ [[Γ(x_i)]]_ξ, dla i = 1, . . . , k,

to M[x₁ := N₁, . . . , x_k := N_k] ∈ [[τ ]]_ξ.

Dowód twierdzenia:

JeśliΓ ` M : τ, to M ∈ [[τ ]]_ξ, bo x ∈ [[Γ(x )]]_ξ. Teza wynika więc stąd, że[[τ ]]_ξ ⊆ SN.

Silna normalizacja (Church)

Jeśli

M = M₀ → M₁ → M₂ → · · · to

|M| = |M0|  |M1|  |M2|  · · ·

gdzie  oznacza→ lub =.

Liczba wystąpień→ jest skończona, bo mamy SN (Curry).

Liczba wystąpień= też, bo redukcje typowe usuwają Λ.

7

Zła wiadomość

Dowód Girarda nie jest wyrażalny nawet w języku arytmetyki drugiego rzędu.

Jeszcze gorsza wiadomość:

Własność SN dla systemu F jest NIEZALEŻNA od arytmetyki drugiego rzędu.

Zła wiadomość

Dowód Girarda nie jest wyrażalny nawet w języku arytmetyki drugiego rzędu.

Jeszcze gorsza wiadomość:

Własność SN dla systemu F jest NIEZALEŻNA od arytmetyki drugiego rzędu.

8

The typability problem

Examples: The following terms are strongly normalizable, but untypable in systemF:

I (λzy . y (zI)(zK))(λx . xx );

I 22K.

Nierozstrzygalność (1)

Twierdzenie (J.B. Wells, 1993)

Problem typowalności:

Dany term M, czy istnieją takie Γ i τ , że Γ ` M : τ ? i problem sprawdzenia typu:

Dane są Γ, M i τ . Czy Γ ` M : τ ? są dla systemu F nierozstrzygalne.

10

Nierozstrzygalność (2)

Twierdzenie (

Dany typ τ , czy istnieje term zamknięty M typu τ ? jest dla systemu F nierozstrzygalny.

Uwaga: To tyle, co nierozstrzygalność intuicjonistycznej logiki zdaniowej drugiego rzędu.

Dowód: Redukcja logiki 1. rzędu: Formuła ϕjest twierdzeniem logiki 1. rzędu wtedy i tylko wtedy, gdy

jej translacjaϕjest niepustym typem systemu F.

Nierozstrzygalność (2)

Twierdzenie (

Dany typ τ , czy istnieje term zamknięty M typu τ ? jest dla systemu F nierozstrzygalny.

Uwaga: To tyle, co nierozstrzygalność intuicjonistycznej logiki zdaniowej drugiego rzędu.

Dowód: Redukcja logiki 1. rzędu: Formuła ϕjest twierdzeniem logiki 1. rzędu wtedy i tylko wtedy, gdy

jej translacjaϕjest niepustym typem systemu F.

11

Nierozstrzygalność (2)

Twierdzenie (

Dany typ τ , czy istnieje term zamknięty M typu τ ? jest dla systemu F nierozstrzygalny.

Uwaga: To tyle, co nierozstrzygalność intuicjonistycznej logiki zdaniowej drugiego rzędu.

Dowód: Redukcja logiki 1. rzędu:

Formuła ϕjest twierdzeniem logiki 1. rzędu wtedy i tylko wtedy, gdy

jej translacjaϕjest niepustym typem systemu F.

Definability of integer functions

Numerals n = Λpλf^p→pλx^p. f (f (· · · f (x ))) are of type ω = ∀p((p → p) → (p → p)).

A functionf : N^k → N is definable in system F iff there is a termF : ω → · · · → ω → ω such that

F n1. . . n_k =_β m iff f (n1, . . . , n_k) = m.

12

Definability of integer functions

Numerals n = Λpλf^p→pλx^p. f (f (· · · f (x ))) are of type ω = ∀p((p → p) → (p → p)).

A functionf : N^k → N is definable in system F iff there is a termF : ω → · · · → ω → ω such that

F n1. . . n_k =_β m iff f (n1, . . . , n_k) = m.

Examples of representable functions:

I Add = λmn.Λp.λfx.mpf (npfx);

I Mult = λmn.Λp.λfx.mp(npf )x;

I Exp = λmn.Λp.λfx.m(p → p)(np)fx.

13

Siła wyrazu polimorfizmu

Twierdzenie (Girard):

Funkcja jest definiowalna w systemie F wtedy i tylko wtedy, gdy jest dowodliwie rekurencyjna w arytmetyce drugiego rzędu.

Idea dowodu(w uproszczeniu):

(⇒) Silną normalizację dla termów F n₁. . . n_k : ω można udowodnić w arytmetyce drugiego rzędu.

(⇐) Dowód formuły∀n∃m P(n, m) „wyciera się” do termu typu ω → ω.

Siła wyrazu polimorfizmu

Twierdzenie (Girard):

Funkcja jest definiowalna w systemie F wtedy i tylko wtedy, gdy jest dowodliwie rekurencyjna w arytmetyce drugiego rzędu.

Idea dowodu(w uproszczeniu):

(⇒) Silną normalizację dla termów F n₁. . . n_k : ω można udowodnić w arytmetyce drugiego rzędu.

(⇐) Dowód formuły∀n∃m P(n, m) „wyciera się” do termu typu ω → ω.

14

Siła wyrazu polimorfizmu

Twierdzenie (Girard):

Funkcja jest definiowalna w systemie F wtedy i tylko wtedy, gdy jest dowodliwie rekurencyjna w arytmetyce drugiego rzędu.

Idea dowodu(w uproszczeniu):

(⇒) Silną normalizację dla termów F n₁. . . n_k : ω można udowodnić w arytmetyce drugiego rzędu.

(⇐) Dowód formuły∀n∃m P(n, m) „wyciera się”

do termu typu ω → ω.

Data types

Zbiór pusty: x ∈ ∅ ⇔ ∀P(x ∈ P).

Typ pusty (fałsz): ⊥ = ∀p p Ex falso quodlibet:

If Γ ` M : ⊥then Γ ` Mτ : τ.

15

Data types

Zbiór pusty: x ∈ ∅ ⇔ ∀P(x ∈ P).

Typ pusty (fałsz): ⊥ = ∀p p Ex falso quodlibet:

If Γ ` M : ⊥then Γ ` Mτ : τ.

Suma/alternatywa

x ∈ A ∪ B ⇔ ∀P(A ⊆ P → B ⊆ P → x ∈ P),

A(x )∨B(x ) ⇔ ∀P(∀y (A(y )→P(y )) → ∀y (B(y )→P(y ))→P(x )).

A ∨ B = ∀p((A → p) → (B → p) → p).

16

Suma/alternatywa

x ∈ A ∪ B ⇔ ∀P(A ⊆ P → B ⊆ P → x ∈ P),

A(x )∨B(x ) ⇔ ∀P(∀y (A(y )→P(y )) → ∀y (B(y )→P(y ))→P(x )).

A ∨ B = ∀p((A → p) → (B → p) → p).

Suma/alternatywa

x ∈ A ∪ B ⇔ ∀P(A ⊆ P → B ⊆ P → x ∈ P),

A(x )∨B(x ) ⇔ ∀P(∀y (A(y )→P(y )) → ∀y (B(y )→P(y ))→P(x )).

A ∨ B = ∀p((A → p) → (B → p) → p).

16

Iloczyn/koniunkcja

x ∈ A ∩ B ⇔ ∀P(∀z(z ∈ A → z ∈ B → z ∈ P) → x ∈ P).

A ∧ B = ∀p((A → B → p) → p).

Iloczyn/koniunkcja

x ∈ A ∩ B ⇔ ∀P(∀z(z ∈ A → z ∈ B → z ∈ P) → x ∈ P).

A ∧ B = ∀p((A → B → p) → p).

17

Iloczyn. . . kartezjański

σ ∧ τ = ∀p((σ → τ → p) → p)

Pairs and projections:

I Term hM^σ, N^τi = Λpλy^{σ→τ →p}.yMN has type σ ∧ τ.

I Term π₁(P^σ∧τ) = Pσ(λx^σλy^τ.x ); has type σ.

I Term π₂(P^σ∧τ) = Pτ (λx^σλy^τ.y ). has type τ.

Beta-reduction works: π₁(hM, Ni)  M, because

(Λpλy^{σ→τ →p}.yMN)σ(λx^σλy^τ.x )  (λx^σλy^τ.x )MN  M. Eta-reduction does not work:

hπ1(P), π2(P)i = Λpλy .y (π1(P))(π2(P)) 6 P

Iloczyn. . . kartezjański

σ ∧ τ = ∀p((σ → τ → p) → p) Pairs and projections:

I Term hM^σ, N^τi = Λpλy^{σ→τ →p}.yMN has type σ ∧ τ.

I Term π₁(P^σ∧τ) = Pσ(λx^σλy^τ.x ); has type σ.

I Term π₂(P^σ∧τ) = Pτ (λx^σλy^τ.y ). has type τ.

Beta-reduction works: π₁(hM, Ni)  M, because

(Λpλy^{σ→τ →p}.yMN)σ(λx^σλy^τ.x )  (λx^σλy^τ.x )MN  M. Eta-reduction does not work:

hπ1(P), π2(P)i = Λpλy .y (π1(P))(π2(P)) 6 P

18

Iloczyn. . . kartezjański

σ ∧ τ = ∀p((σ → τ → p) → p) Pairs and projections:

I Term hM^σ, N^τi = Λpλy^{σ→τ →p}.yMN has type σ ∧ τ.

I Term π₁(P^σ∧τ) = Pσ(λx^σλy^τ.x ); has type σ.

I Term π₂(P^σ∧τ) = Pτ (λx^σλy^τ.y ). has type τ.

Beta-reduction works: π₁(hM, Ni)  M, because

(Λpλy^{σ→τ →p}.yMN)σ(λx^σλy^τ.x )  (λx^σλy^τ.x )MN  M. Eta-reduction does not work:

hπ1(P), π2(P)i = Λpλy .y (π1(P))(π2(P)) 6 P

Iloczyn. . . kartezjański

σ ∧ τ = ∀p((σ → τ → p) → p) Pairs and projections:

I Term hM^σ, N^τi = Λpλy^{σ→τ →p}.yMN has type σ ∧ τ.

I Term π₁(P^σ∧τ) = Pσ(λx^σλy^τ.x ); has type σ.

I Term π₂(P^σ∧τ) = Pτ (λx^σλy^τ.y ). has type τ.

Beta-reduction works: π₁(hM, Ni)  M, because

(Λpλy^{σ→τ →p}.yMN)σ(λx^σλy^τ.x )  (λx^σλy^τ.x )MN  M.

Eta-reduction does not work:

hπ1(P), π2(P)i = Λpλy .y (π1(P))(π2(P)) 6 P

18

Iloczyn. . . kartezjański

σ ∧ τ = ∀p((σ → τ → p) → p) Pairs and projections:

I Term hM^σ, N^τi = Λpλy^{σ→τ →p}.yMN has type σ ∧ τ.

I Term π₁(P^σ∧τ) = Pσ(λx^σλy^τ.x ); has type σ.

I Term π₂(P^σ∧τ) = Pτ (λx^σλy^τ.y ). has type τ.

Beta-reduction works: π₁(hM, Ni)  M, because

(Λpλy^{σ→τ →p}.yMN)σ(λx^σλy^τ.x )  (λx^σλy^τ.x )MN  M. Eta-reduction does not work:

hπ (P), π (P)i = Λpλy .y (π (P))(π (P)) 6 P

Coproduct

σ ∨ τ = ∀p((σ → p) → (τ → p) → p)

Embeddings and cases:

I Term inlσ∨τL^σ = Λpλu^σ→pλv^{τ →p}.uL has type σ ∨ τ.

I Term inr_σ∨τR^τ = Λpλu^σ→pλv^{τ →p}.vR has type σ ∨ τ.

I Andcase M of [x]P^ϑ, [y ]Q^ϑ= Mϑ(λx^σP)(λy^τQ) : ϑ.

Beta-reduction:

case inl(L) of [x]P, [y ]Q = (inl(L))ϑ(λx^σP)(λy^τQ) = (Λpλuv .uL)ϑ(λx^σP)(λy^τQ)  (λx^σP)L  P[x := L].

19

Coproduct

σ ∨ τ = ∀p((σ → p) → (τ → p) → p)

Embeddings and cases:

I Term inlσ∨τL^σ = Λpλu^σ→pλv^{τ →p}.uL has type σ ∨ τ.

I Term inr_σ∨τR^τ = Λpλu^σ→pλv^{τ →p}.vR has type σ ∨ τ.

I Andcase M of [x]P^ϑ, [y ]Q^ϑ= Mϑ(λx^σP)(λy^τQ) : ϑ.

Beta-reduction:

case inl(L) of [x]P, [y ]Q = (inl(L))ϑ(λx^σP)(λy^τQ) = (Λpλuv .uL)ϑ(λx^σP)(λy^τQ)  (λx^σP)L  P[x := L].

Abstract (encapsulated) type

Idea: Type∃p σ(p) is of shape σ(τ ), where τ is unspecified (abstract) and not accesible to the user.

Example: An abstract pds object is of type

∃p (p × p × (p → p) × (p → ω) × (ω × p → p))

20

Existential types

Type assignment:

(pack) Γ ` M : σ[p := τ ] Γ ` pack M, τ to ∃p. σ : ∃p. σ

(unpack) Γ ` M : ∃p. σ Γ(x : σ) ` N : ρ

Γ ` let M be x , p in N : ρ (p 6∈ FV (Γ, ρ))

Beta reduction:

let (pack M, τ to ∃p. σ) be x, p in N −→β N[p := τ ][x := M].

Jak zdefiniować kwantyfikator szczegółowy

x ∈[

P

SP ⇔ ∀Q(∀P(SP ⊆ Q) → x ∈ Q)

∃p σ = ∀q(∀p(σ → q) → q).

22

Jak zdefiniować kwantyfikator szczegółowy

x ∈[

P

SP ⇔ ∀Q(∀P(SP ⊆ Q) → x ∈ Q)

∃p σ = ∀q(∀p(σ → q) → q).

Implementing existential quantifier

Definitions:

I ∃p σ = ∀q(∀p(σ → q) → q).

I pack M^{σ[p:=τ ]}, τ to ∃p. σ = Λqλz^∀p(σ→q).zτ M;

I let M^{∃p. σ} be x, p in N^ρ = Mρ(Λpλx^σ.N). Correctness:

let (pack M, τ to ∃p. σ) be x, p in N^ρ

= (Λqλz^∀p(σ→q). zτ M)ρ(Λpλx^σ.N)

→ (λz^{∀p(σ→ρ)}. zτ M)(Λpλx^σ.N)

→ (Λpλx^σ.N)τ M

 N[p := τ ][x := M].

23

Implementing existential quantifier

Definitions:

I ∃p σ = ∀q(∀p(σ → q) → q).

I pack M^{σ[p:=τ ]}, τ to ∃p. σ = Λqλz^∀p(σ→q).zτ M;

I let M^{∃p. σ} be x, p in N^ρ = Mρ(Λpλx^σ.N). Correctness:

let (pack M, τ to ∃p. σ) be x, p in N^ρ

= (Λqλz^∀p(σ→q). zτ M)ρ(Λpλx^σ.N)

→ (λz^{∀p(σ→ρ)}. zτ M)(Λpλx^σ.N)

→ (Λpλx^σ.N)τ M

 N[p := τ ][x := M].

Implementing existential quantifier

Definitions:

I ∃p σ = ∀q(∀p(σ → q) → q).

I pack M^{σ[p:=τ ]}, τ to ∃p. σ = Λqλz^∀p(σ→q).zτ M;

I let M^{∃p. σ} be x, p in N^ρ = Mρ(Λpλx^σ.N).

Correctness:

let (pack M, τ to ∃p. σ) be x, p in N^ρ

= (Λqλz^∀p(σ→q). zτ M)ρ(Λpλx^σ.N)

→ (λz^{∀p(σ→ρ)}. zτ M)(Λpλx^σ.N)

→ (Λpλx^σ.N)τ M

 N[p := τ ][x := M].

23

Implementing existential quantifier

Definitions:

I ∃p σ = ∀q(∀p(σ → q) → q).

I pack M^{σ[p:=τ ]}, τ to ∃p. σ = Λqλz^∀p(σ→q).zτ M;

I let M^{∃p. σ} be x, p in N^ρ = Mρ(Λpλx^σ.N).

Correctness:

let (pack M, τ to ∃p. σ) be x, p in N^ρ

= (Λqλz^∀p(σ→q). zτ M)ρ(Λpλx^σ.N)

→ (λz^{∀p(σ→ρ)}. zτ M)(Λpλx^σ.N)

→ (Λpλx^σ.N)τ M

 N[p := τ ][x := M].

Implementing existential quantifier

Definitions:

I ∃p σ = ∀q(∀p(σ → q) → q).

I pack M^{σ[p:=τ ]}, τ to ∃p. σ = Λqλz^∀p(σ→q).zτ M;

I let M^{∃p. σ} be x, p in N^ρ = Mρ(Λpλx^σ.N).

Correctness:

let (pack M, τ to ∃p. σ) be x, p in N^ρ

= (Λqλz^∀p(σ→q). zτ M)ρ(Λpλx^σ.N)

→ (λz^{∀p(σ→ρ)}. zτ M)(Λpλx^σ.N)

→ (Λpλx^σ.N)τ M

 N[p := τ ][x := M].

23

Implementing existential quantifier

Definitions:

I ∃p σ = ∀q(∀p(σ → q) → q).

I pack M^{σ[p:=τ ]}, τ to ∃p. σ = Λqλz^∀p(σ→q).zτ M;

I let M^{∃p. σ} be x, p in N^ρ = Mρ(Λpλx^σ.N).

Correctness:

let (pack M, τ to ∃p. σ) be x, p in N^ρ

= (Λqλz^∀p(σ→q). zτ M)ρ(Λpλx^σ.N)

→ (λz^{∀p(σ→ρ)}. zτ M)(Λpλx^σ.N)

→ (Λpλx^σ.N)τ M

 N[p := τ ][x := M].

Implementing existential quantifier

Definitions:

I ∃p σ = ∀q(∀p(σ → q) → q).

I pack M^{σ[p:=τ ]}, τ to ∃p. σ = Λqλz^∀p(σ→q).zτ M;

I let M^{∃p. σ} be x, p in N^ρ = Mρ(Λpλx^σ.N).

Correctness:

let (pack M, τ to ∃p. σ) be x, p in N^ρ

= (Λqλz^∀p(σ→q). zτ M)ρ(Λpλx^σ.N)

→ (λz^{∀p(σ→ρ)}. zτ M)(Λpλx^σ.N)

→ (Λpλx^σ.N)τ M

 N[p := τ ][x := M].

23

Implementing existential quantifier

Definitions:

I ∃p σ = ∀q(∀p(σ → q) → q).

I pack M^{σ[p:=τ ]}, τ to ∃p. σ = Λqλz^∀p(σ→q).zτ M;

I let M^{∃p. σ} be x, p in N^ρ = Mρ(Λpλx^σ.N).

Correctness:

let (pack M, τ to ∃p. σ) be x, p in N^ρ

= (Λqλz^∀p(σ→q). zτ M)ρ(Λpλx^σ.N)

→ (λz^{∀p(σ→ρ)}. zτ M)(Λpλx^σ.N)

→ (Λpλx^σ.N)τ M

 N[p := τ ][x := M].

Higher-order polymorphism

24

Type constructors

Example: Why is (λzy . y (zI)(zK))(λx . xx ) untypable in F?

Because types we can assign toI and Kdiffer too much:

I : ∀p. p → p K :∀p. p → (q → p).

There is no common pattern for these two types,. . .

unless we write it this way:

I, K : ∀p. p → α(p).

Here,α is a type constructor (or type family): if p : Type then α(p) : Type.

We say that the kind of α is Type ⇒ Type.

Type constructors

Example: Why is (λzy . y (zI)(zK))(λx . xx ) untypable in F?

Because types we can assign toI and Kdiffer too much:

I : ∀p. p → p K :∀p. p → (q → p).

There is no common pattern for these two types,. . . unless we write it this way:

I, K : ∀p. p → α(p).

Here,α is a type constructor (or type family): if p : Type then α(p) : Type.

We say that the kind of α is Type ⇒ Type.

25

Type constructors

Example: Why is (λzy . y (zI)(zK))(λx . xx ) untypable in F?

Because types we can assign toI and Kdiffer too much:

I : ∀p. p → p K :∀p. p → (q → p).

There is no common pattern for these two types,. . . unless we write it this way:

I, K : ∀p. p → α(p).

Here,α is a type constructor (or type family):

if p : Type then α(p) : Type.

We say that the kind of α is Type ⇒ Type.

System F

Kinds:

I The constant ∗is a kind;

I If ∇1 and ∇2 are kinds then∇1 ⇒ ∇2 is a kind.

Constructors:

I Constructor variables of any kind;

I Applications ϕ^∇1⇒∇2ψ^∇1 : ∇₂;

I Abstractionsλα^∇1φ^∇2 : ∇₁ ⇒ ∇₂;

I Function types τ^∗ → σ^∗ : ∗;

I Polymorphic types ∀α^∇τ^∗ : ∗.

Constructor reduction: (λα σ)τ −→β σ[α := τ ].

26

Type assignment F

VAR Γ ` x : σ when Γ(x ) = σ

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

Γ ` (M N) : τ

ABS Γ(x : σ) ` M : τ

Γ ` (λx M) : σ → τ

INST Γ ` M : ∀α σ

Γ ` M : σ[α := τ ]

CONV Γ ` M : σ

Γ ` M : τ (σ =<sub>β</sub> τ ) Γ ` M : σ

Przykład

Typowanie dla termu (λzy . y (zI)(zK))(λx . xx ):

Jeślix ma typ ∀p. p → α(p), to ma zarówno typ p → α(p), jak i typ (p → α(p)) → α(p → α(p)).

Zatem λx . xx : ∀α [(∀p. p → α(p)) → α(p → α(p))]. To jest typ zmiennejz, który „pasuje” do obu argumentów

I : ∀p. p → p K :∀p. p → (q → p).

28

Przykład

Typowanie dla termu (λzy . y (zI)(zK))(λx . xx ):

Jeślix ma typ ∀p. p → α(p), to ma zarówno typ p → α(p), jak i typ (p → α(p)) → α(p → α(p)).

Zatem λx . xx : ∀α [(∀p. p → α(p)) → α(p → α(p))]. To jest typ zmiennejz, który „pasuje” do obu argumentów

I : ∀p. p → p K :∀p. p → (q → p).

Przykład

Typowanie dla termu (λzy . y (zI)(zK))(λx . xx ):

Jeślix ma typ ∀p. p → α(p), to ma zarówno typ p → α(p), jak i typ (p → α(p)) → α(p → α(p)).

Zatem λx . xx : ∀α [(∀p. p → α(p)) → α(p → α(p))].

To jest typ zmiennejz, który „pasuje” do obu argumentów I : ∀p. p → p K :∀p. p → (q → p).

28

Example

Letα : ∗ ⇒ ∗, ϕ : (∗ ⇒ ∗) ⇒ (∗ ⇒ ∗). Then:

K : ∀p (p → q → p)

2 : ∀α (∀p (p → α(p)) → ∀p (p → α(α(p)))) 2 : [∀α (∀p (p → α(p)) → ∀p (p → (α(α(p))))] →

[∀α (∀p (p → α(p)) → ∀p (p → (α(α(α(α(p)))))))]

Therefore 22K : ∀p (p → q → q → q → q → p)

2 : ∀ϕ([∀α (∀p (p → α(p)) → ∀p (p → ϕ(α)(p)] → [∀α (∀p (p → α(p)) → ∀p (p → (ϕ(ϕ(α))(p))))] Therefore222K : ∀p (p → q → q → · · · → q → q → p)

Example

Letα : ∗ ⇒ ∗, ϕ : (∗ ⇒ ∗) ⇒ (∗ ⇒ ∗). Then:

K : ∀p (p → q → p)

2 : ∀α (∀p (p → α(p)) → ∀p (p → α(α(p)))) 2 : [∀α (∀p (p → α(p)) → ∀p (p → (α(α(p))))] →

[∀α (∀p (p → α(p)) → ∀p (p → (α(α(α(α(p)))))))]

Therefore 22K : ∀p (p → q → q → q → q → p) 2 : ∀ϕ([∀α (∀p (p → α(p)) → ∀p (p → ϕ(α)(p)] →

[∀α (∀p (p → α(p)) → ∀p (p → (ϕ(ϕ(α))(p))))]

Therefore222K : ∀p (p → q → q → · · · → q → q → p)

29

Example

Let1 = λfu. fu and 1⁰ = λvg . gv. The term (λx . z(x 1)(x 1⁰))(λy . yyy ) is strongly normalizable, but untypable in F_ω

Properties of F

I Every typable term is strongly normalizing.

I Type-checking and typability problems are undecidable.

I The inhabitation problem is undecidable.

31

Properties of F

I Every typable term is strongly normalizing.

I Type-checking and typability problems are undecidable.

I The inhabitation problem is undecidable.

Properties of F

I Every typable term is strongly normalizing.

I Type-checking and typability problems are undecidable.

I The inhabitation problem is undecidable.

31