Rachunek lambda, lato 2019-20

(1)

Rachunek lambda, lato 2019-20

Wykład 11

15 maja 2020

(2)

Powtórzenie z teorii złożoności:

alternacja

(3)

Maszyna alternująca

Maszyna ma stany (konfiguracje, pozycje):

egzystencjalne i uniwersalne.

Konfiguracja akceptująca (końcowa) jest wygrywająca.

Konfiguracja niekońcowa C o następnikach C₁, ..., C_n jest wygrywająca, gdy:

-C jest egzystencjalna i któraś z C₁, ..., C_n jest wygrywająca;

-C jest uniwersalna i wszystkie C₁, ..., C_n są wygrywające.

Maszyna akceptuje, gdy konfiguracja początkowa jest wygrywająca.

Obliczenie akceptujące = drzewo.

(4)

Maszyna alternująca to gra

Pozycje w grze, to konfiguracje maszyny.

Zaczynamy w konfiguracji początkowej.

W pozycji niekońcowej C o następnikach C₁, ..., C_n, następną pozycję spośródC₁, ..., C_n wybiera:

- gracz egzystencjalny ∃, jeśli C egzystencjalna;

- gracz uniwersalny∀, jeśli C uniwersalna.

W pozycji końcowej gracz∃ wygrywa.

Obliczenie akceptujące = strategia gracza egzystencjalnego.

(5)

Złożoność alternująca

A^LOGSPACE = P^TIME APTIME = PSPACE

APSPACE = EXPTIME

A^EXPTIME = E^XPSPACE i tak dalej.

(6)

Powtórzenie z logiki:

minimalny rachunek zdań

(7)

Naturalna dedukcja

Dowodzimy osądów postaciΓ ` A, gdzie Γ jest zbiorem formuł, a Ajest formułą. Sens: A wynika z założeń Γ.

I Reguływprowadzania spójników logicznych: jak można udowodnić formułę danej postaci?

I Regułyeliminacji spójników: jak można wykorzystać formułę tej postaci do udowodnienia innej?

(8)

Naturalna dedukcja

Dowodzimy osądów postaciΓ ` A, gdzie Γ jest zbiorem formuł, a Ajest formułą. Sens: A wynika z założeń Γ.

I Reguływprowadzania spójników logicznych: jak można udowodnić formułę danej postaci?

I Regułyeliminacji spójników: jak można wykorzystać formułę tej postaci do udowodnienia innej?

(9)

Naturalna dedukcja: reguły dla →

Γ, σ ` σ (Ax)

Γ, σ ` τ

(I →) Γ ` σ → τ

Γ ` σ → τ Γ ` σ

(E →) Γ ` τ

(10)

Natural deduction: notacja dla dowodów

Γ,

x :

σ `

x :

σ

Γ,

x :

σ `

M :

τ Γ `

λx M :

σ → τ

Γ `

M :

σ → τ Γ `

N :

σ Γ `

MN :

τ

(11)

Natural deduction: notacja dla dowodów

Γ,x :σ `

x :

σ

Γ,

x :

σ `

M :

τ Γ `

λx M :

σ → τ

Γ `

M :

σ → τ Γ `

N :

σ Γ `

MN :

τ

(12)

Natural deduction: notacja dla dowodów

Γ,x :σ `x :σ

Γ,

x :

σ `

M :

τ Γ `

λx M :

σ → τ

Γ `

M :

σ → τ Γ `

N :

σ Γ `

MN :

τ

(13)

Natural deduction: notacja dla dowodów

Γ,x :σ `x :σ

Γ,

x :

σ `

M :

τ Γ `

λx M :

σ → τ

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

MN :

τ

(14)

Natural deduction: notacja dla dowodów

Γ,x :σ `x :σ

Γ,

x :

σ `

M :

τ Γ `

λx M :

σ → τ

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

(15)

Natural deduction: notacja dla dowodów

Γ,x :σ `x :σ

Γ,x :σ `M :τ Γ `

λx M :

σ → τ

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

(16)

Natural deduction: notacja dla dowodów

Γ,x :σ `x :σ

