Rachunek lambda, lato 2019-20

(1)

Rachunek lambda, lato 2019-20

Wykład 13

29 maja 2020

(2)

Logika pierwszego i drugiego rzędu

Symbole relacyjne: wyrażenia P(x ), Q(t, v ), itp.

są formułami atomowymi. Ich argumentami są zmienne lub termy „indywiduowe” lub „przedmiotowe”.

Kwantyfikatory: zmiennax jest związana w formułach∀x ϕ(x), ∃x ϕ(x).

Logika pierwszego rzędu: kwantyfikatory wiążą tylko zmienne indywiduowe. Symbole relacyjne są stałe.

Logika drugiego rzędu: kwantyfikatory mogą wiązać zmienne relacyjne.

(3)

Typy zależne (Dependent types)

P(a₁, . . . , a_n) — a type thatdepends on the choice of individual valuesa1, . . . ,an.

Na przykład:

M : array(n) M jest tablicą rozmiaru n; array : Int → „Typ” array jest konstruktorem typu (rodziną typów )

(4)

Typy zależne (Dependent types)

Na przykład:

M : array(n) M jest tablicą rozmiarun;

array : Int → „Typ” array jest konstruktorem typu (rodziną typów )

(5)

Typy zależne (Dependent types)

Na przykład:

M : array(n) M jest tablicą rozmiarun;

array : Int → „Typ” array jest konstruktorem typu (rodziną typów )

(6)

Wycieranie zależności

Aksjomat indukcji:

∀n (P(n) → P(n + 1)) → P(0) → ∀n P(n).

Jeśli usuniemy z niego wszystko to, co odnosi się do indywiduów (kwantyfikatory i argumenty relacjiP), to otrzymamy taką formułę zdaniową (typ prosty): (P → P) → P → P.

(7)

Wycieranie zależności

Aksjomat indukcji:

∀n (P(n) → P(n + 1)) → P(0) → ∀n P(n).

Jeśli usuniemy z niego wszystko to, co odnosi się do indywiduów (kwantyfikatory i argumenty relacjiP),

to otrzymamy taką formułę zdaniową (typ prosty): (P → P) → P → P.

(8)

Wycieranie zależności

Aksjomat indukcji:

∀n (P(n) → P(n + 1)) → P(0) → ∀n P(n).

Jeśli usuniemy z niego wszystko to, co odnosi się do indywiduów (kwantyfikatory i argumenty relacjiP), to otrzymamy taką formułę zdaniową (typ prosty):

(P → P) → P → P.

(9)

Polimorfizm

(10)

(Klasyczna) logika drugiego rzędu

Składnia: Zmienne relacyjne i kwantyfikatory ∀R, ∃R.

Przykład formuły: ∀P(P(x) → Q(x)) → Q(x)

Semantyka w stylu Tarskiego: Interpretujemy zmienne relacyjne jako relacje. Na przykład formuła

Nat(x) = ∀R(∀y (R(y ) → R(s y )) → R(0) → R(x)) definiuje standardowe liczby naturalne.

Wniosek: Aksjomaty Peana plus ∀xNat(x) definiują standardowy model arytmetyki z dokładnością do izomorfizmu. Wniosek: Zbiór tautologii drugiego rzędu nie jest

rekurencyjnie przeliczalny (bo Th(N) nie jest). Wniosek: Nie ma pełnego systemu wnioskowania.

(11)

(Klasyczna) logika drugiego rzędu

Wniosek: Aksjomaty Peana plus ∀xNat(x) definiują standardowy model arytmetyki z dokładnością do izomorfizmu. Wniosek: Zbiór tautologii drugiego rzędu nie jest

rekurencyjnie przeliczalny (bo Th(N) nie jest). Wniosek: Nie ma pełnego systemu wnioskowania.

(12)

(Klasyczna) logika drugiego rzędu

Wniosek: Aksjomaty Peana plus ∀xNat(x) definiują standardowy model arytmetyki z dokładnością do izomorfizmu.

Wniosek: Zbiór tautologii drugiego rzędu nie jest rekurencyjnie przeliczalny (bo Th(N) nie jest). Wniosek: Nie ma pełnego systemu wnioskowania.

(13)

(Klasyczna) logika drugiego rzędu

Wniosek: Zbiór tautologii drugiego rzędu nie jest rekurencyjnie przeliczalny (bo Th(N) nie jest).

Wniosek: Nie ma pełnego systemu wnioskowania.

(14)

(Klasyczna) logika drugiego rzędu

