Rachunek lambda

(1)

Rachunek lambda

11 marca 2013

(2)

Zbiory

i funkcje

Sposób u»ycia:

a ∈ A (nale»enie)

F (a) (aplikacja) Tworzenie:

{x | W (x)} (wycinanie)

λx W (x) (abstrakcja)

Ewaluacja:

a ∈ {x | W (x)} ⇔ W (a)

(λx W (x))(a) = W (a)

◦

(3)

Zbiory

i funkcje

Sposób u»ycia:

F (a) (aplikacja)

Tworzenie:

λx W (x) (abstrakcja) Ewaluacja:

a ∈ {x | W (x)} ⇔ W (a)

(λx W (x))(a) = W (a)

◦

(4)

Zbiory

i funkcje

Sposób u»ycia:

F (a) (aplikacja)

Tworzenie:

Ewaluacja:

a ∈ {x | W (x)} ⇔ W (a)

(λx W (x))(a) = W (a)

◦

(5)

Zbiory i funkcje

Sposób u»ycia:

a ∈ A (nale»enie) F (a) (aplikacja)

Tworzenie:

Ewaluacja:

a ∈ {x | W (x)} ⇔ W (a)

(λx W (x))(a) = W (a)

◦

(6)

Zbiory i funkcje

Sposób u»ycia:

Tworzenie:

{x | W (x)} (wycinanie) λx W (x) (abstrakcja) Ewaluacja:

a ∈ {x | W (x)} ⇔ W (a)

(λx W (x))(a) = W (a)

◦

(7)

Zbiory i funkcje

Sposób u»ycia:

Tworzenie:

{x | W (x)} (wycinanie) λx W (x) (abstrakcja) Ewaluacja:

a ∈ {x | W (x)} ⇔ W (a) (λx W (x))(a) = W (a)

◦

(8)

Ekstensjonalno±¢ (?)

Dla zbiorów (niew¡tpliwa):

A = B wtedy i tylko wtedy, gdy ∀x (x ∈ A ⇔ x ∈ B)

A = {x | x ∈ A}

Dla funkcji(w¡tpliwa):

F = G wtedy i tylko wtedy, gdy ∀x (F (x) = G(x))

F = λx Fx (¹)

◦

1Gdy F nie zawiera x.

(9)

Ekstensjonalno±¢ (?)

A = {x | x ∈ A}

F = λx Fx (¹)

◦

(10)

Ekstensjonalno±¢ (?)

A = {x | x ∈ A}

F = λx Fx (¹)

◦

(11)

Ekstensjonalno±¢ (?)

A = {x | x ∈ A}

F = λx Fx (¹)

1Gdy F nie zawiera x. ◦

(12)

Ekstensjonalno±¢ (?)

Statyczne i dynamiczne rozumienie funkcji:

1. Jako przyporz¡dkowanie, wykres, relacj¦, zbiór par. . . 2. Jako reguª¦, przeksztaªcenie, algorytm, metod¦. . . Teoria zbiorów nie nadaje si¦ do opisu aspektu (2).

◦

(13)

Ekstensjonalno±¢ (?)

1. Jako przyporz¡dkowanie, wykres, relacj¦, zbiór par. . .

2. Jako reguª¦, przeksztaªcenie, algorytm, metod¦. . . Teoria zbiorów nie nadaje si¦ do opisu aspektu (2).

◦

(14)

Ekstensjonalno±¢ (?)

1. Jako przyporz¡dkowanie, wykres, relacj¦, zbiór par. . . 2. Jako reguª¦, przeksztaªcenie, algorytm, metod¦. . .

Teoria zbiorów nie nadaje si¦ do opisu aspektu (2).

◦

(15)

Ekstensjonalno±¢ (?)

1. Jako przyporz¡dkowanie, wykres, relacj¦, zbiór par. . . 2. Jako reguª¦, przeksztaªcenie, algorytm, metod¦. . . Teoria zbiorów nie nadaje si¦ do opisu aspektu (2).