Γ,x :σ `M :τ Γ `λx M :σ → τ

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

(17)

Curry-Howard isomorphism

Types = Formulas Terms = Proofs

Computation = Proof normalization

(18)

Curry-Howard isomorphism

Twierdzenie

Dla dowolnego typuτ, kombinator typu τ istnieje wtedy i tylko wtedy, gdyτ jest twierdzeniem logiki minimalnej.

Dowód: Inhabitant typu τ to nic innego jak dowód twierdzenia (ale z dodatkowymi adnotacjami).

(Twierdzenie nadal zachodzi, jeśli zamiast „minimalnej” napiszemy „intuicjonistycznej”.)

(19)

Curry-Howard isomorphism

Twierdzenie

(Twierdzenie nadal zachodzi, jeśli zamiast „minimalnej” napiszemy „intuicjonistycznej”.)

(20)

Curry-Howard isomorphism

Twierdzenie

(Twierdzenie nadal zachodzi, jeśli zamiast „minimalnej”

napiszemy „intuicjonistycznej”.)

(21)

Normalizacja

Γ, σ ` σ

··

·· Γ, σ ` τ· Γ ` σ → τ

·· Γ ` σ· Γ ` τ

⇒

·· Γ ` σ·

··

·· Γ ` τ·

(λx :σ M^τ)N^σ ⇒ M^τ[x := N^σ]

(22)

Normalizacja

Γ, σ ` σ

··

·· Γ, σ ` τ· Γ ` σ → τ

·· Γ ` σ· Γ ` τ

⇒

·· Γ ` σ·

··

·· Γ ` τ·

(23)

Normalizacja

Γ, σ ` σ

··

·· Γ, σ ` τ· Γ ` σ → τ

·· Γ ` σ· Γ ` τ

⇒

·· Γ ` σ·

··

·· Γ ` τ·

(24)

Sens moralny normalizacji

Jeśli τ jest twierdzeniem, to istnieje taki termM w postaci normalnej, że ` M : τ.

Czyli „dowód normalny”.

Wniosek: Logika minimalna jest niesprzeczna: istnieją formuły, których nie można udowodnić. Dowód: Na przykład 0 p, bo w pustym otoczeniu nie ma termu normalnego o typie atomowym.

(25)

Sens moralny normalizacji

Wniosek: Logika minimalna jest niesprzeczna:

istnieją formuły, których nie można udowodnić.

Dowód: Na przykład 0 p, bo w pustym otoczeniu nie ma termu normalnego o typie atomowym.

(26)

Sens moralny normalizacji

Wniosek: Logika minimalna jest niesprzeczna:

istnieją formuły, których nie można udowodnić.

Dowód: Na przykład 0 p, bo w pustym otoczeniu nie ma termu normalnego o typie atomowym.

(27)

The inhabitation problem

Inhabitation problem:

GivenΓ, τ, is there M such that Γ ` M : τ?

Twierdzenie (R. Statman):

Inhabitation in simple types is decidable and P^SPACE-complete.

Wniosek:

To samo dotyczy minimalnego rachunku zdań.

Uwaga:

Klasyczny rachunek zdań jest . . .

. . . „ zaledwie” co-NP zupełny.

(28)

The inhabitation problem

Inhabitation problem:

Twierdzenie (R. Statman):

Inhabitation in simple types is decidable and PSPACE-complete.

Wniosek:

Uwaga:

(29)

The inhabitation problem

Inhabitation problem:

Twierdzenie (R. Statman):

Wniosek:

Uwaga:

(30)

The inhabitation problem

Inhabitation problem:

Twierdzenie (R. Statman):

Wniosek:

Uwaga:

(31)

The inhabitation problem

Inhabitation problem:

Twierdzenie (R. Statman):

Wniosek:

Uwaga:

(32)

Long normal forms

I If x : α1 → · · · α_n → p and M1 : α1, . . . M_k : α_k are long normal forms thenxM1. . . Mk : p is a long normal form.

I If M : β is a long normal form, then λx : α. M is a long normal form of type α → β.

Lemat 1:

If Γ ` M : τ then there exists a long normal formM⁰ such that M⁰ =_βη M and Γ ` M⁰ : τ.

Lemat 2:

If Γ(x ) = ρ and Γ ∪ {y : ρ} ` M : τ then Γ ` M[y := x ] : τ.

(33)

Long normal forms

Lemat 1:

Lemat 2:

If Γ(x ) = ρ and Γ ∪ {y : ρ} ` M : τ then Γ ` M[y := x ] : τ.

(34)

Long normal forms

Lemat 1:

Lemat 2:

If Γ(x ) = ρ and Γ ∪ {y : ρ} ` M : τ

