Rachunek lambda, lato 2019-20

(1)

Rachunek lambda, lato 2019-20

Wykład 2

6 marca 2020

(2)

Beta-redeks (λx P)Q

...

@

}

λx

Q P

◦

(3)

Beta-redukcja (λx P)Q → P[x := Q]

...

@

}

λx

Q .

P

x

33

x

jj

=⇒ ...

.

P

Q Q

◦

(4)

Beta-redeks w grafie

(1)

@

|

λ

(3)

(2)

◦

(5)

Beta-redukcja w grafie

(1)

@

|

λ

(3)

(2)

◦

33

◦

jj

=⇒ (1)

(2)

(3) (3)

◦

(6)

Beta-redukcja nieco wyidealizowana

(1)

@

|

λx

(4)

(3)

@@

(2)

=⇒ (1)

(4)

(3)

&&

(2)

◦

(7)

Kompozycjonalność

Lemat

(1) Jeśli M →_β M⁰, to M[x := N] →_β M⁰[x := N];

(2) Jeśli N →β N⁰, to M[x := N] β M[x := N⁰], Dowód: Indukcja ze względu na długość M.

Wniosek

Jeśli M β M⁰ i N β N⁰, to M[x := N] β M⁰[x := N⁰].

◦

(8)

Normalizacja

Postać normalnato term bez redeksów.

Nie da się go redukować.

Term M ma postać normalną (jest normalizowalny), gdy redukuje się do pewnej postaci normalnej.

Nazywamy jąpostacią normalna termu M.

Term M jestsilnie normalizowalny (M ∈ SN), gdy nie istnieje nieskończony ciąg

M = M₀ →_β M₁ →_β M₂ →_β · · ·

Inaczej: każdy ciąg redukcji prowadzi do postaci normalnej.

◦

(9)

Przykłady

I Term S = λxyz.xz(yz) jest w postaci normalnej.

I Term SKKjest silnie normalizowalny i ma postać normalną I.

I Term Ω = (λx . xx )(λx . xx ) nie ma postaci normalnej.

I Term (λx . y )Ωma postać normalną y, ale nie jest silnie normalizowalny.

◦

(10)

Własności redukcji

(11)

Abstrakcyjne systemy redukcyjne

Abstrakcyjny system redukcyjny:

para hA, →i, gdzie → jest relacją binarną wA.

Oznaczenia:

→⁺ domknięcie przechodnie;

domknięcie przechodnio-zwrotne;

→⁼ domknięcie zwrotne.

Postać normalna: takie a ∈ A, że ∀b. a 6→ b. Inne definicje stosują się odpowiednio.

◦

(12)

Abstrakcyjne systemy redukcyjne

Oznaczenia:

Postać normalna: takie a ∈ A, że ∀b. a 6→ b.

Inne definicje stosują się odpowiednio.

◦

(13)

Abstrakcyjne systemy redukcyjne

Oznaczenia:

Postać normalna: takie a ∈ A, że ∀b. a 6→ b.

Inne definicje stosują się odpowiednio.

◦

(14)

Silna normalizacja (SN)

Każdy ciąg redukcji a0 → a1 → a2 → · · · jest skończony.

(Wtedy relacja jest dobrym ufundowaniem.)

Fakt: Beta-redukcja nie ma własności silnej normalizacji: Ω →_β Ω →_β Ω →_β · · ·

◦

(15)

Silna normalizacja (SN)

Fakt: Beta-redukcja nie ma własności silnej normalizacji: Ω →_β Ω →_β Ω →_β · · ·

◦

(16)

Silna normalizacja (SN)

Fakt: Beta-redukcja nie ma własności silnej normalizacji:

Ω →_β Ω →_β Ω →_β · · ·

◦

(17)

Własność Churcha-Rossera (CR)

Jeślia b i a c, to istnieje takie d, że b d i c d.

a

b

c

d

◦

(18)

Własność Churcha-Rossera (CR)

Jeślia b i a c, to istnieje takie d, że b d i c d.

a

b

c

d

◦

(19)

Własność rombu (diamond property)

Jeślia → b i a → c, to istnieje takie d, że b → d i c → d.

a

b

c

d

◦

(20)

Własność rombu (diamond property)