◦

(16)

Beztypowy rachunek lambda

I Funkcja rozumiana jako dziaªanie.

I Przedmiotem dziaªania mo»e by¢ cokolwiek, zatem. . .

I . . . funkcja nie ma a priori ograniczonej dziedziny.

I Funkcja mo»e by¢ np. aplikowana sama do siebie.

I Ka»demu obiektowi mo»na przypisa¢ dziaªanie, wi¦c. . .

I . . . nie ma innych obiektów ni» funkcje.

Analogia: Ka»dy ci¡g bitów mo»na zinterpretowa¢

jako program;

jako dane.

◦

(17)

Beztypowy rachunek lambda

jako program;

jako dane.

◦

(18)

Beztypowy rachunek lambda

jako program;

jako dane.

◦

(19)

Beztypowy rachunek lambda

jako program;

jako dane.

◦

(20)

Beztypowy rachunek lambda

jako program;

jako dane.

◦

(21)

Beztypowy rachunek lambda

jako program;

jako dane.

◦

(22)

Beztypowy rachunek lambda

jako program;

jako dane.

◦

(23)

Skªadnia: lambda-wyra»enia

Lambda-wyra»enia:

Zmienne x,y, z, . . .

Aplikacje (MN);

Abstrakcje (λx M).

Konwencje:

Opuszczamy zewn¦trzne nawiasy;

Aplikacja wi¡»e w lewo: MNP oznacza (MN)P

Skrót z kropk¡: λx1. . .xn.M oznaczaλx1(. . . (λxnM) · · · ).

◦

(24)

Skªadnia: lambda-wyra»enia

Lambda-wyra»enia:

Zmienne x,y, z, . . .

Aplikacje (MN);

Abstrakcje (λx M).

Konwencje:

Opuszczamy zewn¦trzne nawiasy;

Aplikacja wi¡»e w lewo: MNP oznacza (MN)P

Skrót z kropk¡: λx1. . .xn.M oznaczaλx1(. . . (λxnM) · · · ).

◦

(25)

Przykªady

I = λx.x

K = λxy.x

S = λxyz.xz(yz) 2 = λfx. f (fx) ω = λ x.xx Ω = ωω