(35)

Searching for long normal forms

The Wajsberg/Ben-Yelles algorithm:

To answerΓ ` ? : α, apply one of the following tactics:

I Forα = β → γ, ask Γ ∪ {x : β} ` ? : γ (freshx). (SolutionM = λx :β. N^γ.)

I Forα = p, choose x : β1 → · · · → βk → p from Γ, then ask Γ ` ? : β_i,for all i. Success if k = 0. (SolutionM = xN₁^β¹. . . N_k^β^k.)

(36)

Searching for long normal forms

I Forα = β → γ, ask Γ ∪ {x : β} ` ? : γ (freshx).

(SolutionM = λx :β. N^γ.)

I Forα = p, choose x : β1 → · · · → βk → p from Γ, then ask Γ ` ? : β_i,for all i. Success if k = 0. (SolutionM = xN₁^β¹. . . N_k^β^k.)

(37)

Searching for long normal forms

I Forα = p, choose x : β1 → · · · → βk → p from Γ, then ask Γ ` ? : β_i,for all i. Success if k = 0.

(SolutionM = xN₁^β¹. . . N_k^β^k.)

(38)

Alternation

I A solution of Γ ` ? : p is of the form M = xN₁^β¹. . . N_k^β^k, for somex : β1 → · · · → βk → p in Γ.

I Nondeterminism: because there can be more than one x.

I Branching (recursion): because Γ ` Ni : βi must be solved in parallel.

(39)

Alternation

I Branching (recursion): because Γ ` Ni : βi must be solved in parallel.

(40)

Alternation

I Branching (recursion): because Γ ` N_i : β_i must be solved in parallel.

(41)

Ben-Yelles algorithm

Ten alternujący proces można objaśniać jako grę między graczem ∃(który dowodzi twierdzenia) i graczem ∀ (który poszukuje błędu w dowodzie). Rozwiązanie istnieje wtedy i tylko wtedy, gdy gracz ∃ma strategię zwycięską.

(42)

Ben-Yelles algorithm

Ten alternujący proces można objaśniać jako grę między graczem ∃(który dowodzi twierdzenia) i graczem ∀ (który poszukuje błędu w dowodzie). Rozwiązanie istnieje

(43)

Przykład (nieformalny): (p → ¬q) → (¬p → ¬q) → ¬q (Negacja ¬α oznacza α → ⊥)

(Assumptions: x : p → ¬q, y : ¬p → ¬q, z : q. Goal: ⊥) Opponent (∀): Can you prove ⊥?

Player (∃): I will use assumptiony!

Opponent (∀): Can you prove the 1st assumption¬p ? That is, can you prove⊥ using new asumption v : p? Player (∃): Yes, I will use assumption x!

Opponent (∀): Can you prove the 2nd assumptionq? Player (∃): Sure, take z!

Proof = strategy = inhabitant: λxyz.y(λv .xvz)z

(44)

Przykład (nieformalny): (p → ¬q) → (¬p → ¬q) → ¬q (Negacja ¬α oznacza α → ⊥)

(Assumptions: x : p → ¬q, y : ¬p → ¬q, z : q. Goal: ⊥)

Opponent (∀): Can you prove ⊥? Player (∃): I will use assumptiony!

(45)

Przykład (nieformalny): (p → ¬q) → (¬p → ¬q) → ¬q (Negacja ¬α oznacza α → ⊥)

(46)

Przykład (nieformalny): (p → ¬q) → (¬p → ¬q) → ¬q (Negacja ¬α oznacza α → ⊥)