Jeślia → b i a → c, to istnieje takie d, że b → d i c → d.

a

b

c

d

◦

(21)

Własność rombu implikuje CR

a₁

//.

//a₂

.

//.

a₃ ^//. ^//. ^//a₄

◦

(22)

Własność rombu?

Fakt: Beta-redukcja nie ma własności rombu.

(λx .xx )((λx .x )y )

xx ''

(λx .x )y ((λx .x )y )

&&

(λx .xx )y

ww

??

◦

(23)

Własność rombu?

Fakt: Beta-redukcja nie ma własności rombu.

(λx .xx )((λx .x )y )

xx ''

(λx .x )y ((λx .x )y )

&&

(λx .xx )y

ww

??

◦

(24)

Słaba własność Churcha-Rossera (WCR)

Jeślia → b i a → c, to istnieje takie d, że b d i c d.

a

b

c

d

Fakt: Beta-redukcja ma słabą własność Churcha-Rossera.

◦

(25)

Słaba własność Churcha-Rossera (WCR)

a

b

c

d

◦

(26)

Słaba własność Churcha-Rossera (WCR)

a

b

c

d

◦

(27)

WCR nie implikuje CR

Przykład:

a ←− b ←→ c −→ d

Lemat Newmana:

WCR ∧ SN =⇒ CR

◦

(28)

Twierdzenie Churcha-Rossera: Beta ma własność CR

Definicja(complete development): Term M^• to pełne rozwinięcie termu M. – x^• = x ;

– (λx M)^• = λx M^•;

– (MN)^• = M^•N^•, gdy M nie jest abstrakcją; – ((λx M)N)^• = M^•[x := N^•].

Sens: jednoczesna redukcja wszystkich istniejących redeksów.

◦

(29)

Twierdzenie Churcha-Rossera: Beta ma własność CR

Definicja(complete development):

Term M^• to pełne rozwinięcie termu M.

– x^• = x ;

– (λx M)^• = λx M^•;

– (MN)^• = M^•N^•, gdy M nie jest abstrakcją;

– ((λx M)N)^• = M^•[x := N^•].

Sens: jednoczesna redukcja wszystkich istniejących redeksów.

◦

(30)

Relacja pomocnicza →

¹

– x → x, gdy x jest zmienną;¹ – jeśli M → M¹ ⁰, to λxM → λxM¹ ⁰; – jeśli M → M¹ ⁰ i N → N¹ ⁰, to:

MN → M¹ ⁰N⁰, oraz (λxM)N → M¹ ⁰[x := N⁰].

Sens: jednoczesna redukcja kilku redeksów

już obecnych w termie.

◦

(31)

Własności relacji →

¹

(1) Jeśli M → M¹ ⁰, to FV(M⁰) ⊆FV(M).

(2) Dla dowolnego M zachodzi M → M¹ oraz M → M¹ ^•.

(3) Jeśli M → M¹ ⁰ i N → N¹ ⁰, to M[x := N]→ M¹ ⁰[x := N⁰].

(4) Jeśli M → M¹ ⁰, to M⁰ → M¹ ^•.

◦

(32)

Własności relacji →

¹

(4) Jeśli M → M¹ ⁰, to M⁰ → M¹ ^•.

◦

(33)

Własności relacji →

¹

(4) Jeśli M → M¹ ⁰, to M⁰ → M¹ ^•.

◦

(34)

Własności relacji →

¹

(4) Jeśli M → M¹ ⁰, to M⁰ → M¹ ^•.

◦

(35)

Relacja → ma własność rombu

¹

M

1

~~

1

!!

M⁰

1

M⁰⁰

}} 1

M^•

◦

(36)

Dowód twierdzenia Churcha-Rossera

1) Ponieważ relacja→ ma własność rombu, więc tym¹ bardziej jej domknięcie przechodnio-zwrotne ma¹ własność rombu.

M₁

//.

//M₂

.

//.

M₃ ^//. ^//. ^//M₄

2) Ponieważ→_β ⊆→ ⊆ ¹ β, więc ¹ i β są równe. 3) Własność rombu dla to własność CR dla →.

◦

(37)

Dowód twierdzenia Churcha-Rossera

M₁

//.

//M₂

.

//.

M₃ ^//. ^//. ^//M₄