Y = λf ((λx.f (xx))(λx.f (xx))

◦

(26)

Przykªady

I = λx.x K = λxy.x

S = λxyz.xz(yz) 2 = λfx. f (fx) ω = λ x.xx Ω = ωω

Y = λf ((λx.f (xx))(λx.f (xx))

◦

(27)

Przykªady

I = λx.x K = λxy.x

S = λxyz.xz(yz)

2 = λfx. f (fx) ω = λ x.xx Ω = ωω

Y = λf ((λx.f (xx))(λx.f (xx))

◦

(28)

Przykªady

I = λx.x K = λxy.x

S = λxyz.xz(yz) 2 = λfx. f (fx)

ω = λ x.xx Ω = ωω

Y = λf ((λx.f (xx))(λx.f (xx))

◦

(29)

Przykªady

I = λx.x K = λxy.x

S = λxyz.xz(yz) 2 = λfx. f (fx) ω = λ x.xx

Ω = ωω

Y = λf ((λx.f (xx))(λx.f (xx))

◦

(30)

Przykªady

I = λx.x K = λxy.x

S = λxyz.xz(yz) 2 = λfx. f (fx) ω = λ x.xx Ω = ωω

Y = λf ((λx.f (xx))(λx.f (xx))

◦

(31)

Przykªady

I = λx.x K = λxy.x

S = λxyz.xz(yz) 2 = λfx. f (fx) ω = λ x.xx Ω = ωω

Y = λf ((λx.f (xx))(λx.f (xx))

◦

(32)

Zmienne wolne (globalne)

FV(x) = {x};

FV(MN) = FV(M) ∪FV(N);

FV(λx M) =FV(M) − {x}.

Na przykªad:

FV(λx x) = ∅; FV(λx. xy) = {y};

FV((λx. xy)(λy. xy)) = {x, y}.

◦

(33)

Zmienne wolne (globalne)

FV(x) = {x};

Na przykªad:

FV(λx x) = ∅;

FV(λx. xy) = {y};

◦

(34)

Zmienne wolne (globalne)

FV(x) = {x};

Na przykªad:

FV(λx x) = ∅;

FV(λx. xy) = {y};

◦

(35)

Zmienne wolne (globalne)

FV(x) = {x};

Na przykªad:

FV(λx x) = ∅;

FV(λx. xy) = {y};

◦

(36)

Alfa-konwersja

Wyra»enia λx. xy i λz. zy oznaczaj¡ t¦ sam¡ operacj¦

(zaaplikuj dany argument do y).

Nale»y je uwa»a¢ za identyczne.

Alfa-konwersja: Wyra»enia ró»ni¡ce si¦ tylko wyborem zmiennych zwi¡zanych uto»amiamy.

Lambda-termy to klasy abstrakcji tego uto»samienia.

atwiej powiedzie¢, ni» zrobi¢. . .

◦

(37)

Alfa-konwersja

◦

(38)

Alfa-konwersja

◦

(39)

Alfa-konwersja

◦

(40)

Termy jako grafy:

x y

@

G

Jeden wierzchoªek pocz¡tkowy;

Zmienne wolne jako wierzchoªki ko«cowe (li±cie).

◦

(41)

Termy jako grafy: zmienna

x

◦

(42)

Termy jako grafy: aplikacja

◦

(43)

Termy jako grafy: abstrakcja

◦

(44)

Termy jako grafy: abstrakcja

Zmienne zwi¡zane sa niepotrzebne.

◦

(45)

Przykªad

λ

@

mmmmmmmm QQQQQQQQQ

λ @

{{{{ BBBB

@

|||| BBBB λ ◦

oo

◦

33

◦

hh

@

zzzz DDDD

◦

66

y

To jest graf termu λx.(λy. xy)((λz. zy)x)

◦

(46)

Podstawienie G[x := T ]

Podstawienie termu T do termu G w miejsce wolnych wyst¡pie« zmiennej x.

A

A A

A

A A

A

x x

@

G

T T

◦

(47)

Podstawienie G[x := T ]

Podstawienie termu T do termu G w miejsce wolnych wyst¡pie« zmiennej x.

A

A A

A

A A

A

x x

@

G

T T

◦

(48)

Podstawienie

I x[x := N] = N;

I y[x := N] = y,

gdy y jest zmienn¡ ró»n¡ od x;

I (PQ)[x := N] = P[x := N]Q[x := N];

I (λy P)[x := N] = λy.P[x := N],

gdy y 6= x oraz y 6∈FV(N).

Wykonanie podstawienia na konkretnej reprezentacji termu mo»e wymaga¢ wymiany zmiennych:

(λy P)[x := N] = λz P[y := z][x := N], gdzie z jest nowe.

◦

(49)

Podstawienie

I x[x := N] = N;

I y[x := N] = y,

I (PQ)[x := N] = P[x := N]Q[x := N];

I (λy P)[x := N] = λy.P[x := N],

◦

(50)

Podstawienie

I x[x := N] = N;

I y[x := N] = y,

I (PQ)[x := N] = P[x := N]Q[x := N];

I (λy P)[x := N] = λy.P[x := N],

◦

(51)

Podstawienie

I x[x := N] = N;

I y[x := N] = y,

I (PQ)[x := N] = P[x := N]Q[x := N];

I (λy P)[x := N] = λy.P[x := N],

◦

(52)

Podstawienie

I x[x := N] = N;

I y[x := N] = y,

I (PQ)[x := N] = P[x := N]Q[x := N];

I (λy P)[x := N] = λy.P[x := N],

◦

(53)

Podstawienie

I x[x := N] = N;

I y[x := N] = y,

I (PQ)[x := N] = P[x := N]Q[x := N];

I (λy P)[x := N] = λy.P[x := N],

◦

(54)

Podstawienie

I x[x := N] = N;

I y[x := N] = y,

I (PQ)[x := N] = P[x := N]Q[x := N];

I (λy P)[x := N] = λy.P[x := N],

◦

(55)

Lemat o podstawieniu

M[x := N][y := R] = M[y := R][x := N[y := R]]

gdy x 6∈FV(R) lub y 6∈FV(M)

x y

x

@

M

y y

A A A A AA

N N

AA AA

A

◦

(56)

Beta-redukcja

Najmniejsza relacja →β, speªniaj¡ca warunki:

I (λxP)Q →β P[x := Q];

I je±li M →β M⁰, to:

MN →β M⁰N, NM →β NM⁰ oraz λxM →β λxM⁰.

Term postaci (λxP)Q to β-redeks.

Relacja →β to zredukowanie jednego dowolnego redeksu.

◦

(57)

Beta-redukcja

◦

(58)

Beta-redukcja

◦

(59)

Relacje pochodne:

Dowolna liczba kroków: β lub →^∗_β; Niezerowa liczba kroków: →⁺_β;

Co najwy»ej jeden krok: →⁼_β;

Równowa»no±¢ (beta-konwersja): =_β.

◦

(60)

Przykªad: SKK =

^β

I

SKK = (λxyz.xz(yz))(λxy.x)(λxy.x)

→

_β

(λ yz.(λxy.x)z(yz))(λxy.x)

→

_β

λ z.(λxy.x)z((λxy.x)z)

→

_β

λ z.(λy.z)((λxy.x)z)

→

_β

λ z.(λy.z)(λy.z)

→

_β

λ z.z = I

◦

(61)

Przykªad: SKK =

^β

I

SKK = (λx yz.x z(yz)) (λ xy.x) (λ xy.x)

→

_β

(λ yz.(λxy.x)z(yz))(λxy.x)

→

_β

λ z.(λxy.x)z((λxy.x)z)

→

_β

λ z.(λy.z)((λxy.x)z)

→

_β

λ z.(λy.z)(λy.z)

→

_β

λ z.z = I

◦

(62)

Przykªad: SKK =

^β

I

SKK = (λx yz.x z(yz)) (λ xy.x) (λ xy.x)

→

_β

(λ yz.(λxy.x)z(yz))(λxy.x)

→

_β

λ z.(λxy.x)z((λxy.x)z)

→

_β

λ z.(λy.z)((λxy.x)z)

→

_β

λ z.(λy.z)(λy.z)

→

_β

λ z.z = I

◦

(63)

Przykªad: SKK =

^β

I

SKK = (λxyz.xz(yz))(λxy.x)(λxy.x)

→

_β

(λ y z.(λxy.x)z(y z)) (λ xy.x)

→

_β

λ z.(λxy.x)z((λxy.x)z)

→

_β

λ z.(λy.z)((λxy.x)z)

→

_β

λ z.(λy.z)(λy.z)

→

_β

λ z.z = I

◦

(64)

Przykªad: SKK =

^β

I

SKK = (λxyz.xz(yz))(λxy.x)(λxy.x)

→

_β

(λ y z.(λxy.x)z(y z)) (λ xy.x)

→

_β

λ z.(λxy.x)z((λxy.x)z)

→

_β

λ z.(λy.z)((λxy.x)z)

→

_β

λ z.(λy.z)(λy.z)

→

_β

λ z.z = I

◦

(65)

Przykªad: SKK =

^β

I

SKK = (λxyz.xz(yz))(λxy.x)(λxy.x)

→

_β

(λ yz.(λxy.x)z(yz))(λxy.x)

→

_β

λ z.(λx y.x ) z ((λ xy.x)z)

→

_β

λ z.(λy.z)((λxy.x)z)

→

_β

λ z.(λy.z)(λy.z)

→

_β

λ z.z = I

◦

(66)

Przykªad: SKK =

^β

I

SKK = (λxyz.xz(yz))(λxy.x)(λxy.x)

→

_β

(λ yz.(λxy.x)z(yz))(λxy.x)

→

_β

λ z.(λx y.x ) z ((λ xy.x)z)

→

_β

λ z.(λy.z)((λxy.x)z)

→

_β

λ z.(λy.z)(λy.z)

→

_β

λ z.z = I

◦

(67)

Przykªad: SKK =

^β

I

SKK = (λxyz.xz(yz))(λxy.x)(λxy.x)

→

_β

(λ yz.(λxy.x)z(yz))(λxy.x)

→

_β

λ z.(λxy.x)z((λxy.x)z)

→

_β

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

→

_β

λ z.(λy.z)(λy.z)

→

_β

λ z.z = I

◦

(68)

Przykªad: SKK =

^β

I

SKK = (λxyz.xz(yz))(λxy.x)(λxy.x)

→

_β

(λ yz.(λxy.x)z(yz))(λxy.x)

→

_β

λ z.(λxy.x)z((λxy.x)z)

→

_β

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

→

_β

λ z.(λy.z)(λy.z)

→

_β

λ z.z = I

◦

(69)

Przykªad: SKK =

^β

I

SKK = (λxyz.xz(yz))(λxy.x)(λxy.x)

→

_β

(λ yz.(λxy.x)z(yz))(λxy.x)

→

_β

λ z.(λxy.x)z((λxy.x)z)

→

_β

λ z.(λy.z)((λxy.x)z)

→

_β

λ z.(λy . z) (λ y.z)

→

_β

λ z.z = I

◦

(70)

Przykªad: SKK =

^β

I

SKK = (λxyz.xz(yz))(λxy.x)(λxy.x)

→

_β

(λ yz.(λxy.x)z(yz))(λxy.x)

→

_β

λ z.(λxy.x)z((λxy.x)z)

→

_β

λ z.(λy.z)((λxy.x)z)

→

_β

λ z.(λy . z) (λ y.z)

→

_β

λ z.z = I

◦

(71)

Jaja aligatorów

http://worrydream.com/AlligatorEggs/

(72)

Rachunek lambda jako teoria równo±ciowa

Termy M i N s¡ beta-równe (M =β N) wtedy i tylko wtedy, gdy równo±¢ M = N mo»na udowodni¢ w systemie:

(β) (λx M)N = M[x := N] x = x M = N

MP = NP

M = N

PM = PN (ξ) M = N

λx M = λx N M = N

N = M

M = N, N = P M = P

◦

(73)

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.

◦

(74)

Normalizacja

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

◦

(75)

Normalizacja

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

◦

(76)

Normalizacja

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

◦

(77)

Normalizacja

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

◦

(78)

Normalizacja

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

◦

(79)

Przykªady

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

I Term SKK jest 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.

◦

(80)

Przykªady

I Term SKKjest silnie normalizowalny i ma posta¢

normaln¡ I.

◦

(81)

Przykªady

normaln¡ I.

◦

(82)

Przykªady

normaln¡ I.

◦

(83)

Woªanie przez nazw¦

(λx P)Q →β P[x := Q]

Ewaluacja procedury o parametrze formalnymx i tre±ciP, gdy parametrem aktualnym jestQ:

Nale»y wstawi¢ parametr aktualny do tre±ci procedury, wymieniaj¡c, je±li trzeba, lokalne identykatory na nowe.

◦

(84)

Woªanie przez nazw¦

◦

(85)

Woªanie przez nazw¦

Nale»y wstawi¢ parametr aktualny do tre±ci procedury,

wymieniaj¡c, je±li trzeba, lokalne identykatory na nowe.

◦

(86)

Woªanie przez nazw¦

◦

(87)

Beta-redeks w grae

(1)

@

| >>>>>>

λ

(3)

(2)

◦

(88)

Beta-redukcja w grae

(1)

@

| >>>>>>

λ

(3)

(2)

◦

77

◦

hh

=⇒ (1)

(2)

(3) (3)

◦

(89)

Beta-redukcja nieco wyidealizowana

(1)

@

| >>>>>>

λx

(4)

(3)

@@

(2)

=⇒ (1)

(4)

(3)

&&

(2)

◦

(90)

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

◦

(91)

Wªasno±¢ Churcha-Rossera (CR)

Je±li a b i a c, to istnieje takie d, »e b d i c d.

a

?

??

b

?

??

? c

d

◦

(92)

Wªasno±¢ Churcha-Rossera (CR)

Je±li a b i a c, to istnieje takie d, »e b d i c d.

a

?

??

b

?

??

? c

d

◦

(93)

Twierdzenie Churcha-Rossera: Beta ma wªasno±¢ CR

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.

◦

(94)

Twierdzenie Churcha-Rossera: Beta ma wªasno±¢ CR

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.

◦

(95)

Peªne rozwini¦cie

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.

◦

(96)

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^•.

◦

(97)

Wªasno±ci relacji →

¹

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

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

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

◦

(98)

Wªasno±ci relacji →

¹

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

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

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

◦

(99)

Wªasno±ci relacji →

¹

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

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

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

◦

(100)

Relacja →

¹

ma wªasno±¢ rombu

M

1

~~}}}}}}}} ₁

B!!B BB BB BB

M⁰

1AA A

A M⁰⁰

~~|||1|

M^•

◦

(101)

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₂

.

//.

M3 //. //. //M4

2) Poniewa»→_β ⊆→ ⊆ ¹ β, wi¦c ¹ i β s¡ równe. 3) Wªasno±¢ rombu dla^β to wªasno±¢ CR dla →β.

◦

(102)

Dowód twierdzenia Churcha-Rossera

M₁

//.

//M₂

.

//.

M3 //. //. //M4

2) Poniewa»→_β ⊆→ ⊆ ¹ β, wi¦c ¹ i β s¡ równe. 3) Wªasno±¢ rombu dla^β to wªasno±¢ CR dla →β.