(47)

Przykład (nieformalny): (p → ¬q) → (¬p → ¬q) → ¬q (Negacja ¬α oznacza α → ⊥)

Opponent (∀): Can you prove the 1st assumption¬p ?

That is, can you prove⊥ using new asumption v : p? Player (∃): Yes, I will use assumption x!

(48)

Przykład (nieformalny): (p → ¬q) → (¬p → ¬q) → ¬q (Negacja ¬α oznacza α → ⊥)

Opponent (∀): Can you prove the 1st assumption¬p ? That is, can you prove⊥ using new asumption v : p?

Player (∃): Yes, I will use assumption x!

(49)

Przykład (nieformalny): (p → ¬q) → (¬p → ¬q) → ¬q (Negacja ¬α oznacza α → ⊥)

(50)

Przykład (nieformalny): (p → ¬q) → (¬p → ¬q) → ¬q (Negacja ¬α oznacza α → ⊥)

Opponent (∀): Can you prove the 2nd assumptionq?

Player (∃): Sure, take z!

(51)

Przykład (nieformalny): (p → ¬q) → (¬p → ¬q) → ¬q (Negacja ¬α oznacza α → ⊥)

(52)

Przykład (nieformalny): (p → ¬q) → (¬p → ¬q) → ¬q (Negacja ¬α oznacza α → ⊥)

Opponent (∀): Can you prove the 2nd assumptionq?

(53)

Termination

I The question Γ ` ? : β → γ leads to Γ ∪ {x :β} ` ? : γ.

The environment Γ is extended by x : β.

I Every suchβ is a subformula in the initial problem (there is only a linear number of such formulas).

I New variables can be replaced by old ones, i.e.,Γ must in fact stabilize (in polynomial time).

Po wielomianowej liczbie kroków zadanie musi się powtórzyć. Morał: Problem inhabitacji (czyli problem decyzyjny dla minimalnego rachunku zdań) jest w klasie A^PTIME = P^SPACE

(54)

Termination

(55)

Termination

(56)

Termination

Po wielomianowej liczbie kroków zadanie musi się powtórzyć.

Morał: Problem inhabitacji (czyli problem decyzyjny dla minimalnego rachunku zdań) jest w klasie A^PTIME = P^SPACE

(57)

Termination

Po wielomianowej liczbie kroków zadanie musi się powtórzyć.

Morał: Problem inhabitacji (czyli problem decyzyjny dla minimalnego rachunku zdań) jest w klasie A = P

(58)

Konstrukcja dowodu jako obliczenie