2) Ponieważ→_β ⊆→ ⊆ ¹ β, więc ¹ i β są równe. 3) Własność rombu dla to własność CR dla →.

◦

(38)

Dowód twierdzenia Churcha-Rossera

M₁

//.

//M₂

.

//.

M₃ ^//. ^//. ^//M₄

2) Ponieważ→_β ⊆→ ⊆ ¹ β, więc ¹ i β są równe.

3) Własność rombu dla to własność CR dla →.

◦

(39)

Dowód twierdzenia Churcha-Rossera

M₁

//.

//M₂

.

//.

M₃ ^//. ^//. ^//M₄

2) Ponieważ→_β ⊆→ ⊆ ¹ β, więc ¹ i β są równe.

3) Własność rombu dla to własność CR dla →.

◦

(40)

Wnioski z twierdzenia Churcha-Rossera

(1)Jeśli M =_β N, toM β Q_β N, dla pewnego Q.

Q₁

Q₂

Q_n

}}}}

M

M₁

"" ""

M₂ . . . M_n−1 N

{{{{

•

"" ""

•

◦

(41)

Wnioski z twierdzenia Churcha-Rossera

(1)Jeśli M =_β N, toM β Q_β N, dla pewnego Q.

Q₁

Q₂

Q_n

}}}}

M

M₁

"" ""

M₂ . . . Mn−1 N

{{{{

•

"" ""

•

◦

(42)

Wnioski z twierdzenia Churcha-Rossera

(2)Każdy term ma co najwyżej jedną postać normalną (i do niej się redukuje).

Dowód:

JeśliM =_β N i N normalne, to M β Q_β N. SkoroN normalne, to N = Q.

JeśliM też normalne, to M = Q = N.

◦

(43)

Wnioski z twierdzenia Churcha-Rossera

(2)Każdy term ma co najwyżej jedną postać normalną (i do niej się redukuje).

Dowód:

JeśliM =_β N i N normalne, to M β Q_β N. SkoroN normalne, to N = Q.

JeśliM też normalne, to M = Q = N.

◦

(44)

Wnioski z twierdzenia Churcha-Rossera

(3)Beta-konwersja jest niesprzeczną teorią równościową

Dowód: Na przykład 0 x = y, ponieważ x 6=_β y.

◦

(45)

Wnioski z twierdzenia Churcha-Rossera

(3)Beta-konwersja jest niesprzeczną teorią równościową

Dowód: Na przykład 0 x = y, ponieważ x 6=_β y.

◦

(46)

Eta-redukcja

(47)

Eta-reduction

The least relation →_η, satisfying the conditions:

I λx .Mx →_η M, when x 6∈FV(M);

I jeśli M →_η M⁰, to MN →_η M⁰N, NM →_η NM⁰ oraz λxM →_η λxM⁰.

Symbol→_βη stands for the union of relations →β and →η. Other definitions and notation are applicable respectively.

◦

(48)

Eta-reduction

The least relation →_η, satisfying the conditions:

I λx .Mx →_η M, when x 6∈FV(M);

I jeśli M →_η M⁰, to MN →_η M⁰N, NM →_η NM⁰ oraz λxM →_η λxM⁰.

Symbol→_βη stands for the union of relations →β and →η. Other definitions and notation are applicable respectively.

◦

(49)

Eta-conversion

Axiom (η): λx .Mx = M, when x 6∈FV(M).

Rule (ext): Mx = Nx

M = N (when x 6∈FV(M) ∪FV(N))

Fakt

Axiom (η) and rule (ext) are equivalent.

Proof.

(1) Assume (η) and let Mx = Nx. Then λx Mx = λx Nx, by rule (ξ), whence M = N.

(2) Since(λx .Mx )x = Mx, one has λx .Mx = M by (ext).

◦

(50)

Eta-conversion

Rule (ext): Mx = Nx

Fakt

Proof.

◦

(51)

Eta-conversion

Rule (ext): Mx = Nx

Fakt

Proof.

◦

(52)

Eta-conversion

Rule (ext): Mx = Nx

Fakt

Proof.

◦

(53)

Eta-conversion

Rule (ext): Mx = Nx

Fakt

Proof.

◦

(54)

Ekstensjonalność i słaba ekstensjonalność

(ext) Mx = Nx

JeśliM = λx P i N = λx Q, to wystarczy: (ξ) P = Q

λx P = λx Q

Słaba ekstensjonalność dla zbiorów to taka zasada

` W (x) ↔ V (x) {x | W (x)} = {x | V (x)}

◦

(55)

Ekstensjonalność i słaba ekstensjonalność

(ext) Mx = Nx

M = N (when x 6∈FV(M) ∪FV(N)) JeśliM = λx P i N = λx Q, to wystarczy:

(ξ) P = Q λx P = λx Q

Słaba ekstensjonalność dla zbiorów to taka zasada

` W (x) ↔ V (x) {x | W (x)} = {x | V (x)}

◦

(56)

Eta-reduction graphically

λ

@

=⇒ M

M •

bb

Eta-reduction amounts to removing a small loop in a graph.

◦

(57)

Eta-reduction

Fakt

Eta-reduction is strongly normalizing.

Proof.

Because terms shrink under eta.

Fakt

Eta-reduction is Church-Rosser.

Proof.

Because it is WCR (easy), Newman’s lemma applies.

◦

(58)

Eta-reduction

Fakt

Proof.

Fakt

Proof.

◦

(59)

Eta-reduction

Fakt

Proof.

Fakt

Proof.

◦

(60)

Eta-reduction

Fakt

Proof.

Fakt

Proof.

◦

(61)

Beta-eta-redukcja

Relacja →_βη to suma →_β i →_η.

Notacja^βη, =_βη itd. stosuje się odpowiednio.

◦

(62)

Beta-eta critical pairs

@

|

λ

[λ]

[@]

|

@

}}

λ

•

dd

•

cc

(λx Mx )N λx (λy M)x

Critical pair occurs when two redexes use the same resource. Proving WCR amounts to resolving critical pairs.

◦

(63)

Beta-eta critical pairs

@

|

λ

[λ]

[@]

|

@

}}

