Silna normalizacja

Rachunek lambda, lato 2019-20

Wykład 14

5 czerwca 2020

1

Silna normalizacja

Twierdzenie (Jean-Yves Girard, 1972)

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.

3

Girarda metoda kandydatów

Zbiór nasycony (Candidat de reductibilité)

1) X ⊆ SN.

2) JeśliN1, . . . , Nk∈ SN, toxN1. . . Nk∈ X . 3) JeśliM[x := N0]N1. . . Nk∈ X, orazN0∈ SN,

to(λx .M)N0N1. . . Nk∈ X.

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

4

Interpretacja Girarda

Wartościowanie ξ : TV → Gwyznacza interpretację typu:

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

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

[[∀p.σ]]ξ = T

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

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

5

Silna normalizacja (Curry)

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

JeśliNi∈ [[Γ(xi)]]ξ, dlai = 1, . . . , k,

toM[x1:= N1, . . . , xk:= Nk] ∈ [[τ ]]ξ.

Dowód twierdzenia:

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

6

Silna normalizacja (Church)

Jeśli

M = M0→ M1→ M2→ · · · to

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

gdzieoznacza→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.

8

The typability problem

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

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

I 22K.

9

Nierozstrzygalność (1)

Twierdzenie (J.B. Wells, 1993)

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.

11

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→ Nisdefinable in system F iff there is a termF : ω → · · · → ω → ωsuch that

F n1. . . nk=βm iff f (n1, . . . , nk) = m.

12

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ówF n1. . . nk: ωmożna udowodnić w arytmetyce drugiego rzędu.

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

do termu typuω → ω.

14

Data types

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

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

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

15

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

17

Iloczyn. . . kartezjański

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

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

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

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

Beta-reduction works:π1(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

Coproduct

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

Embeddings and cases:

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

I Terminrσ∨τ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

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

21

Jak zdefiniować kwantyfikator szczegółowy

x ∈[

P

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

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

22

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

Higher-order polymorphism

24

Type constructors

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

Because types we can assign toIandKdiffer 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 atype constructor(ortype family):

ifp : Typethenα(p) : Type.

We say that thekindofαisType ⇒ Type.

25

System F

Kinds:

I The constant∗is a kind;

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

Constructors:

I Constructor variables of any kind;

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

I Abstractionsλα^∇1φ^∇2: ∇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 : τ (σ =βτ )

GEN Γ ` M : σ

Γ ` M : ∀α σ α 6∈ FV(Γ)

27

Przykład

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

Jeślixma typ∀p. p → α(p), to ma zarówno typp → α(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)

29

Example

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

30

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 32