OsądΓ ` q (gdzie q – atom), można interpretować jako konfigurację automatu:

I Cel atomowyq to stan maszyny;

I OtoczenieΓ to zawartość pamięci, w tym program.

I Założenie p → q umożliwia zmianę stanu z q na p.

I Założenie (b → p) → q umożliwia zmianę stanu zq na p, z jednoczesnym zapisaniem b w pamięci.

I Założenie p → r → q to krok uniwersalny do p i r na raz.

I Założenie a → p → q umożliwia zmianę stanu zq na p, gdy w pamięci jest zapisanea.

Uwaga: (1) nie można usunąć danej z pamięci; (2) nie można sprawdzić, że danej w pamięci nie ma.

(59)

Konstrukcja dowodu jako obliczenie

(60)

Konstrukcja dowodu jako obliczenie

(61)

Konstrukcja dowodu jako obliczenie

(62)

Konstrukcja dowodu jako obliczenie

I Założenie (b → p) → q umożliwia zmianę stanu zq na p, z jednoczesnym zapisaniemb w pamięci.

(63)

Konstrukcja dowodu jako obliczenie

(64)

Konstrukcja dowodu jako obliczenie

(65)

Konstrukcja dowodu jako obliczenie

Uwaga: (1) nie można usunąć danej z pamięci;

(66)

Monotonic automata

Monotonic automaton: M = hQ, R, f , Ii,

I Q is a finite set of states, f ∈ Q the final state.

I R is a finite set of registers;

I I is a finite set of instructions of the form:

(1) q :checkS1;setS2;jmpp, (2) q :jmpp₁ andp₂,

wherep, p₁, p₂ ∈ Q and S₁, S₂ ⊆ R.

(67)

Monotonic automata

Configuration: hq, Si, where q ∈ Q and S ⊆ R.

Final configurations are winning.

Transitions:

I forI = q : checkS1;setS2;jmpp: hq, Si →_I hp, S ∪ S₂i, provided S₁ ⊆ S; If hp, S ∪ S₂i winning then hq, Si is winning

I forI = q : jmpp1 andp2:

hq, Si →_I hp₁, S i and hq, Si →_I hp₂, S i If hp₁, S i and hp₂, S i are winning then so is hq, Si.

(68)

Monotonic automata

Transitions:

I forI = q : checkS₁;setS₂;jmpp:

hq, Si →_I hp, S ∪ S₂i, provided S₁ ⊆ S; If hp, S ∪ S₂i winning then hq, Si is winning

I forI = q : jmpp1 andp2:

(69)

Monotonic automata

Transitions:

I forI = q : checkS₁;setS₂;jmpp:

hq, Si →_I hp, S ∪ S₂i, provided S₁ ⊆ S; If hp, S ∪ S₂i winning then hq, Si is winning

I forI = q : jmpp₁ andp₂:

(70)

Monotonic automata

Lemma

The halting problem for monotonic automata Is a given configuration winning?

is PSPACE-hard.

(71)

Monotonic encoding of an ATM

Alternating time p(n).

Registers: stan^t_s, lit^t_ia, poz^t_i, Initial configuration:

C0 = hloop⁰₁, {lit⁰_1a₁, ..., lit⁰_na_n, lit⁰_n+1B, ..., lit⁰_p(n)B, stan⁰₀, poz⁰₁}i. represents initial ID of TM for inputw = a₁...a_n.

Later:

C = hloop^t₁, S i encodes the firstt steps of TM computation, e.g., lit⁵_6a ∈ S iff after 5 steps, the 6th cell contains a.

(72)

Monotonic encoding of an ATM

Registers: stan^t_s, lit^t_ia, poz^t_i,

Initial configuration:

C0 = hloop⁰₁, {lit⁰_1a₁, ..., lit⁰_na_n, lit⁰_n+1B, ..., lit⁰_p(n)B, stan⁰₀, poz⁰₁}i. represents initial ID of TM for inputw = a₁...a_n.

Later:

(73)

Monotonic encoding of an ATM

C0 = hloop⁰₁, {lit⁰_1a₁, ..., lit⁰_na_n, lit⁰_n+1B, ..., lit⁰_p(n)B, stan⁰₀, poz⁰₁}i.

represents initial ID of TM for inputw = a₁...a_n.

Later:

(74)

Monotonic encoding of an ATM

C0 = hloop⁰₁, {lit⁰_1a₁, ..., lit⁰_na_n, lit⁰_n+1B, ..., lit⁰_p(n)B, stan⁰₀, poz⁰₁}i.

represents initial ID of TM for inputw = a₁...a_n. Later:

C = hloop^t₁, S i encodes the firstt steps of TM computation,

(75)

Example instructions for (s, a) ⇒ (u, b, +ε)

When i < p(n):

loop^t_i :

checkstan^t_s, poz^t_i, lit^t_ia;setstan^t+1_u , poz^t+1_{i +ε}, lit^t+1_ib ;jmploop^t_{i +1}; checkstan^t_s, poz^t_j, lit^t_ia;setlit^t+1_ia ;jmploop^t_{i +1};

When i = p(n):

loop^t_i :

checkstan^t_s, poz^t_i, lit^t_ia;setstan^t+1_u , poz^t+1_{i +ε}, lit^t+1_ib ;jmploop^t+1₁ ; checkstan^t_s, poz^t_j, lit^t_ia;setlit^t+1_ia ;jmploop^t+1₁ .

(76)

Example instructions for (s, a) ⇒ (u, b, +ε)

When i < p(n):

loop^t_i :

checkstan^t_s, poz^t_i, lit^t_ia;setstan^t+1_u , poz^t+1_{i +ε}, lit^t+1_ib ;jmploop^t_{i +1}; checkstan^t_s, poz^t_j, lit^t_ia;setlit^t+1_ia ;jmploop^t_{i +1};

When i = p(n):

loop^t_i :

checkstan^t_s, poz^t_i, lit^t_ia;setstan^t+1_u , poz^t+1_{i +ε}, lit^t+1_ib ;jmploop^t+1₁ ;

(77)

Example instructions: universal split

Assume that TM does not write nor move in universal states.

When i < p(n):

loop^t_i :checkstan^t_s, lit^t_ia, poz^t_j;setlit^t+1_ia , poz^t+1_j ;jmploop^t_{i +1};

When i = p(n):

loop^t_i :checkstan^t_s, lit^t_ia, poz^t_j;setlit^t+1_ia , poz^t+1_j ;jmpsplit_s^t+1₁_s₂; split^t+1_s₁_s₂ :jmpgo^t+1_s₁ andgo^t+1_s₂ ;

go^t+1_s₁ :check∅;setstan^t+1_s₁ ;jmploop^t+1₁ ;

(78)

Example instructions: universal split

Assume that TM does not write nor move in universal states.

When i < p(n):

loop^t_i :checkstan^t_s, lit^t_ia, poz^t_j;setlit^t+1_ia , poz^t+1_j ;jmploop^t_{i +1};

When i = p(n):

loop^t_i :checkstan^t_s, lit^t_ia, poz^t_j;setlit^t+1_ia , poz^t+1_j ;jmpsplit_s^t+1₁_s₂; split^t+1_s₁_s₂ :jmpgo^t+1_s₁ andgo^t+1_s₂ ;

(79)

Programs into proofs!

GivenM = hQ, R, f , Ii and C₀ = hq₀, S₀i, define a set of axiomsΓ so that

Γ ` q0 iff C0 is winning.