λ

•

dd

•

cc

Critical pair occurs when two redexes use the same resource. Proving WCR amounts to resolving critical pairs.

◦

(64)

Beta-eta critical pairs

@

|

λ

[λ]

[@]

|

@

}}

λ

•

dd

•

cc

Critical pair occurs when two redexes use the same resource.

Proving WCR amounts to resolving critical pairs.

◦

(65)

Beta-eta critical pairs

@

|

λ

[λ]

[@]

|

@

}}

λ

•

dd

•

cc

Critical pair occurs when two redexes use the same resource.

Proving WCR amounts to resolving critical pairs.

◦

(66)

Beta-eta critical pairs

(λx Mx )N → MN

λx (λy M)x → λy M = λx . M[y := x ]

Morał

Beta-eta reduction is weakly Church-Rosser.

◦

(67)

Beta-eta critical pairs

(λx Mx )N → MN

Morał

◦

(68)

Beta-eta critical pairs

(λx Mx )N → MN

Morał

◦

(69)

Towards Church-Rosser

Lemma

If P_η← M →_β Q then there is N such that P →⁼_β N _η Q.

M

η

β

P

β

=

Q

η

N

◦

(70)

Towards Church-Rosser

Lemma

Relations β and η commute:

if Pη M β Q then there is N such that P β N _η Q.

M

η

β

P

β

Q

η

N

◦

(71)

Beta-eta is Church-Rosser

M1 β

η // //.

β

β // //.

β

η // //M2

β

.

η

η // //.

η

β // //.

η

η // //.

η