Wniosek: Zbiór tautologii drugiego rzędu nie jest rekurencyjnie przeliczalny (bo Th(N) nie jest).

Wniosek: Nie ma pełnego systemu wnioskowania.

(15)

Logika drugiego rzędu

Two ways to understand the quantifier∀P:

1. Tarski: the variableP ranges over unary relations (subsets of a domain).

2. Henkin: The variable P ranges over definable predicates.

The set of tautologies wrt (1) is not recursively enumerable. There is no complete proof system.

We think in terms of (2).

(16)

Logika drugiego rzędu

Przykład formuły: ∀P(P(x) → Q(x)) → Q(x) Two ways to understand the quantifier∀P:

(17)

Logika drugiego rzędu

(18)

Logika drugiego rzędu

The set of tautologies wrt (1) is not recursively enumerable.

There is no complete proof system.

(19)

Logika drugiego rzędu

The set of tautologies wrt (1) is not recursively enumerable.

There is no complete proof system.

(20)

Logika drugiego rzędu w stylu Henkina

Semantyka (nieformalna): Interpretujemy zmienne relacyjne jako definiowalne predykaty.

To ma sens klasycznie i intuicjonistycznie.

Reguły wnioskowania:

X ton-arna zmienna relacyjna, σ to „formuła zn argumentami”.

Γ ` ∀X ϕ(X ) Γ ` ϕ(σ)

Γ ` ϕ(X ) Γ ` ∀X ϕ(X )

(X 6∈FV(Γ))

Γ ` ϕ(σ) Γ ` ∃X ϕ(X )

Γ ` ∃X ϕ(X ), Γ, ϕ(X ) ` ψ Γ ` ψ

(X 6∈FV(Γ, ψ))

(21)

“Dependency erasure”

Example 1: ∀P(P(x) → Q(x)) → Q(x)

This is the same principle as ∀p(p → q) → q. Example 2: Definition of natural numbers:

Nat(n) : ∀R(∀x(R(x) → R(sx)) → R(0) → R(n)) Jak można udowodnić formułęNat(5 )?

Deleting first-order layer: ∀r ((r → r ) → r → r ).

(22)

“Dependency erasure”

Example 1: ∀P(P(x) → Q(x)) → Q(x) This is the same principle as ∀p(p → q) → q.

Example 2: Definition of natural numbers:

(23)

“Dependency erasure”

Nat(n) : ∀R(∀x(R(x) → R(sx)) → R(0) → R(n))

Jak można udowodnić formułęNat(5 )?

(24)

“Dependency erasure”

(25)

“Dependency erasure”

(26)

Second-order propositional logic

(Ax) Γ, ϕ ` ϕ

(→ I) Γ, ϕ ` ψ Γ ` ϕ → ψ

(→ E) Γ ` ϕ → ψ Γ ` ϕ Γ ` ψ

(∀I) Γ ` ϕ Γ ` ∀p ϕ

(p 6∈ FV(Γ)) (∀E) Γ ` ∀p ϕ Γ ` ϕ[p := ϑ]

(∃I) Γ ` ϕ[p := ϑ]

Γ ` ∃p ϕ

(∃E) Γ ` ∃p ϕ, Γ, ϕ ` ψ Γ ` ψ

(p 6∈ FV(Γ, ψ))

(27)

Two educated cliches

I Full comprehension: Propositional variables range over all formulas:

∃p (ϕ ↔ p)

∀p ϕ(p) → ϕ(ψ)

The meaning ofp in ∀p ϕ can be ∀p ϕ itself.

I Impredicativity: The meaning of∀p ϕ is defined by a reference to a domain to which∀p ϕ itself belongs.

(28)

Two educated cliches

∃p (ϕ ↔ p)

∀p ϕ(p) → ϕ(ψ)

(29)

Two educated cliches

∃p (ϕ ↔ p)

∀p ϕ(p) → ϕ(ψ)

(30)

Comparison with classical logic

I Validity/provability in classical propositional logic is complete in the complexity class. . .

co-NP.

I Provability in intuitionistic propositional logic isPSPACE-complete.

I Validity/provability in second-order classical propositional logic (known as the QBF problem) is PSPACE-complete.

I Provability in second-order intuitionistic propositional logic is undecidable.

(31)

Comparison with classical logic

I Validity/provability in classical propositional logic is complete in the complexity class. . .co-NP.

(32)

Comparison with classical logic

(33)

Comparison with classical logic

(34)

Comparison with classical logic

(35)

Polymorphic types