Propositional variables: states and registers of M. Put all ofS₀ into Γ, alsof ∈ Γ.

Other axioms represent instructions of M.

(80)

Programs into proofs!

Propositional variables: states and registers of M.

Put all ofS₀ into Γ, alsof ∈ Γ.

(81)

Programs into proofs!

(82)

Programs into proofs!

(83)

Instructions seen as axioms

Axiom for q :checkS₁;setS₂;jmpp, whereS₁ = {s₁¹, ..., s₁^k} and S₂ = {s₂¹, ..., s₂^`}:

(1) s₁¹ → · · · → s₁^k → (s₂¹ → · · · s₂^` → p) → q.

Axiom forq :jmpp₁ andp₂:

(2) p₁ → p₂ → q.

(84)

Proof construction as computation

To prove Γ, S ` q, one can:

I Note that q = f and observe f ∈ Γ;

I Use axiomp₁ → p₂ → q and prove in parallel: Γ, S ` p1 and Γ, S ` p2

I Use axioms₁¹ → · · · → s₁^k → (s₂¹ → · · · s₂^` → p) → q, provided S1 = {s₁¹, ..., s₁^k} ⊆ S, and prove that

Γ, S , s₂¹, ..., s₂^` ` p

(85)

Proof construction as computation

I Use axiomp₁ → p₂ → q and prove in parallel: Γ, S ` p1 and Γ, S ` p2

Γ, S , s₂¹, ..., s₂^` ` p

(86)

Proof construction as computation

I Use axiomp₁ → p₂ → q and prove in parallel:

Γ, S ` p1 and Γ, S ` p2

Γ, S , s₂¹, ..., s₂^` ` p

(87)

Proof construction as computation

I Use axiomp₁ → p₂ → q and prove in parallel:

Γ, S ` p1 and Γ, S ` p2

Γ, S , s₂¹, ..., s₂^` ` p

(88)

The technical lemma we need

Lemma

