Wykład 14. Rachunek λ z typami prostymi
Zdzisław Spławski
Dedukcja naturalna dla rachunku zdań
Rachunek lambda z typami prostymi λ→
Izomorfizm Curry’ego-Howarda
Rachunek lambda z typami prostymi λ→∧∨⊥¬
Przykłady dla λ→∧∨⊥¬
Własności rachunku lambda z typami prostymi
I H.P.Barendregt, Lambda Calculi with Types, w:
S.Abramsky, Dov M. Gabbay, T.S.E. Maibaum, Handbook of Logic in Computer Science, vol. 2, Clarendon Press, Oxford 1992, pp. 117-309,
http://www.cs.ru.nl/˜henk/papers.html
I M.Felleisen, M.Flatt, Programming Languages and Lambda Calculi, draft 2006,
http://www.cs.utah.edu/plt/publications/pllc.pdf
I J.R.Hindley, J.P.Seldin, Lambda-Calculus and Combinators, an Introduction, Cambridge University Press, Cambridge 2008
I M.H.Sørensen, P.Urzyczyn, Lectures on the Curry-Howard Isomorphism, Elsevier, Amsterdam 2006
Twierdzenie. Istnieją dwie niewymierne liczby a i b takie, że ab jest wymierne.
Dowód. Albo (√ 2)
√
2 jest wymierne i wtedy a = b =√ 2 albo (√
2)
√
2 jest niewymierne i wtedy a = (√ 2)
√
2, b =√ 2.
Dowód tego twierdzenie jest oczywiście poprawny w logice klasycznej.
Jest to przykład dowodu niekonstruktywnego, ze względu na wykorzystanie reguły wykluczonego środka. Pomimo, że twierdzenie jest dowiedzione i wiadomo, że liczby a i b istnieją, to nie można (na podstawie dowodu) znaleźć pary liczb spełniających warunek
określony w twierdzeniu. Konstruktywny dowód tego twierdzenia jest oparty na twierdzeniu Gelfonda–Schneidera.Wynika z niego, że liczby a = b =√
2 spełniają powyższe twierdzenie.
Reguły wnioskowania w notacji sekwentowej I
(Ass) Γ, ϕ ` ϕ
Γ ` ϕ Γ, ψ ` ϕ (W )
reguły wprowadzania reguły eliminacji Γ, ϕ ` ψ
(→ I) Γ ` ϕ → ψ
Γ1` ϕ → ψ Γ2` ϕ
(→ E) Γ1, Γ2` ψ
Γ, ϕ ` ⊥ Γ ` ¬ϕ (¬I)
Γ1` ¬ϕ Γ2` ϕ Γ1, Γ2` ⊥ (¬E)
Reguły wnioskowania w notacji sekwentowej II
reguły wprowadzania reguły eliminacji Γ1` ϕ Γ2` ψ
Γ1, Γ2` ϕ ∧ ψ (∧I)
Γ ` ϕ ∧ ψ (∧E1) Γ ` ϕ
Γ ` ϕ ∧ ψ (∧E2) Γ ` ψ
Γ ` ϕ
(∨I1) Γ ` ϕ ∨ ψ
Γ ` ψ
(∨I2) Γ ` ϕ ∨ ψ
Γ1` ϕ ∨ ψ Γ2, ϕ ` ρ Γ3, ψ ` ρ Γ1, Γ2, Γ3` ρ (∨E)
(>I)
` > brak
brak Γ ` ⊥ (⊥E)
Γ ` ϕ
Reguły wnioskowania w notacji sekwentowej III
reguły wprowadzania reguły eliminacji Γ1, ϕ ` ψ Γ2, ψ ` ϕ
Γ1, Γ2` ϕ ↔ ψ (↔I)
Γ1` ϕ ↔ ψ Γ2` ϕ
(↔E1) Γ1, Γ2` ψ
Γ1` ϕ ↔ ψ Γ2` ψ
(↔E2) Γ1, Γ2` ϕ
dla logiki klasycznej Γ, ¬ϕ ` ⊥
(RAA)
Γ ` ϕ lub Γ ` ¬¬ϕ
Γ ` ϕ (¬¬) lub (T N D)
` ϕ ∨ ¬ϕ (RAA) — reductio ad absurdum (reguła sprowadzenia do sprzeczności)
Reguły wnioskowania w notacji założeniowej I
reguły wprowadzania reguły eliminacji
ϕ ψ
ϕ ∧ ψ (∧I)
ϕ ∧ ψ
(∧E1) ϕ
ϕ ∧ ψ (∧E2) ψ
ϕ (∨I1) ϕ ∨ ψ
ψ (∨I2)
ϕ ∨ ψ ϕ ∨ ψ
[ϕ]n ... ρ
[ψ]n ... ρ
n(∨E) ρ
(>I)
> brak
brak ⊥ϕ (⊥E)
Reguły wnioskowania w notacji założeniowej II
reguły wprowadzania reguły eliminacji [ϕ]n
... ψ
n(→ I) ϕ → ψ
ϕ → ψ ϕ
(→ E) ψ
[ϕ]n ...
⊥ n(¬I)
¬ϕ
¬ϕ ϕ
⊥ (¬E)
Reguły wnioskowania w notacji założeniowej III
reguły wprowadzania reguły eliminacji [ϕ]n
.. . ψ
[ψ]n .. . ϕ
n(↔ I) ϕ ↔ ψ
ϕ ↔ ψ ϕ
(↔ E1) ψ
ϕ ↔ ψ ψ
(↔ E2) ϕ
dla logiki klasycznej [¬ϕ]n
.. .
⊥ϕ n(RAA)
lub ¬¬ϕ
ϕ (¬¬) lub (T N D)
ϕ ∨ ¬ϕ
(RAA) — reductio ad absurdum (reguła sprowadzenia do sprzeczności) (T N D) — tertium non datur (reguła wykluczonego środka)
(¬¬) — reguła podwójnego zaprzeczenia
Prawo sylogizmu hipotetycznego:
` (ϕ → ψ) → (ψ → ρ) → ϕ → ρ
Notacja sekwentowa.
(Ass)
ψ → ρ ` ψ → ρ
(Ass)
ϕ → ψ ` ϕ → ψ ϕ ` ϕ (Ass)
(→ E)
ϕ → ψ, ϕ ` ψ
(→ E)
ψ → ρ, ϕ → ψ, ϕ ` ρ
(→ I)
ψ → ρ, ϕ → ψ ` ϕ → ρ
(→ I)
ϕ → ψ ` (ψ → ρ) → ϕ → ρ
(→ I)
` (ϕ → ψ) → (ψ → ρ) → ϕ → ρ
Prawo sylogizmu hipotetycznego:
` (ϕ → ψ) → (ψ → ρ) → ϕ → ρ
Notacja założeniowa.
[ψ → ρ]1
[ϕ → ψ]2 [ϕ]3
(→ E)
ψ (→ E)
ρ
3(→ I)
ϕ → ρ
1(→ I)
(ψ → ρ) → ϕ → ρ
2(→ I)
(ϕ → ψ) → (ψ → ρ) → ϕ → ρ
Prawo importacji: ` (ϕ → ψ → ρ) → (ϕ ∧ ψ → ρ)
Notacja sekwentowa.
(Ass) p → q → r ` p → q → r
(Ass) p ∧ q ` p ∧ q
p ∧ q ` p (∧E) (→ E) p → q → r, p ∧ q ` q → r
(Ass) p ∧ q ` p ∧ q
p ∧ q ` q (∧E) (→ E) p → q → r, p ∧ q ` r
(→ I) p → q → r ` p ∧ q → r
(→ I)
` (p → q → r) → (p ∧ q → r)
Prawo importacji: ` (ϕ → ψ → ρ) → (ϕ ∧ ψ → ρ)
Notacja założeniowa.
[ϕ → ψ → ρ]2
[ϕ ∧ ψ]1 ϕ (∧E)
(→ E)
ψ → ρ
[ϕ ∧ ψ]1 ψ (∧E)
(→ E)
ρ
1(→ I)
ϕ ∧ ψ → ρ
2(→ I)
(ϕ → ψ → ρ) → (ϕ ∧ ψ → ρ)
Relacja typizująca
Γ ` M : τ gdzie Γ oznacza kontekst typizujący
Γ ≡ {x1 : σ1, . . . , xn: σn}
w którym każda zmienna występuje co najwyżej raz.
Γ ` M : τ można czytać “w kontekście Γ term M ma typ τ ”.
Reguły typizacji. Wersja 1: notacja sekwentowa
(Ass)
Γ, x : τ ` x : τ Γ ` M : τ (W) Γ, x : σ ` M : τ Γ, x : σ ` M : τ
(→ I)
Γ ` λx.M : σ → τ Γ1 ` M : σ → τ Γ2 ` N : σ
(→ E)
Γ1, Γ2 ` M N : τ
Reguły typizacji. Wersja 2: notacja założeniowa
reguła wprowadzania reguła eliminacji [x : ϕ]
... M : ψ
(→ I) λx.M : ϕ → ψ
M : ϕ → ψ N : ϕ
(→ E) M N : ψ
Termin “izomorfizm Curry’ego-Howarda” oznacza ścisłą odpowiedniość pomiędzy
I formułami i typami
I dowodami i termami (programami)
Prawo sylogizmu hipotetycznego:
` (ϕ → ψ) → (ψ → ρ) → ϕ → ρ
(Ass) f : ψ → ρ ` f : ψ → ρ
(Ass)
g : ϕ → ψ ` g : ϕ → ψ (Ass)
x : ϕ ` x : ϕ (→ E) g : ϕ → ψ, x : ϕ ` gx : ψ
(→ E) f : ψ → ρ, g : ϕ → ψ, x : ϕ ` f (gx) : ρ
(→ I) f : ψ → ρ, g : ϕ → ψ ` λx.f (gx) : ϕ → ρ
(→ I) g : ϕ → ψ ` λf x.f (gx) : (ψ → ρ) → ϕ → ρ
(→ I)
` λgf x.f (gx) : (ϕ → ψ) → (ψ → ρ) → ϕ → ρ
Prawo sylogizmu hipotetycznego = składanie funkcji
Niech będą dane dwie funkcje f : ψ → ρ oraz g : ϕ → ψ. Złożenie (f ◦ g) : ϕ → ρ jest definiowane następująco (patrz wykład 3):
(f ◦ g)(x) = f (gx)
(Ass)
f : ϕ → ϕ ` f : ϕ → ϕ f : ϕ → ϕ, x : ψ ` f : ϕ → ϕ (W )
(→ I)
f : ϕ → ϕ ` λx.f : ψ → ϕ → ϕ
(→ I)
` λf x.f : (ϕ → ϕ) → ψ → ϕ → ϕ
(Ass)
y : ϕ ` y : ϕ
(→ I)
` λy.y : ϕ → ϕ
(→ E)
` (λf x.f )(λy.y) : ψ → ϕ → ϕ
Przedstawione drzewo wywodu nie jest najprostsze. Wykorzystano założenie f : ϕ → ϕ. Jednak w prawym poddrzewie rzeczywiście udowodniliśmy ϕ → ϕ, wobec tego założenie f : ϕ → ϕ właściwie nie było potrzebne. W efekcie otrzymany λ-term zawiera β-redeks. Niżej przedstawiono najkrótszy dowód ψ → ϕ → ϕ.
(Ass)
y : ϕ ` y : ϕ x : ψ, y : ϕ ` y : ϕ (W )
(→ I)
x : ψ ` λy.y : ϕ → ϕ
(→ I)
` λxy.y : ψ → ϕ → ϕ
Normalizacja (upraszczanie) dowodów ≈ redukcja termów
(Ass) x : σ ` x : σ
D1
∆, x : σ ` M : τ
(→ I)
∆ ` λx.M : σ → τ
D2
Γ ` N : σ (→ E) Γ, ∆ ` (λx.M )N : τ
→β
D2
Γ ` N : σ D1[x := N ] Γ, ∆ ` M [x := N ] : τ
Bezpośrednio po regule wprowadzania (→ I) została użyta reguła eliminacji (→ E).
D
Γ ` M : σ → τ x : σ ` x : σ (Ass)(→ E) Γ, x : σ ` M x : τ
(→ I)
Γ ` λx.M x : σ → τ
→η D
Γ ` M : σ → τ Bezpośrednio po regule eliminacji (→ E)
Przykład (bardziej skomplikowany) D= [y : σ → τ] [z : σ]
(→ E)
yz : τ
[v : τ → ξ] [u : τ ] (→ E) vu : ξ
(→ I) λu.vu : τ → ξ
(→ I) λvu.vu : (τ → ξ) → τ → ξ
[x : σ → τ → ξ] [z : σ]
(→ E) xz : τ → ξ
(→ E)
(λvu.vu)(xz) : τ → ξ D
(λvu.vu)(xz)(yz) : ξ
(→ I) λz.(λvu.vu)(xz)(yz) : σ → ξ
(→ I) λyz.(λvu.vu)(xz)(yz) : (σ → τ ) → σ → ξ
λxyz.(λvu.vu)(xz)(yz) : (σ → τ → ξ) → (σ → τ ) → σ → ξ W otrzymanym λ-termie są zawarte dwa redeksy: η-redeks λvu.vu oraz β-redeks (λv.M )(xz). Po redukcji otrzymamy term λxyz.xz(yz).
Przykładowy wywód po zastosowaniu →η
D= [y : σ → τ] [z : σ]
(→ E)
yz : τ
[v : τ → ξ]
(→ I) λv.v : (τ → ξ) → τ → ξ
[x : σ → τ → ξ] [z : σ]
(→ E) xz : τ → ξ
(→ E)
(λv.v)(xz) : τ → ξ D
(λv.v)(xz)(yz) : ξ
(→ I) λz.(λv.v)(xz)(yz) : σ → ξ
(→ I) λyz.(λv.v)(xz)(yz) : (σ → τ ) → σ → ξ
λxyz.(λv.v)(xz)(yz) : (σ → τ → ξ) → (σ → τ ) → σ → ξ
Przykładowy wywód po zastosowaniu →β
D= [y : σ → τ] [z : σ]
(→ E)
yz : τ
[x : σ → τ → ξ] [z : σ]
(→ E)
xz : τ → ξ D
(→ E)
xz(yz) : ξ
(→ I)
λz.xz(yz) : σ → ξ
(→ I)
λyz.xz(yz) : (σ → τ ) → σ → ξ
λxyz.xz(yz) : (σ → τ → ξ) → (σ → τ ) → σ → ξ
Relacja typizująca
Γ ` M : τ gdzie Γ oznacza kontekst typizujący
Γ ≡ {x1 : σ1, . . . , xn: σn}
w którym każda zmienna występuje co najwyżej raz.
Γ ` M : τ można czytać “w kontekście Γ term M ma typ τ ”.
Reguły typizacji. Notacja sekwentowa
(Ass)
Γ, x : τ ` x : τ Γ ` M : τ (W) Γ, x : σ ` M : τ Γ, x : σ ` M : τ
(→ I)
Γ ` λx.M : σ → τ Γ1 ` M : σ → τ Γ2 ` N : σ
(→ E)
Γ1, Γ2 ` M N : τ Γ ` M : ϕ ∆ ` N : ψ
Γ, ∆ ` pair M N : ϕ ∧ ψ (∧I)
Γ ` M : ϕ ∧ ψ
(∧E1)
Γ ` fst M : ϕ
Γ ` M : ϕ ∧ ψ
(∧E2)
Γ ` snd M : ψ
Reguły typizacji. Notacja sekwentowa
Γ ` M : ϕ
(∨I1)
Γ ` inl M : ϕ ∨ ψ
Γ ` M : ψ
(∨I2)
Γ ` inr M : ϕ ∨ ψ Γ ` M : ϕ ∨ ψ ∆1, x : ϕ ` P : ρ ∆2, x : ψ ` Q : ρ
Γ, ∆1, ∆2 ` when M (λx.P )(λx.Q) : ρ (∨E)
Γ ` M : ⊥ (⊥E) Γ ` absurdE M : τ
Γ, x : σ ` M : ⊥ Γ ` neg λx.M : ¬σ (¬I)
Γ1 ` M : ¬σ Γ2 ` N : σ
Reguły redukcji dla λ
→∧∨⊥¬I (λx.M )N → M [x := N ]
I fst(pair M N ) → M
I snd(pair M N ) → N
I when(inl M )P Q → P M
I when(inr M )P Q → QM
I negE(neg M )N → M N
Prawo importacji: ` (ϕ → ψ → ρ) → (ϕ ∧ ψ → ρ)
Notacja sekwentowa.
D= x : p ∧ q ` x : p ∧ q (Ass) x : p ∧ q ` snd x : q (∧E)
(Ass)
f : p → q → r ` f : p → q → r
(Ass)
x : p ∧ q ` x : p ∧ q x : p ∧ q ` fst x : p (∧E)
(→ E)
f : p → q → r, x : p ∧ q ` f (fst x) : q → r D f : p → q → r, x : p ∧ q ` f (fst x)(snd x) : r
(→ I)
f : p → q → r ` λx.f (fst x)(snd x) : p ∧ q → r
(→ I)
` λf.λx.f (fst x)(snd x) : (p → q → r) → (p ∧ q → r)
Prawo importacji: ` (ϕ → ψ → ρ) → ϕ ∧ ψ → ρ
Notacja założeniowa.
[f : ϕ → ψ → ρ]
[x : ϕ ∧ ψ]
fst x : ϕ (∧E) (→ E)
f (fst x) : ψ → ρ
[x : ϕ ∧ ψ]
snd x : ψ (∧E) (→ E)
f (fst x)(snd x) : ρ
(→ I)
λx.f (fst x)(snd x) : ϕ ∧ ψ → ρ
(→ I)
λf λx.f (fst x)(snd x) : (ϕ → ψ → ρ) → ϕ ∧ ψ → ρ Prawo importacji = zwijanie funkcji
(patrz wykład 3, funkcja uncurry)
Prawo eksportacji: ` (ϕ ∧ ψ → ρ) → ϕ → ψ → ρ
[f : ϕ ∧ ψ → ρ]
[x : ϕ] [y : ψ]
pair x y : ϕ ∧ ψ (∧I) (→ E)
f (pair x y) : ρ
(→ I)
λy.f (pair x y) : ψ → ρ
(→ I)
λxy.f (pair x y) : ϕ → ψ → ρ
(→ I)
λf xy.f (pair x y) : (ϕ ∧ ψ → ρ) → ϕ → ψ → ρ Prawo eksportacji = rozwijanie funkcji
(patrz wykład 3, funkcja curry)
I Podstawianie. Jeśli Γ, x : σ ` M : τ oraz Γ ` N : σ, to Γ ` M [x := N ] : τ .
I Poprawność redukcji. Jeśli Γ ` M : τ oraz M βη N , to Γ ` N : τ .
I Silna normalizacja. Jeśli Γ ` M : τ to term M jest silnie normalizowalny.
I Typ główny (najogólniejszy). Jeśli term M jest typizowalny, to istnieje dla niego typ główny, z którego można otrzymać wszystkie typy tego termu (przez odpowiednie podstawienia za zmienne przebiegające typy).