I Basic idea: ∀p. p → p is a type of a generic identity.

I Church style (explicit polymorphism):

I Generic identityI admits a type argument.

I The application Iτ is of typeτ → τ.

I Curry style (implicit polymorphism):

I Generic identityI has all typesτ → τ at once.

(36)

Polymorphic types

(37)

Polymorphic types

(38)

Polymorphic types

(39)

Girard’s System F (Church style)

Γ(x : ϕ) ` x : ϕ

Γ(x : ϕ) ` M : ψ Γ ` (λx :ϕ M) : ϕ → ψ

Γ ` M : ϕ → ψ Γ ` N : ϕ Γ ` (MN) : ψ

Γ ` M : ϕ Γ ` (Λp M) : ∀p ϕ

(p 6∈FV(Γ)) Γ ` M : ∀p ϕ Γ ` Mϑ : ϕ[p := ϑ]

(40)

Girard’s System F (Church style)

Γ(x :ϕ) ` x : ϕ

Γ(x :ϕ) ` M :ψ Γ ` (λx:ϕ M) :ϕ → ψ

Γ ` M :ϕ → ψ Γ ` N :ϕ Γ ` (MN) :ψ

Γ ` M :ϕ

Γ ` (Λp M) :∀p ϕ (p 6∈FV(Γ)) Γ` M :∀p ϕ Γ ` Mϑ :ϕ[p := ϑ]

(41)

Reduction rules

Beta:

I (λx :τ.M)N =⇒_β M[x := N];

I (Λp. M)τ =⇒_β M[p := τ ],

Eta:

I λx :τ.Mx =⇒_η M (x 6∈ FV(M));

I Λp.M p =⇒_η M (p 6∈ FV(M)). Subject reduction:

If Γ ` M : τ and M βη N then Γ ` N : τ

(42)

Reduction rules

Beta:

I (λx :τ.M)N =⇒_β M[x := N];

I (Λp. M)τ =⇒_β M[p := τ ], Eta:

I λx :τ.Mx =⇒_η M (x 6∈ FV(M));

I Λp.M p =⇒_η M (p 6∈ FV(M)).

Subject reduction:

(43)

Reduction rules

Beta:

I (λx :τ.M)N =⇒_β M[x := N];

I (Λp. M)τ =⇒_β M[p := τ ], Eta:

I λx :τ.Mx =⇒_η M (x 6∈ FV(M));

I Λp.M p =⇒_η M (p 6∈ FV(M)).

Subject reduction:

(44)

A few examples

^(zamiastλx :τ piszemy λx^τ)

I Term Λqλx^∀p(p→p).x (q → q)(xq)

has type ∀q(∀p(p → p) → q → q);

I Term 2 = Λp.λf^p→pλx^p.f (fx )

has type ∀p((p → p) → (p → p));

I Term λf^{∀p(p→q→p)}Λpλx^p.f (q→p)(fpx )

has type ∀p(p → q → p) → ∀p(p → q → q → p).

(45)

A few examples

has type ∀p((p → p) → (p → p));

(46)

A few examples

has type ∀p((p → p) → (p → p));

(47)

Wycieranie typów

|x| = x

|MN| = |M||N|

|λx:σ. M| = λx. |M|

|Λp. M| = |M|

|Mτ | = |M|

(48)

Girard’s System F (Church style)

Γ(x : ϕ) ` x : ϕ

Γ(x : ϕ) ` M : ψ Γ ` (λx :ϕ M) : ϕ → ψ

Γ ` M : ϕ → ψ Γ ` N : ϕ Γ ` (MN) : ψ

Γ ` M : ϕ Γ ` (Λp M) : ∀p ϕ

(p 6∈FV(Γ)) Γ ` M : ∀p ϕ Γ ` Mϑ : ϕ[p := ϑ]

(49)

System F w stylu Curry’ego

Γ(x : τ ) ` x : τ

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

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

Γ ` M : σ