Γ, S ` q iff hq, S0∪ Si is winning.

Proof.

(⇒) Induction wrt the size of proof.

(⇐) Induction wrt the definition of acceptance.

(89)

Morał

Twierdzenie:

Minimalny rachunek zdań jest PSPACE-zupełny.

A klasyczny?

Tylko co-NP zupełny.

(90)

Morał

Twierdzenie:

A klasyczny?

(91)

Morał

Twierdzenie:

A klasyczny?

(92)

Hilbert style proofs

Hilbert style propositional axioms for implication:

I α → β → α;

I (α → β → γ) → (α → β) → α → γ.

Hilbert style proof rule: modus ponens (application). Dowód to po prostu ciąg formuł.

Deduction theorem:

If Γ, σ ` τ then Γ ` σ → τ.

(93)

Hilbert style proofs

I α → β → α;

I (α → β → γ) → (α → β) → α → γ.

Hilbert style proof rule: modus ponens (application).

Dowód to po prostu ciąg formuł.

Deduction theorem:

If Γ, σ ` τ then Γ ` σ → τ.

(94)

Hilbert style proofs

I α → β → α;

I (α → β → γ) → (α → β) → α → γ.

Hilbert style proof rule: modus ponens (application).

Dowód to po prostu ciąg formuł.

Deduction theorem:

(95)

Example proof

1. (ϕ → (ψ → ϕ) → ϕ) → (ϕ → ψ → ϕ) → ϕ → ϕ;

2. ϕ → (ψ → ϕ) → ϕ;

3. (ϕ → ψ → ϕ) → ϕ → ϕ (detach 2 from 1);

4. ϕ → ψ → ϕ;

5. ϕ → ϕ (detach 4 from 3).

(96)

Proofs as combinators

I

K :

α → β → α;

I

S :

(α → β → γ) → (α → β) → α → γ.

Deduction theorem:

If Γ,

x :

σ `

M :

τ then Γ `

λ^∗x . M :

σ → τ.

(97)

Proofs as combinators

I K : α → β → α;

I S : (α → β → γ) → (α → β) → α → γ.

Deduction theorem:

If Γ,

x :

σ `

M :

τ then Γ `

λ^∗x . M :

σ → τ.

(98)

Proofs as combinators

I K : α → β → α;

I S : (α → β → γ) → (α → β) → α → γ.

Deduction theorem:

If Γ,x :σ ` M :τ then Γ `

λ^∗x . M :

σ → τ.

(99)

Proofs as combinators

I K : α → β → α;

I S : (α → β → γ) → (α → β) → α → γ.

Deduction theorem:

If Γ,x :σ ` M :τ then Γ `λ^∗x . M :σ → τ.

(100)

Logical connectives

Γ ` ϕ Γ ` ψ

Γ ` ϕ ∧ ψ (I ∧) Γ ` ϕ ∧ ψ

Γ ` ϕ (E ∧) Γ ` ϕ ∧ ψ Γ ` ψ Γ ` ϕ

Γ ` ϕ ∨ ψ (I ∨) Γ ` ψ Γ ` ϕ ∨ ψ Γ ` ϕ ∨ ψ Γ, ϕ ` ϑ Γ, ψ ` ϑ

Γ ` ϑ (E ∨)

Γ ` ⊥ Γ ` ϕ (E ⊥)

(101)

Logical connectives

Γ ` ϕ Γ ` ψ Γ ` ϕ ∧ ψ (I ∧)

Γ ` ϕ ∧ ψ

Γ ` ϕ (E ∧) Γ ` ϕ ∧ ψ Γ ` ψ Γ ` ϕ

Γ ` ϑ (E ∨)

Γ ` ⊥ Γ ` ϕ (E ⊥)

(102)

Logical connectives

Γ ` ϕ Γ ` ψ

Γ ` ϕ ∧ ψ (I ∧) Γ ` ϕ ∧ ψ

Γ ` ϕ (E ∧) Γ ` ϕ ∧ ψ Γ ` ψ

Γ ` ϕ

Γ ` ϑ (E ∨)

Γ ` ⊥ Γ ` ϕ (E ⊥)

(103)

Logical connectives

Γ ` ϕ Γ ` ψ

Γ ` ϕ ∧ ψ (I ∧) Γ ` ϕ ∧ ψ