◦

(103)

Dowód twierdzenia Churcha-Rossera

M₁

//.

//M₂

.

//.

M3 //. //. //M4

2) Poniewa»→_β ⊆→ ⊆ ¹ β, wi¦c ¹ i ^β s¡ równe.

3) Wªasno±¢ rombu dla^β to wªasno±¢ CR dla →β.

◦

(104)

Dowód twierdzenia Churcha-Rossera

M₁

//.

//M₂

.

//.

M3 //. //. //M4

2) Poniewa»→_β ⊆→ ⊆ ¹ β, wi¦c ¹ i ^β s¡ równe.

3) Wªasno±¢ rombu dla^β to wªasno±¢ CR dla →β.

◦

(105)

Wnioski z twierdzenia Churcha-Rossera

(1)Je±li M =β N, toM β Qβ N, dla pewnego Q.

Q1

?? ? Q2

?? ? Qn

}}}}{{{{

?

??

M

?

? M1

"" ""E EE EE EE EE

E M2 . . . Mn−1 N

{{{{w ww ww ww ww ww

•

"" ""E EE EE EE EE E

•

◦

(106)

Wnioski z twierdzenia Churcha-Rossera

(1)Je±li M =β N, toM β Qβ N, dla pewnego Q.

Q1

?? ? Q2

?? ? Qn

}}}}{{{{

?

??

M

?

? M1

"" ""E EE EE EE EE

E M2 . . . Mn−1 N

{{{{w ww ww ww ww ww

•

"" ""E EE EE EE EE E

•

◦

(107)

Wnioski z twierdzenia Churcha-Rossera

(2)Ka»dy term ma co najwy»ej jedn¡ posta¢ normaln¡

(i do niej si¦ redukuje).

Dowód:

Je±li M =β N i N normalne, to M β Qβ N. Skoro N normalne, to N = Q.

Je±li M te» normalne, to M = Q = N.

◦

(108)

Wnioski z twierdzenia Churcha-Rossera

(2)Ka»dy term ma co najwy»ej jedn¡ posta¢ normaln¡

(i do niej si¦ redukuje).

Dowód:

Je±li M =β N i N normalne, to M β Qβ N.

Skoro N normalne, to N = Q.

Je±li M te» normalne, to M = Q = N.

◦

(109)

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.

◦

(110)

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.

◦

(111)

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⁰ and λxM →η λxM⁰.

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

◦

(112)

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⁰ and λxM →η λxM⁰.

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

◦

(113)

Eta-reduction

Fakt

Eta-reduction is strongly normalizing (because terms shrink under eta).

Fakt

Beta-eta-reduction is Church-Rosser.

◦

(114)

Eta-reduction

Fakt

Eta-reduction is strongly normalizing (because terms shrink under eta).

Fakt

Beta-eta-reduction is Church-Rosser.

◦

(115)

Standardization

Standard reduction: Always reduce the leftmost redex.

Theorem:

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

Slogan:

The leftmostreduction strategy is normalizing.

◦

(116)

Standardization

Standard reduction: Always reduce the leftmost redex.

Theorem:

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

Slogan:

The leftmostreduction strategy is normalizing.

◦

(117)

Head normalization

A term λ~x.z~R is inhead normal form.

A term λ~x.(λy.P)Q~R has ahead 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 →^h N.

Other reductions areinternal. Write M →ⁱ N.

◦

(118)

Head normalization

A term λ~x.z~R is inhead normal form.

A term λ~x.(λy.P)Q~R has ahead 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 →^h N.

Other reductions areinternal. Write M →ⁱ N.

◦

(119)

Main Lemma

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

Warning: A naive proof attempt fails. This diagram is wrong.

·

h

<

<<

·

i@@ @@

h

<

<<

< ·

·

i @@ @@

◦

(120)

Main Lemma

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

Warning: A naive proof attempt fails. This diagram is wrong.

·

h

<

<<

·

i@@ @@

h

<

<<

< ·

·

i @@ @@

◦

(121)

Curry's xed point combinator Y

Y = λf ((λx.f (xx))(λx.f (xx))

Fact: YF =β F (YF ), for every F .

Proof: YF →β ((λx.F (xx))(λx.F (xx)) →β

F ((λx.F (xx))(λx.F (xx))β ←F (YF )

◦

(122)

Curry's xed point combinator Y

Y = λf ((λx.f (xx))(λx.f (xx))

◦

(123)

Curry's xed point combinator Y

Y = λf ((λx.f (xx))(λx.f (xx))

◦

(124)

YF =

^β

F (YF )

Example: Find an M such that Mxy =β MxxyM.

Solution: No problem, M = Y(λm λxy. mxxym).

◦

(125)

YF =

^β

F (YF )

Example: Find an M such that Mxy =β MxxyM.

Solution: No problem, M = Y(λm λxy. mxxym).

◦

(126)

Turing's xed-point combinator

Θ = (λ xf . f (xxf ))(λxf . f (xxf ))

Fact: ΘF β F (ΘF ), all F .

Proof: ΘF = (λxf . f (xxf ))(λxf . f (xxf ))F →β

(λf . f ((λxf . f (xxf ))(λxf . f (xxf ))f )F →β

F ((λxf . f (xxf ))(λxf . f (xxf ))F ) = F (ΘF )

◦

(127)

Turing's xed-point combinator

Θ = (λ xf . f (xxf ))(λxf . f (xxf ))

◦

(128)

Turing's xed-point combinator

Θ = (λ xf . f (xxf ))(λxf . f (xxf ))

◦