Γ ` M : ∀p σ (p 6∈ FV(Γ)) Γ ` M : ∀p σ Γ ` M : σ[p := τ ]

(50)

Wycieranie redukcji

(λx :τ.M)N =⇒_β M[x := N];

(λx . |M|)|N| =⇒_β |M|[x := |N|] = |M[x := N]|

(Λp. M)τ =⇒_β M[p := τ ],

|M| = |M|

λx :τ.Mx =⇒_η M;

λx . |M|x =⇒η |M|

Λp.M p =⇒_η M;

|M| = |M|

(51)

Wycieranie redukcji

(λx :τ.M)N =⇒_β M[x := N];

(λx . |M|)|N| =⇒_β |M|[x := |N|] = |M[x := N]|

(Λp. M)τ =⇒_β M[p := τ ],

|M| = |M|

λx . |M|x =⇒η |M|

Λp.M p =⇒_η M;

|M| = |M|

(52)

Wycieranie redukcji

(λx :τ.M)N =⇒_β M[x := N];

(λx . |M|)|N| =⇒_β |M|[x := |N|] = |M[x := N]|

(Λp. M)τ =⇒_β M[p := τ ],

|M| = |M|

λx . |M|x =⇒η |M|

Λp.M p =⇒_η M;

|M| = |M|

(53)

Wycieranie redukcji

(λx :τ.M)N =⇒_β M[x := N];

(λx . |M|)|N| =⇒_β |M|[x := |N|] = |M[x := N]|

(Λp. M)τ =⇒_β M[p := τ ],

|M| = |M|

λx :τ.Mx =⇒_η M; λx . |M|x =⇒η |M|

Λp.M p =⇒_η M;

|M| = |M|

(54)

Wycieranie redukcji

(λx :τ.M)N =⇒_β M[x := N];

(λx . |M|)|N| =⇒_β |M|[x := |N|] = |M[x := N]|

(Λp. M)τ =⇒_β M[p := τ ],

|M| = |M|

λx :τ.Mx =⇒_η M; λx . |M|x =⇒η |M|

Λp.M p =⇒_η M;

|M| = |M|

(55)

Properties of type erasure

(Church is blue, Curry is red.) 1. If Γ ` M : τ then Γ ` |M| : τ. 2. If Γ ` M : τ then there existsM

such that |M| = M oraz Γ ` M : τ. 3. If M ^β N then |M| ^β |N|.

4. If |M| →_β N then there existsN such that |N| = N and M →β N.

Uwaga:

Tym razem część 4 nie jest oczywista, a w części 3 jest tylko , a nie →.

(56)

Poprawność redukcji (Curry)

Twierdzenie:

JeśliΓ ` M : τ, oraz M →_β M⁰ to Γ ` M⁰ : τ.

Dowód: Nie jest oczywisty.

(57)

Poprawność redukcji (Curry)

Twierdzenie:

JeśliΓ ` M : τ, oraz M →_β M⁰ to Γ ` M⁰ : τ. Dowód: Nie jest oczywisty.

(58)

Generation lemma

Write σ τ whenσ = ∀~p σ⁰ and τ = ∀~q.σ⁰[~p := ~%], whereσ⁰ 6= ∀ . . ., and ~q are not free in σ.

Na przykład∀p. p → r ∀q. (q → r ) → r.

Generation lemma:

1. If Γ ` x : τ then Γ(x ) τ.

2. If Γ ` MN : τ then Γ ` M : % → σ and Γ ` N : %, for some %, σ, with ∀~p σ τ, where p =~ FV(σ) −FV(Γ). 3. If Γ ` λx M : τ then τ = ∀~p(% → σ),

whereΓ(x :%) ` M : σ and p~ are not free in Γ.

(59)

Generation lemma

Write σ τ whenσ = ∀~p σ⁰ and τ = ∀~q.σ⁰[~p := ~%], whereσ⁰ 6= ∀ . . ., and ~q are not free in σ.

Na przykład∀p. p → r ∀q. (q → r ) → r. Generation lemma:

1. If Γ ` x : τ then Γ(x ) τ.

2. If Γ ` MN : τ then Γ ` M : % → σ and Γ ` N : %, for some %,σ, with ∀~p σ τ, where p =~ FV(σ) −FV(Γ).

3. If Γ ` λx M : τ then τ = ∀~p(% → σ),

whereΓ(x :%) ` M : σ and p~ are not free in Γ.

(60)

Subject reduction

Lemma:

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

2. If Γ ` (λx M)N : σ then Γ ` M[x := N] : σ.

Proof: (1) Induction. (2) By (1) and generation lemma.

Corollary (subject reduction):

If Γ ` M : σ and M ^β N then Γ ` N : σ.

(61)

Subject reduction. . .

fails for η

Example:

x : p → ∀q (q → q) ` λy . xy : p → q → q. x : p → ∀q (q → q) 6` x : p → q → q.

26

(62)

Subject reduction. . . fails for η

Example:

x : p → ∀q (q → q) ` λy . xy : p → q → q.

x : p → ∀q (q → q) 6` x : p → q → q.