Γ ` ϕ (E ∧) Γ ` ϕ ∧ ψ Γ ` ψ Γ ` ϕ

Γ ` ϕ ∨ ψ (I ∨) Γ ` ψ Γ ` ϕ ∨ ψ

Γ ` ϕ ∨ ψ Γ, ϕ ` ϑ Γ, ψ ` ϑ

Γ ` ϑ (E ∨)

Γ ` ⊥ Γ ` ϕ (E ⊥)

(104)

Logical connectives

Γ ` ϕ Γ ` ψ

Γ ` ϕ ∧ ψ (I ∧) Γ ` ϕ ∧ ψ

Γ ` ϕ (E ∧) Γ ` ϕ ∧ ψ Γ ` ψ Γ ` ϕ

Γ ` ϑ (E ∨)

Γ ` ⊥ Γ ` ϕ (E ⊥)

(105)

Logical connectives

Γ ` ϕ Γ ` ψ

Γ ` ϕ ∧ ψ (I ∧) Γ ` ϕ ∧ ψ

Γ ` ϕ (E ∧) Γ ` ϕ ∧ ψ Γ ` ψ Γ ` ϕ

Γ ` ϑ (E ∨)

Γ ` ⊥ Γ ` ϕ (E ⊥)

(106)

Conjunction is the product

Γ ` M : ϕ Γ ` N : ψ Γ ` hM, Ni : ϕ ∧ ψ (I ∧)

Γ ` M : ϕ ∧ ψ

Γ ` π₁(M) : ϕ (E ∧) Γ ` M : ϕ ∧ ψ Γ ` π₂(M) : ψ

π₁(hM, Ni) ⇒ M, π₂(hM, Ni) ⇒ N

(107)

Disjunction is the coproduct

Γ `M : ϕ

Γ `inl(M) : ϕ ∨ ψ (W ∨) Γ ` M : ψ Γ `inr(M): ϕ ∨ ψ

Γ ` M : ϕ ∨ ψ Γ(x : ϕ) `P : ϑ Γ(y : ψ) `Q : ϑ Γ `case M of [x]P, [y ]Q : ϑ (E ∨)

case inl(P) of [x]M, [y ]N ⇒ M[x := P]

case inr(Q) of [x]M, [y ]N ⇒ N[y := Q].

(108)

Generalized eta-reductions

If we believe everything is canonical. . . hπ1(M), π2(M)i ⇒ M

(case M of [x ]inl x , [y ]inr y ) ⇒ M.

(109)

Absurd is the empty type (the thing which is not)

Ex falso quodlibet:

Γ ` M : ⊥

Γ ` ε_ϕ(M) : ϕ (E ⊥)

No introduction rule, no beta- or eta-reduction.

(110)

Konserwatywność

Twierdzenie

Intuicjonistyczny rachunek zdań IPC (ze wszystkimi spójnikami

∨, ∧, →, ⊥, ¬ i regułą ex falso) jest konserwatywny nad logiką minimalną: jeśli formuła implikacyjna τ jest twierdzeniem IPC, to jest twierdzeniem logiki minimalnej.

Dowód: Trzeba zdefiniować odpowiedni rachunek lambda z produktami, koproduktami i typem pustym i udowodnić normalizację.

Postać normalna o typie implikacyjnym jest zbudowana tylko

(111)

Classical (unnatural) deduction

¹

Γ, ¬σ ` ⊥

(Cheat) Γ ` σ

Example: Peirce’s Law

((p → q) → p) → p

is classically valid, but unprovable without rule (Cheat). Indeed, there is no normal M with

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

(112)

Classical (unnatural) deduction

¹

Γ, ¬σ ` ⊥

(Cheat) Γ ` σ

((p → q) → p) → p

is classically valid, but unprovable without rule (Cheat).

Indeed, there is no normal M with x : (p → q) → p ` M : p

(113)

Classical (unnatural) deduction

¹

Γ, ¬σ ` ⊥

(Cheat) Γ ` σ

((p → q) → p) → p

is classically valid, but unprovable without rule (Cheat).

Indeed, there is no normal M with x : (p → q) → p ` M : p