M₃ _η ^{// //}.

β // //. _η ^{// //}M₄

◦

(72)

Beta-SN versus beta-eta-SN

Theorem 0: A term is βη-SN if and only if it is β-SN.

Proof: (⇒) Obvious.

(⇐) Ćwiczenia?

◦

(73)

Eta-postponement (odkładanie eta-redukcji)

Theorem 1: If M βη N then M β P η N, for some P.

Theorem 2:

A term has a β-normal form iff it has a βη-normal form.

Proofs: Omitted.

Uwaga: Thm. 2 nie wynika natychmiast z Thm. 1.

◦

(74)

Eta-postponement (odkładanie eta-redukcji)

Theorem 2:

Proofs: Omitted.

◦

(75)

Eta-postponement (odkładanie eta-redukcji)

Theorem 2:

Proofs: Omitted.

◦

(76)

Standaryzacja

(77)

Standard reduction:

Never reduce to the left of something already reduced.

Standard reduction:

(λx .xx )((λzy .z(zy ))(λu.u)(λw .w )) → (λx .xx )((λy .(λu.u)((λu.u)y ))(λw .w )) → (λx .xx )((λu.u)((λu.u)(λw .w ))) →

(λx .xx )((λu.u)(λw .w )) → (λx .xx )(λw .w ).

Non-standard reduction:

(λx .xx )((λzy .z(zy ))(λu.u)(λw .w )) → (λx .xx )((λy .(λu.u)((λu.u)y ))(λw .w )) → (λx .xx )((λy .(λu.u)y)(λw .w )) →

(λx .xx )((λy .y )(λw .w )) → (λx .xx )(λw .w ).

◦

(78)

Standardization

Theorem:

If M β N then there is a standard reduction from M to N.

Corollary:

If M has a β-normal form then theleftmost reduction leads to the normal form.

Slogan:

The leftmostreduction strategy is normalizing.

◦

(79)

Standardization

Theorem:

Corollary:

Slogan:

◦

(80)

Standardization

Theorem:

Corollary:

Slogan:

◦

(81)

Redukcje czołowe i wewnętrzne

A term λ~x .z ~R is in head normal form.¹

A term λ~x .(λy .P)Q ~R has a head redex (λy .P)Q.

A reduction step of the form

M = λ~x .(λy .P)Q ~R →_β λ~x .P[y := Q] ~R = N is calledhead reduction. Write M → N.^h

Other reductions areinternal. Write M → N.ⁱ

◦

1Postać normalna jest wtedy, gdy ~R są normalne.

(82)

Redukcje czołowe i wewnętrzne

A term λ~x .z ~R is in head normal form.¹

A term λ~x .(λy .P)Q ~R has a head redex (λy .P)Q.

A reduction step of the form

M = λ~x .(λy .P)Q ~R →β λ~x .P[y := Q] ~R = N is calledhead reduction. Write M → N.^h

Other reductions areinternal. Write M → N.ⁱ

◦

1Postać normalna jest wtedy, gdy ~R są normalne.

(83)

Main Lemma

Lemma: If M β N then M P^h N, for some P.ⁱ

Warning: A naive proof attempt fails. The assumption: λ~x .(λy .P)Q ~R λ~x.(λy .Pⁱ ⁰)Q⁰R~^{0 h}→ λ~x .P⁰[y := Q⁰] ~R⁰ does not imply

λ~x .(λy .P)Q ~R → λ~^h x .P[y := Q] ~R λ~x.Pⁱ ⁰[y := Q⁰] ~R⁰. This diagram is wrong. ·

h

·

i @@ @@

h

·

i @@ @@

◦

(84)

Main Lemma

Lemma: If M β N then M P^h N, for some P.ⁱ Warning: A naive proof attempt fails. The assumption:

λ~x .(λy .P)Q ~R λ~x.(λy .Pⁱ ⁰)Q⁰R~^{0 h}→ λ~x .P⁰[y := Q⁰] ~R⁰ does not imply

λ~x .(λy .P)Q ~R → λ~^h x .P[y := Q] ~R λ~x.Pⁱ ⁰[y := Q⁰] ~R⁰.

This diagram is wrong. ·

h

·

i @@ @@

h

·

i @@ @@

◦

(85)

Main Lemma

Lemma: If M β N then M P^h N, for some P.ⁱ Warning: A naive proof attempt fails. The assumption:

λ~x .(λy .P)Q ~R λ~x.(λy .Pⁱ ⁰)Q⁰R~^{0 h}→ λ~x .P⁰[y := Q⁰] ~R⁰ does not imply

λ~x .(λy .P)Q ~R → λ~^h x .P[y := Q] ~R λ~x.Pⁱ ⁰[y := Q⁰] ~R⁰. This diagram is wrong. ·

h

·

i @@ @@

h

·

i @@ @@

◦

(86)

Dygresja

Lemat łatwy:

Jeśli M Nⁱ → P, to M^h → Q ^h β P, dla pewnego Q.

Wniosek: If M has a reduction with infinitely many head steps then it has an infinite head reduction.

◦

(87)

Dygresja

Lemat łatwy:

Jeśli M Nⁱ → P, to M^h → Q ^h β P, dla pewnego Q.

Wniosek: If M has a reduction with infinitely many head steps then it has an infinite head reduction.

◦

(88)

Standaryzacja: jeśli M ^β N, to istnieje standardowa redukcja

Lemma: If M β N then M P^h Nⁱ , for some P.

(Dowód lematu opuszczamy)

Dowód standaryzacji: Indukcja ze względu na długość N. Najpierw wykonujemy same redukcje czołowe. Dostajemy termP = λ~x . M1M2. . . Mk, i dalej wszystkie redukcje są wewnątrz termówM₁, M₂, . . . , M_k. Można je łatwo

przepermutować tak, aby najpierw redukować wewnątrzM₁, potem wewnątrzM2 i tak dalej. Do tych redukcji można zastosować indukcję.

◦

(89)

◦

(90)

◦

(91)

Redukcje quasi-lewostronne

Lemma: If M has a reduction with infinitely many head steps then it has an infinite head reduction.

Uogólnienie:

Aquasi-leftmost reduction is an infinite reduction sequence with infinitely many leftmost steps.

◦

(92)

Redukcje quasi-lewostronne

Lemma: If M has a reduction with infinitely many head steps then it has an infinite head reduction.

Uogólnienie:

Aquasi-leftmost reduction is an infinite reduction sequence with infinitely many leftmost steps.

◦

(93)

Redukcje quasi-lewostronne

Theorem: A normalizing term has no quasi-leftmost reduction sequence.

Proof: Induction wrt the length of the normal form ofM. SupposeM has a quasi-leftmost reduction. If there is infinitely many head steps, thenM has an infinite head (thus leftmost) reduction and cannot normalize.

Thus almost all reductions are internal. (W szczególności, od pewnego miejsca mamy czołowe postaci normalne.)

λ~z.yP₁. . . P_k → λ~ⁱ z.yP₁⁰. . . P_k⁰ → λ~ⁱ z.yP₁⁰⁰. . . P_k⁰⁰→ · · ·ⁱ Infinitely many leftmost steps are within the sameP_i. By induction,P_i cannot normalize.

But thenM cannot normalize.

◦

(94)

Redukcje quasi-lewostronne

λ~z.yP₁. . . P_k → λ~ⁱ z.yP₁⁰. . . P_k⁰ → λ~ⁱ z.yP₁⁰⁰. . . P_k⁰⁰→ · · ·ⁱ Infinitely many leftmost steps are within the sameP_i. By induction,P_i cannot normalize.

◦

(95)

Redukcje quasi-lewostronne

λ~z.yP₁. . . P_k → λ~ⁱ z.yP₁⁰. . . P_k⁰ → λ~ⁱ z.yP₁⁰⁰. . . P_k⁰⁰→ · · ·ⁱ

Infinitely many leftmost steps are within the sameP_i. By induction,P_i cannot normalize.

◦

(96)

Redukcje quasi-lewostronne

λ~z.yP₁. . . P_k → λ~ⁱ z.yP₁⁰. . . P_k⁰ → λ~ⁱ z.yP₁⁰⁰. . . P_k⁰⁰→ · · ·ⁱ Infinitely many leftmost steps are within the sameP_i.

By induction,P_i cannot normalize. But thenM cannot normalize.

◦

(97)

Redukcje quasi-lewostronne

λ~z.yP₁. . . P_k → λ~ⁱ z.yP₁⁰. . . P_k⁰ → λ~ⁱ z.yP₁⁰⁰. . . P_k⁰⁰→ · · ·ⁱ Infinitely many leftmost steps are within the sameP_i. By induction,Pi cannot normalize.

◦

(98)

Redukcje quasi-lewostronne

λ~z.yP₁. . . P_k → λ~ⁱ z.yP₁⁰. . . P_k⁰ → λ~ⁱ z.yP₁⁰⁰. . . P_k⁰⁰→ · · ·ⁱ Infinitely many leftmost steps are within the sameP_i. By induction,Pi cannot normalize.

◦