1 Sk ladnia rachunku lambda

Rachunek lambda

Pawe l Urzyczyn urzy@mimuw.edu.pl 21 wrze´snia 2020, godzina 18: 10

Rachunek lambda i logika kombinatoryczna powsta ly w latach trzydziestych dwudziestego wieku. Poczatkowo mia ly stanowi´_, c alternatywne wobec teorii mnogo´sci podej´scie do pod- staw matematyki, w kt´orym funkcja (rozumiana intensjonalnie jako definicja) by la pojeciem_, pierwotnym. Ten zamiar sie nie powi´_, od l, ale szybko okaza lo sie, ˙ze rachunek lambda jest_, niezwykle u˙zytecznym aparatem w teorii oblicze´n. Definicje funkcji obliczalnej sformu lowano_, wcze´sniej za pomoca rachunku lambda, ni˙z w j_, ezyku maszyn Turinga._,

P´o´zniej, w zwiazku z rozwojem informatyki, j_, ezyk rachunku lambda okaza l si_, e niezast_, apionym_, narzedziem w teorii jezyk´_, ow programowania. A wreszcie i w praktyce, gdy pojawi ly sie jezyki_, programowania funkcyjnego. Dzisiaj znajomo´s´c podstaw rachunku lambda jest niezbednym_, elementem wykszta lcenia nowoczesnego informatyka.

Poprzez zwiazki z logik_, a intuicjonistyczn_, a, rachunek lambda odzyska l te˙z nale˙zne sobie miejsce_, w podstawach matematyki, zw laszcza w teorii dowodu. Dlatego ta tematyka powinna by´c interesujaca tak˙ze dla student´_, ow matematyki zainteresowanych logika._,

Te notatki obejmuja najwa˙zniejsze wiadomo´_, sci z rachunku lambda bez typ´ow i podstawowe informacje o systemach z typami. Zrozumienie ich nie wymaga w zasadzie przygotowania wykraczajacego poza materia l wyk ladany na I roku. Jednak wcze´_, sniejsze wys luchanie wy- k ladu z jezyk´_, ow i automat´ow pozwoli na spojrzenie na pewne zagadnienia z szerszej perspek- tywy.

1 Sk ladnia rachunku lambda

W rachunku lambda rozwa˙zamy obiekty zwane lambda-termami . Tradycyjnie lambda-termy definiowane sa jako formalne wyra˙zenia pewnego j_, ezyka, podobnie jak zwyk le termy w alge-_, brze i logice pierwszego rzedu. Istotna r´_, o˙znica polega na tym, ˙ze lambda-termy pozostajace_, w pewnej relacji r´ownowa˙zno´sci (alfa-konwersji) sa ze sob_, a uto˙zsamiane (uwa˙zane za iden-_, tyczne). A wiec lambda-termy to w istocie nie wyra˙zenia, ale klasy abstrakcji lambda-wyra˙ze´_, n (nazywanych te˙z pre-termami ), kt´ore teraz zdefiniujemy.

Przyjmijmy, ˙ze mamy pewien przeliczalny niesko´nczony zbi´or zmiennych przedmiotowych.

– Zmienne przedmiotowe sa lambda-wyra˙zeniami;_, – Je´sli M i N sa lambda-wyra˙zeniami, to (M N ) te˙z;_,

– Je´sli M jest lambda-wyra˙zeniem i x jest zmienna, to (λxM ) jest lambda-wyra˙zeniem._, Wyra˙zenie postaci (M N ) nazywamy aplikacja, a wyra˙zenie postaci (λxM ) to λ-abstrakcja._, Intuicyjny sens aplikacji (M N ) to zastosowanie operacji M do argumentu N . Abstrakcje_, (λxM ) interpretujemy natomiast jako definicje operacji (funkcji), kt´_, ora argumentowi x przy- pisuje M . Oczywi´scie x mo˙ze wystepowa´_, c w M , tj. M zale˙zy od x. Narzuca sie analogia_, z procedura (funkcj_, a) o parametrze formalnym x i tre´_, sci M .

Stosujemy nastepuj_, ace konwencje notacyjne:_, – opuszczamy zewnetrzne nawiasy;_,

– aplikacja wia˙ze w lewo, tj. M N P oznacza (M N )P ;_, – piszemy λx₁. . . x_n.M zamiast λx₁(. . . (λx_nM ) . . .).

Kropka w wyra˙zeniu λx₁. . . x_n. M oznacza to samo, co ujecie w nawiasy ca lego wyra˙ze-_, nia M . Na przyk lad napis (λx. x(xx))y odczytamy jako ((λx(x(xx)))y). Czasem piszemy niepotrzebne kropki, np. λx. x zamiast λx x.

Operator lambda-abstrakcji λ wia˙ze zmienne, tj. wszystkie wyst_, apienia x w wyra˙zeniu λxM_, uwa˙za sie za zwi_, azane (lokalne). Zmienne wolne (globalne) definiuje si_, e tak:_,

–FV(x) = {x};

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

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

Alfa-konwersja

Wyb´or zmiennych u˙zywanych w wyra˙zeniu jako zwiazane jest spraw_, a drugorz_, edn_, a. Takie_, wyra˙zenia, jak na przyk lad λx.xy i λz.zy, intuicyjnie definiuja t_, e sam_, a operacj_, e (_,

”zaapli- kuj dany argument do y”) wiec z naszego punktu widzenia powinny by´_, c uwa˙zane za takie same. Dlatego lambda-wyra˙zenia r´o˙zniace si_, e tylko zmiennymi zwi_, azanymi chcemy ze sob_, a_, uto˙zsamia´c. Uto˙zsamienie to nazywa sie alfa-konwersj_, a._,

Pojecie alfa-konwersji mo˙zna ´_, sci´sle zdefiniowa´c na wiele sposob´ow, my wybierzemy interpre- tacje grafow_, a._,

Lambda-grafy

Przez drzewo rozumiemy poni˙zej sko´nczone drzewo etykietowane, w kt´orym wystepowa´_, c moga_, nastepuj_, ace rodzaje wierzcho lk´_, ow:

• wierzcho lki o etykiecie @, kt´ore maja zawsze dwa nast_, epniki: lewy i prawy;_,

• wierzcho lki o etykiecie λ, kt´ore maja zawsze jeden nast_, epnik;_,

• li´scie etykietowane zmiennymi przedmiotowymi;

• li´scie bez etykiet.

Przy tym ˙zadamy, aby ka˙zdy li´_, s´c bez etykiety mia l cho´c jednego przodka z etykieta λ._, Je´sli z ka˙zdego wierzcho lka bez etykiety poprowadzimy nowa kraw_, ed´_, z do kt´orego´s z poprzed- nik´ow tego wierzcho lka o etykiecie λ, to otrzymany graf skierowany nazwiemy lambda-drzewem.

Li´s´cmi lambda-drzewa nazywamy jego wierzcho lki ko´ncowe (ich etykietami sa zmienne)._, Na przyk lad taki graf jest lambda-drzewem (wierzcho lki bez etykiet oznaczono przez ◦).

λ

@

λ @

@ λ ◦

pp

◦

11

◦

jj

@

◦

44

y

Teraz dowolnemu lambda-wyra˙zeniu M przypiszemy lambda-drzewo G(M ).

• Je´sli x jest zmienna to G(x) sk lada si_, e tylko z jednego wierzcho lka o etykiecie x._,

• Graf G(P Q) ma korze´n o etykiecie @. Jego lewym nastepnikiem jest korze´_, n grafu G(P ) a prawym korze´n grafu G(Q).

• Graf G(λx P ) jest otrzymany z G(P ) poprzez – Dodanie nowego korzenia o etykiecie λ.

– Po laczenie go kraw_, edzi_, a z korzeniem grafu G(P )._,

– Dodanie krawedzi od wszystkich wierzcho lk´_, ow z etykieta x do nowego korzenia._, – Usuniecie etykiet x._,

Na przyk lad G(λz.(λu.zu)((λu.uy)z)) to lambda-drzewo na rysunku powy˙zej. Latwo widzie´c,

˙ze etykiety li´sci w G(M ) to dok ladnie zmienne wolne M . Na dodatek mamy:

Fakt 1.1 Je´sli T jest lambda-drzewem, to T = G(M ) dla pewnego lambda-wyra˙zenia M .

Dow´od: Indukcja ze wzgledu na liczb_, e wierzcho lk´_, ow grafu T . Je´sli jest tylko jeden wierz- cho lek, to jego etykieta jest pewna zmienna x i mamy T = G(x). Je´_, sli etykieta korzenia_, jest @, to T sk lada sie z korzenia i dw´_, och roz lacznych podgraf´_, ow T₁ i T₂, do kt´orych stosu- jemy za lo˙zenie indukcyjne. Mamy wiec T_, 1 = G(M1) oraz T2 = G(M2). Oczywi´scie wtedy T = G(M1M2). Pozostaje przypadek gdy etykieta korzenia jest λ. Wtedy T sk lada si_, e z ko-_, rzenia, podgrafu T₁ zaczepionego w nastepniku korzenia i pewnej liczby kraw_, edzi prowadz_, a-_, cych do korzenia z wierzcho lk´ow bez etykiet. Przypisujac tym wierzcho lkom etykiet_, e z, kt´_, ora nie wystepuje w grafie T_, 1, otrzymujemy z T1 lambda-drzewo T₁⁰. Z za lo˙zenia indukcyjnego T₁⁰ = G(M₁) dla pewnego lambda-wyra˙zenia M₁ i mo˙zemy napisa´c T = G(λz.M₁).

Relacje alfa-konwersji (oznaczan_, a przez =_{, α}) definiujemy tak:

M =α N wtedy i tylko wtedy, gdy G(M ) = G(N ).

Od tej pory przez lambda-termy albo po prostu termy rozumiemy

”lambda-wyra˙zenia z dok lad- no´scia do alfa-konwersji”, czyli w istocie klasy abstrakcji relacji =_{, α}. Ka˙zda taka klasa jest wyznaczona przez pewne lambda-drzewo, mo˙zemy wiec uwa˙za´_, c, ˙ze lambda-termy to tak naprawde lambda-drzewa. Lambda-wyra˙zenia s_, a tylko ich syntaktyczn_, a reprezentacj_, a, przy_, czym dowolne dwie alfa-r´ownowa˙zne reprezentacje tego samego termu (lambda-drzewa) sa_, tak samo dobre. Na przyk lad (λx.x(λx.xy))(λy.yx) to to samo co (λu.u(λx.xy))(λv.vx), ale nie to samo co (λy.y(λy.yx))(λx.xy). Od tej pory znak r´owno´sci oznacza r´owno´s´c lambda- term´ow (a nie ich reprezentacji), napiszemy wiec np. λx x = λy y._,

Podstawienie

Dla danych lambda-grafow G i T przez podstawienie G[x := T ] rozumiemy graf otrzymany z G przez zamiane ka˙zdego li´_, scia z etykieta x na korze´_, n odrebnej kopii grafu T . Ilustracja jest_, chyba prostsza i bardziej zrozumia la ni˙z jakakolwiek formalna definicja. Je´sli mamy grafy

x x

@

@

@

@

@

@

@ G

A

A A

A A

A T

to graf G[x := T ] wyglada tak jak na Obrazku 1 (etykiety x ju˙z nie ma):_,

A

A A

A A

A

A

A A

A A

A

@

@

@

@

@

@

@ G

T T

Obrazek 1: Podstawienie G[x := T ]

Je´sli M i N sa lambda-wyra˙zeniami to notacja M [x := N ] oznacza lambda-term o grafie_, G(M )[x := G(N )]. Zwykle m´owimy, ˙ze M [x := N ] to wynik podstawienia wyra˙zenia N na miejsce wszystkich wolnych wystapie´_, n zmiennej x w M . Ale ta interpretacja nie zawsze

jest poprawna. Problem powstaje wtedy, gdy jaka´s zmienna z wolna w N przy

”naiwnym”

tekstowym podstawieniu znalaz laby sie w zasi_, egu wi_, azania λz. Na przyk lad wynikiem pod-_, stawienia z na x w termie λz.x(xz) nie powinno by´c λz.z(zz). Chcemy bowiem podstawi´c z na miejsce x nie w napisie λz.x(xz) ale w grafie

λ

@

x @

x ◦

oo

w kt´orym w og´ole nie ma ˙zadnego z. A wiec zgodnie z nasz_, a definicj_, a_, (λz.x(xz))[x := z] = λy.z(zy),

przy czym wyb´or zwiazanej zmiennej y jest nieistotny. Tekstowe podstawienie jest poprawne_, tylko wtedy, gdy nie wystepuje konflikt nazw wolnych i zwi_, azanych (globalnych i lokalnych)._, Dlatego wcze´sniej nale˙zy dokona´c odpowiedniej wymiany zmiennych zwiazanych._,

Nastepuj_, acy lemat stanowi syntaktyczn_, a definicj_, e podstawienia._,

Lemat 1.2 R´owno´s´c M [x := N ] = R ma miejsce wtedy i tylko wtedy, gdy zachodzi jeden z nastepuj_, acych przypadk´_, ow:

1. M = x, oraz R = N ;

2. M jest zmienna r´_, o˙zna od x, oraz R = M ;_, 3. M = P Q, oraz R = P [x := N ]Q[x := N ];

4. M = λy P , gdzie y 6∈ {x} ∪FV(N ), oraz R = λy.P [x := N ].

Dow´od: Ka˙zdy term M jest albo zmienna albo aplikacj_, a albo abstrakcj_, a. Ta ostatnia_, mo˙zliwo´s´c to jedyny nieoczywisty przypadek, niech wiec M b_, edzie abstrakcj_, a. Je´_, sli z lambda- drzewa termu M odrzucimy korze´n wraz z prowadzacymi do niego kraw_, edziami, to otrzymamy_, graf M⁰, w kt´orym niekt´ore wierzcho lki ko´ncowe nie maja etykiet. Nadaj_, ac tym wierzcho lkom_,

”nowa” etykiet_, e y otrzymamy taki term P , ˙ze M = λy P . Poniewa˙z y nie wyst_, epuje jako_, etykieta w lambda-drzewie N , wiec nie ma znaczenia czy najpierw w termie P zamienimy x_, na N , a potem dodamy lambde wi_, a˙z_, ac_, a y, czy post_, apimy w odwrotnej kolejno´_, sci.

Zapiszmy tre´s´c lematu 1.2 w nieco prostszej postaci:

• x[x := N ] = N ;

• y[x := N ] = y, gdy y jest zmienn

a r´, o˙zna od x;_,

• (P Q)[x := N ] = P [x := N ]Q[x := N ];

• (λy P )[x := N ] = λy.P [x := N ], gdy y 6= x oraz y 6∈FV(N ).

Powy˙zsze regu ly mo˙zna stosowa´c w dowodach indukcyjnych.

Lemat 1.3

1. FV(M [x := N ]) =

 (FV(M ) − {x}) ∪FV(N ), je´sli x ∈FV(M );

FV(M ), w przeciwnym przypadku.

2. Je´sli x 6∈FV(M ) to M [x := N ] = M . 3. M [x := x] = M .

4. Je´sli λx.P = λy.Q to P [x := y] = Q i Q[y := x] = P .

Latwy dow´od tego lematu pomijamy, udowodnimy za to nastepny._,

Lemat 1.4 (o podstawieniu) Je´sli x 6= y oraz albo x 6∈FV(R) albo y 6∈FV(M ), to M [x := N ][y := R] = M [y := R][x := N [y := R]].

Dow´od: Dow´od jest przez indukcje ze wzgl_, edu na rozmiar M . Rozwa˙zamy r´_, o˙zne przy- padki, w zale˙zno´sci od postaci tego termu.

Przypadek 1: Je˙zeli M = x, to M [x := N ][y := R] = x[x := N ][y := R] = N [y := R] = x[x := N [y := R]] = x[y := R][x := N [y := R]].

Przypadek 2: Je˙zeli M = y, to M [x := N ][y := R] = y[x := N ][y := R] = y[y := R] = R = R[x := N [y := R]] = y[y := R][x := N [y := R]], bo wtedy x 6∈FV(R).

Przypadek 3: Je˙zeli M jest jaka´_,s inna zmienn_, a z, to zar´_, owno M [x := N ][y := R] jak te˙z M [y := R][x := N [y := R]] jest r´owne z.

Przypadek 4: Gdy M = P Q, to M [x:=N ][y:=R] = P [x:=N ][y:=R]Q[x:=N ][y:=R] = P [y:=R][x:=N [y:=R]]Q[y:=R][x:=N [y:=R]] = (P Q)[y:=R][x:=N [y:=R]], na mocy za lo˙zenia indukcyjnego.

Przypadek 5: Je˙zeli M jest abstrakcja to mo˙zna zak lada´_, c, ˙ze M = λz Q, gdzie z 6= x, y.

Po lewej stronie mamy wtedy λz. Q[x := N ][y := R] i z za lo˙zenia indukcyjnego otrzymamy M [x := N ][y := R] = λz. Q[y := R][x := N [y := R]] = (λz. Q)[y := R][x := N [y := R]].

Wniosek 1.5 Je´sli y 6∈FV(M ) to M [x := y][y := R] = M [x := R].

Cwiczenia´

1. Jaki b lad pope lniono w tej definicji lambda-termu:_,

M ::= x | M N | λx.M ? 2. Udowodni´c lemat 1.3.

3. Napis M (a|b) oznacza wyra˙zenie powsta le z M przez jednoczesna zamian_, e wszystkich wyst_, apie´_, n symbolu a w M na wystapienia b i odwrotnie. Przez ≡_{, α} oznaczmy najmniejsza relacj_, e r´_, owno- wa˙zno´sci w zbiorze lambda-wyra˙ze´n, spe lniajac_, a nast_, epuj_, ace warunki:_,

• λx.M ≡αλy.M (x|y), dla y 6∈ FV(M );

• je˙zeli M ≡αM⁰, to λx.M ≡αλx.M⁰;

• je˙zeli M ≡αM⁰ i N ≡αN⁰ to M N ≡αM⁰N⁰.

Udowodni´c, ˙ze M ≡_αN wtedy i tylko wtedy, gdy M =_αN .

2 Redukcje

Relacja beta-redukcji to najmniejsza relacja w zbiorze lambda-term´ow, spe lniajaca warunki:_,

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

• je´sli M →_β M⁰, to M N →β M⁰N , N M →β N M⁰ oraz λxM →β λxM⁰.

Inaczej m´owiac, M →_{, β} M⁰ zachodzi gdy podterm termu M postaci (λxP )Q, czyli β-redeks, zostaje zastapiony w termie M_, ⁰ przez P [x := Q]. Znakiem β lub →^∗_β oznaczamy domknie-_, cie przechodnio-zwrotne relacji →_β, a znakiem =_β najmniejsza relacj_, e r´_, ownowa˙zno´sci zawie- rajac_, a →_{, β}, kt´ora nazywamy relacj_, a beta-r´_, owno´sci . Inne popularne oznaczenia to →⁺_β na domkniecie przechodnie i →_, ⁼_β na domkniecie zwrotne relacji →_, β. Indeks β przy strza lkach bywa pomijany.

Z punktu widzenia grafowego, beta-redeks to krawed´_, z od @ do λ:

(1)



@

| 

λ



(3)

(2)

Beta-redukcja polega na usunieciu tej kraw_, edzi, tj. na_,

”wyprostowaniu” drogi od (1) do (2).

Ka˙zda krawed´_, z wchodzaca do λ (reprezentuj_, aca wyst_, apienie zmiennej zwi_, azanej) zostaje przy_, tym skierowana do osobnej kopii termu zaczepionego w (3). Inaczej, podgraf postaci

(1)



@

| 

λ



(3)

(2)

 

◦

77

◦

hh

zostaje zastapiony podgrafem postaci:_,

(1)



(2)

 

(3) (3)

Uwaga: mo˙ze sie zdarzy´_, c, ˙ze lambda nie wia˙ze ˙z_, adnego wyst_, apienia zmiennej (nie ma ˙zad-_, nej krawedzi prowadz_, acej do λ). Wtedy podgraf (3) znika. Odpowiada to redukcji postaci_, (λx.M )N →_β M , gdzie x 6∈FV(M ).

Nastepuj_, acy latwy lemat stwierdza, ˙ze β-redukcja jest zgodna z operacj_, a podstawienia._, Lemat 2.1 Je´sli M β M⁰ i N β N⁰ to M [x := N ] β M⁰[x := N⁰].

Dow´od: Nale˙zy pokaza´c dwa prostsze stwierdzenia:

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

(2) Je´sli N →_β N⁰, to M [x := N ] β M [x := N⁰],

a nastepnie zastosowa´_, c indukcje ze wzgl_, edu na liczb_, e krok´_, ow redukcji. Zar´owno (1) jak (2) mo˙zna udowodni´c przez indukcje ze wzgl_, edu na d lugo´_, s´c termu M . Istotny przypadek w dowo- dzie cze´_,sci (1) zachodzi wtedy, gdy M = (λy P )Q i M⁰ = P [y:=Q], dla pewnych P, Q. Przyj- mujac y 6∈_, FV(N ), mamy M [x:=N ] = (λy.P [x:=N ])Q[x:=N ] →_β P [x:=N ][y:=Q[x:=N ]] = P [y:=Q][x:=N ] = M⁰[x:=N ], na mocy lematu o podstawieniu 1.4. Szczeg´o ly pozostawiamy jako ´cwiczenie.

Teoria λ

Rachunek lambda bez typ´ow mo˙zna przedstawi´c jako teorie r´_, owno´sciowa o aksjomatach i re-_, gu lach jak na Obrazku 2. Je´sli w tym systemie mo˙zna wyprowadzi´c r´owno´s´c M = N , to napiszemy λ ` M = N . Latwo sprawdzi´c r´ownowa˙zno´s´c:

λ ` M = N wtedy i tylko wtedy, gdy M =_β N .

Jednak˙ze dla nas wa˙zne sa te˙z w lasno´_, sci beta-redukcji, a nie tylko beta-r´owno´sci. Term postaci (λxP )Q nazywamy beta-redeksem. Je´sli w termie M nie wystepuje ˙zaden beta-redeks, to dla_,

˙zadnego N nie zachodzi M →β N . M´owimy wtedy, ˙ze M jest w postaci β-normalnej, lub po prostu w postaci normalnej. Nietrudno zauwa˙zy´c, ˙ze postaci normalne to dok ladnie termy kszta ltu λ~x. y ~N , gdzie ~N sa normalne._,

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

M P = N P

M = N

P M = P N (ξ) M = N

λx M = λx N M = N

N = M

M = N, N = P M = P

Obrazek 2: Rachunek lambda jako teoria r´owno´sciowa Przyk lad: Nastepuj_, ace termy s_, a w postaci normalnej:_,

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

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

Natomiast term Ω = ωω nie jest w postaci normalnej, bo Ω →_β Ω.

Je´sli M β N i N jest w postaci normalnej, to m´owimy, ˙ze M ma posta´c normalna, i ˙ze N jest_, postacia normaln_, a termu M . M´_, owimy, ˙ze term M ma w lasno´s´c silnej normalizacji (jest silnie normalizowalny) je˙zeli nie istnieje niesko´nczony ciag redukcji M = M_{, 0} →_β M₁ →_β M₂ →_β · · · Oczywi´scie term silnie normalizowalny musi mie´c posta´c normalna._,

Jeszcze jedno przydatne czasem oznaczenie. Piszemy M ↓_β N , gdy istnieje taki term P , ˙ze M β P_β N .

G l´ownym przedmiotem naszego zainteresowania jest beta-redukcja. Dlatego np. symbole → i  domy´slnie¹ oznaczaja →_{, β} i β. Ale czasami rozwa˙zamy tak˙ze relacje eta-redukcji. Jest_, to najmniejsza relacja →_η, spe lniajac_, a warunki:_,

• λx.M x →_η M , gdy x 6∈FV(M );

• je´sli M →_η M⁰, to M N →_η M⁰N , N M →_η N M⁰ oraz λxM →_η λxM⁰.

Symbol →_βηoznacza sume tych relacyj. U˙zywamy odpowiednio notacji np. _, η, =_βη, m´owimy o”postaciach η-normalnych” itd.

Je˙zeli do aksjomat´ow i regu l r´owno´sciowych rozwa˙zanych powy˙zej dodamy nowy aksjomat (η) λx.M x = M,

dla x 6∈ FV(M ), to oczywi´scie otrzymamy system wnioskowania, pozwalajacy na wyprowa-_, dzenie r´owno´sci M = N wtedy i tylko wtedy gdy M =_βη N . Mniej oczywiste jest to, ˙ze aksjomat (η) mo˙zna r´ownowa˙znie zastapi´_, c przez nastepuj_, ac_, a regu l_, e ekstensjonalno´_, sci:

(ext) M x = N x

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

1W odniesieniu do znaku r´owno´sci nie stosujemy tej konwencji (ale spotyka sie to cz_, esto w literaturze)._,

Regu la ekstensjonalno´sci wyra˙za taka my´_, sl: funkcje, kt´ore dla tych samych argument´ow daja_, te same wyniki, sa r´_, owne.

Dygresja: Zauwa˙zmy, ˙ze beta- i eta-redukcja sa w pewnym sensie dualne do siebie. Beta-_, redeks to term, w kt´orym najpierw utworzyli´smy funkcje, tj. wprowadzili´_, smy abstrakcje (czyli_, zapytanie o argument, prompt), a potem ja eliminujemy przez dostarczenie argumentu. Eta-_, redeks odpowiada odwrotnej kolejno´sci: najpierw eliminujemy prompt, dostarczajac zmiennej_, jako argumentu, a potem wprowadzamy abstrakcje ze wzgl_, edu na t_, e zmienn_, a._,

Cwiczenia´

1. Napisa´c program, kt´ory drukuje w lasny tekst. (Nie wolno odwo lywa´c sie do nazwy pliku, miejsca_, w pamieci itp.) Zadanie latwe w Lispie, trudne w Pascalu._,

2. Udowodni´c, ˙ze je´sli (λxP )Q = (λyP⁰)Q⁰ to P [x := Q] = P⁰[y := Q⁰].

3. Udowodni´c, ˙ze aksjomat (η) jest r´ownowa˙zny regule (ext), tj. te same r´owno´sci mo˙zna wypro- wadzi´c w systemie z Obrazka 2 rozszerzonym o (η) i w systemie rozszerzonym o regu le (ext)._, 4. Sprawdzi´c, ˙ze λx.M x =_βM , gdy M jest abstrakcja._,

3 Twierdzenie Churcha-Rossera

W jednym termie mo˙ze wystepowa´_, c wiecej ni˙z jeden redeks._, Mo˙zna wiec go redukowa´_, c na r´o˙zne sposoby. Niedobrze jednak by loby, gdyby te r´o˙zne ciagi redukcji prowadzi ly do_, nieodwracalnie r´o˙znych rezultat´ow. Na szcze´_,scie mamy twierdzenie Churcha-Rossera.

Twierdzenie 3.1 Je´sli P _β M β Q, to P ↓_β Q.

Tre´s´c twierdzenia Churcha-Rossera przedstawiamy za pomoca diagramu (Obrazek 3)._, M

β

~~~~

β

P

β

Q

~~~~ β

•

Obrazek 3: Twierdzenie Churcha-Rossera

Inaczej m´owiac, twierdzenie to m´_, owi, ˙ze relacja β ma tzw. w lasno´s´c rombu, kt´ora niestety nie zachodzi dla relacji →_β. Jako przyk lad mo˙zna poda´c term M = (λx.xx)((λx.x)y).

Zanim udowodnimy twierdzenie Churcha-Rossera, zauwa˙zmy, ˙ze pojecie o kt´_, orym m´owimy, ma sens dla ka˙zdej relacji dwuargumentowej. Poni˙zej przyjmujemy taka konwencj_, e: po-_, dw´ojna strza lka zawsze oznacza domkniecie przechodnio-zwrotne relacji oznaczonej strza lk_, a_, pojedyncza._,

M´owimy, ˙ze relacja → w zbiorze A ma w lasno´s´c Churcha-Rossera (CR), je˙zeli dla dowolnych element´ow a, b, c ∈ A, takich ˙ze b  a  c, istnieje takie d, ˙ze b  d  c. Relacja → ma s laba_,

w lasno´s´c Churcha-Rossera (WCR), je˙zeli b ← a → c implikuje b  d  c dla pewnego d.

Oczywi´scie w lasno´s´c rombu implikuje CR (ale nie na odwr´ot), a w lasno´s´c CR implikuje WCR.

Mniej oczywiste jest to, ˙ze w lasno´s´c CR nie wynika z WCR. Najprostszy przyk lad jest taki:

• ←− • ←→ • −→ •

Je´sli jednak relacja → ma w lasno´s´c silnej normalizacji (SN), tj. nie istnieje niesko´nczony ciag_, postaci a0 → a₁ → a₂ → · · · , to ju˙z jest dobrze.

a

 

b1

  

c1

  

b

d



c

·

·

·

Obrazek 4: Rysunek do lematu Newmana

Fakt 3.2 (Lemat Newmana) Jednoczesne zachodzenie WCR i SN implikuje CR.

Dow´od: Je´sli relacja → ma w lasno´s´c SN to relacja  jest dobrym ufundowaniem zbioru A.

Przez indukcje ze wzgl_, edu na porz_, adek  dowodzimy, ˙ze ka˙zdy element a ∈ A ma w lasno´s´c:_, Dla dowolnych b, c, je´sli b  a  c, to b ↓ c.

Je´sli a = b lub a = c to teza jest oczywista. Za l´o˙zmy wiec, ˙ze b  b_, 1← a → c₁ c.

Na mocy WCR jest takie d, ˙ze b1  d  c1. Z za lo˙zenia indukcyjnego, zastosowanego do b1

i c₁ mamy wiec b ↓ d ↓ c i mo˙zemy zastosowa´_, c za lo˙zenie indukcyjne dla d.

Dow´od twierdzenia Churcha-Rossera

Dla dowodu zdefiniujemy pewna pomocnicz_, a relacj_, e. B_, edzie to relacja_, →, okre´slona jako¹ najmniejsza relacja na termach, kt´ora spe lnia nastepuj_, ace warunki:_,

– x→ x, gdy x jest zmienn¹ a;_, – je´sli M → M^{1 0}, to λxM → λxM^{1 0};

– je´sli M → M^{1 0} i N → N^{1 0}, to M N → M^{1 0}N⁰, oraz (λxM )N → M^{1 0}[x := N⁰].

Relacja → odpowiada jednoczesnej redukcji kilku beta-redeks´¹ ow wystepuj_, acych w termie._, Je´sli zredukujemy wszystkie redeksy w termie M , to otrzymamy jego pe lne rozwiniecie M_, ^•: – x^• = x;

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

– (M N )^• = M^•N^•, gdy M nie jest abstrakcja;_, – ((λx M )N )^•= M^•[x := N^•].

Lemat 3.3

(1) Dla dowolnego M zachodzi M → M oraz M¹ → M^{1 •}. (2) Je´sli M → M^{1 0} i N → N^{1 0}, to M [x := N ]→ M^{1 0}[x := N⁰].

(3) Je´sli M → M^{1 0}, to M^{0 1}→ M^•.

Dow´od: Dow´od cze´_,sci (1) jest przez indukcje ze wzgl_, edu na budow_, e M , a cz_, e´_,sci (2) i (3) przez indukcje ze wzgl_, edu na wyprowadzenie M_, → M^{1 0}. W dowodzie punktu (2) nieoczywisty jest przypadek, gdy M = (λyP )Q→ P^{1 0}[y := Q⁰], gdzie P → P^{1 0} oraz Q→ Q^{1 0}. Zak ladajac, ˙ze_, zmienna zwiazana y jest tak wybrana, ˙ze y 6∈ FV (N ), i korzystaj_, ac z za lo˙zenia indukcyjnego_, o P → P^{1 0} i Q→ Q^{1 0}, mamy wtedy na mocy lematu o podstawieniu:

M [x:=N ] = (λyP [x:=N ])Q[x:=N ]→ P^{1 0}[x:=N⁰][y:=Q⁰[x:=N⁰]] = P⁰[y:=Q⁰][x:=N⁰].

Uwaga: U˙zyty w powy˙zszym dowodzie zwrot

”dow´od przez indukcje ze wzgl_, edu na wypro-_, wadzenie M → M^{1 0}” mo˙zna ´sci´sle rozumie´c tak: Zbi´or par term´ow {(M, M⁰) | M → M^{1 0}} jest suma wst_, epuj_, acego ci_, agu zbior´_, ow Xi, gdzie X0 = {(x, x) | x jest zmienna}, a ka˙zdy zbi´_, or Xi+1

powstaje z X_i przez dodanie wszystkich par (M N, M⁰N⁰), ((λxM )N, M⁰[x := N⁰]) oraz (λxM, λxM⁰), dla dowolnych (M, M⁰) i (N, N⁰), kt´ore sa ju˙z w X_{, i}. Indukcje tak naprawd_, e_, prowadzimy ze wzgledu na najmniejsze takie i, ˙ze (M, M_, ⁰) ∈ Xi.

M

1

}}

1

!!

M⁰

1 !!

M⁰⁰ }} 1

M⁰⁰⁰

Obrazek 5: W lasno´s´c rombu

Wniosek 3.4 Relacja→ ma w lasno´s´¹ c rombu, tj. je´sli M → M^{1 0} i M → M^{1 00}, to dla pewnego termu M⁰⁰⁰ zachodzi M^{0 1}→ M^{000 1}← M⁰⁰.

Dow´od: Z lematu 3.3(3) wynika, ˙ze jako M⁰⁰⁰ mo˙zna wzia´_,c M^•.

Dow´od twierdzenia 3.1: Poniewa˙z relacja → ma w lasno´s´¹ c rombu, wiec tym bardziej jej_, domkniecie przechodnio-zwrotne_,  ma w lasno´s´c rombu.¹

Zauwa˙zmy teraz, ˙ze mamy nastepuj_, ace zawierania pomi_, edzy relacjami:_,

→_β ⊆→ ⊆ ¹ β.

Stad latwo wywnioskowa´_, c, ˙ze relacje  i ¹ β sa r´_, owne, a wiec _, β ma w lasno´s´c rombu.

Skoro udowodnili´smy twierdzenie Churcha-Rossera, zobaczmy jakie ma ono konsekwencje.

Wniosek 3.5

0) Je´sli M ↓_β N ↓_β Q, to M ↓_β Q.

1) Je´sli M =β N , to M ↓β N .

2) Ka˙zdy term ma co najwy˙zej jedna posta´_, c normalna._,

3) Rachunek lambda jest niesprzeczny jako teoria r´owno´sciowa: nie mo˙zna np. wyprowadzi´c r´owno´sci x = y, poniewa˙z x 6=β y.

Q1

  

Q2

  

Qn

}}}}  

M0

M1



"" ""

M2 . . . M_n−1 Mn

{{{{

•

"" ""

•



•

Obrazek 6: Dow´od wniosku 3.5(1)

Dow´od: Jedyna nieoczywista cze´_,s´c to (1). Je´sli M =_β N , to mamy taki ciag:_, M = M₀  Q1  M1 Q2  M2 · · ·  Mn= N

Dowodzimy M ↓β N , przez indukcje ze wzgl_, edu na n. Je´_, sli n = 0, to sprawa jest oczywista, w przeciwnym razie z za lo˙zenia indukcyjnego mamy M₁ ↓_β N . Ale M₀ ↓_β M₁ na mocy CR, wiec M ↓_{, β} N wynika z cze´_,sci (0). Zob. Obrazek 6.

A zatem sens twierdzenia Churcha-Rossera mo˙zna wyrazi´c tak. Chocia˙z term mo˙ze by´c re- dukowany na wiele sposob´ow, to wszystkie te sposoby sa zgodne. Ka˙zde obliczenie zako´_, nczone sukcesem (uzyskaniem postaci normalnej) daje ten sam wynik.

Cwiczenia´

1. Jaki sens grafowy ma relacja→ i pe lne rozwini¹ ecie termu?_,

2. Term M^•powstaje przez redukcje wszystkich redeks´_, ow w M . Czy M^• jest postacia normaln_, a?_,

4 Eta-redukcja

Ka˙zdy krok η-redukcji λx. M x →η M zmniejsza d lugo´s´c termu, zatem zachodzi Fakt 4.1 Relacja η-redukcji ma w lasno´s´c silnej normalizacji.

Aby wywnioskowa´c, ˙ze →_η ma w lasno´s´c Churcha-Rossera, wystarczy wiec pokaza´_, c WCR.

W istocie mamy prawie w lasno´s´c rombu, co mo˙zna latwo pokaza´c, badajac mo˙zliwe przypadki_, wzajemnego po lo˙zenia redeks´ow.

Lemat 4.2 Domkniecie zwrotne →_, ⁼_η relacji →η ma w lasno´s´c rombu.

W lasno´s´c rombu dla η-redukcji nie zachodzi bo y η← λx. yx →_η y, tymczasem nie ma termu, do kt´orego y redukowa lby sie w jednym kroku._,

Wniosek 4.3 Relacja η-redukcji ma w lasno´s´c Churcha-Rossera.

Poka˙zemy teraz, ˙ze w lasno´s´c Churcha-Rossera zachodzi tak˙ze dla relacji →_βη. Lemat 4.4 Je´sli P_η← M →_β Q to istnieje takie N , ˙ze P →⁼_β N _η Q.

M

η



β

P

β

=

Q

 η

N

Dow´od: Badajac wzajemne po lo˙zenie beta- i eta-redeks´_, ow w grafie termu M (Obrazek 7), widzimy ˙ze kolejno´s´c, w kt´orej redukujemy te redeksy, na og´o l nie ma znaczenia i rezultat jest taki sam. Pierwszy wyjatek, to sytuacja gdy eta-redeks znajduje si_, e w argumencie beta-_, redeksu i wskutek redukcji mo˙ze zosta´c usuniety lub powielony. Dlatego w tre´_, sci lematu

λ



@



@



λ

•

cc

Obrazek 7: Eta-redeks i beta-redeks

po prawej stronie mamy strza lke podw´_, ojna_{, η} a nie pojedyncza. Pozosta le dwa wyj_, atki_, zachodza wtedy, gdy nasze dwa redeksy wykorzystuj_, a ten sam wierzcho lek grafu (lambd_, e_, lub aplikacje). Ma to miejsce w podtermach postaci (λx.M x)N , gdzie x 6∈_, FV(M ) oraz postaci λx(λy M )x, gdzie x 6∈FV(λy M ). Na obrazku 8 wsp´olne wierzcho lki sa w nawiasach_, kwadratowych. Szcze´_,sliwie w obu przypadkach redukcja ka˙zdego z konkurujacych redeks´_, ow daje ten sam rezultat.

@

 

λ



[λ]



[@]

 

@

~~

λ



•

dd

•

dd

Obrazek 8: Pary krytyczne dla beta-eta-redukcji

Sytuacja zilustrowana na Obrazku 8 mo˙ze dotyczy´c tak˙ze innych system´ow redukcyjnych.

Je´sli redukcja ka˙zdego z dw´och redeks´ow wymaga zu˙zycia tego samego

”zasobu”, to m´owimy,

˙ze redeksy te tworza par_, e krytyczn_, a. Je´_, sli ka˙zda par_, e krytyczn_, a mo˙zna_,

”uzgodni´c” to dana relacja redukcji ma s laba w lasno´_, s´c Churcha-Rossera.²

Z lematu 4.4 wynika latwo, ˙ze mamy nastepuj_, acy diagram:_,

·

η β

=

·

β

=

·

η

·

2Dla system´ow o w lasno´sci SN mamy wiec og´_, olna metod_, e dowodzenia w lasno´_, sci Churcha-Rossera: uzgodni´c pary krytyczne i zastosowa´c lemat Newmana 3.2.

Z tego diagramu otrzymamy nastepny. M´_, owi on, ˙ze relacje β i η sa przemienne:_,

·

η β

·

β  

·

η

·

Poniewa˙z obie relacje maja w lasno´_, s´c Churcha-Rossera, nietrudno teraz pokaza´c Twierdzenie 4.5 Relacja →_βη ma w lasno´s´c Churcha-Rossera.

Beta-eta-redukcja

Poka˙zemy teraz, ˙ze w lasno´s´c silnej β-normalizacji jest r´ownowa˙zna silnej βη-normalizacji.

Wynika to latwo z nastepuj_, acego prostego lematu._,

Lemat 4.6 Niech M →η N →_β P ale M 6→_β N . Wtedy istnieje takie Q, ˙ze M →_β Q η P .

Dow´od: Zauwa˙zmy, ˙ze jedyna sytuacja, w kt´orej eta-redukcja mo˙ze wykreowa´c nowy beta- redeks wyglada tak, jak na Obrazku 9. To jest akurat sytuacja zabroniona, bo zamiast eta-_,

@

λ



@

λ •

ee

Obrazek 9: Eta-redukcja tworzy beta-redeks

redeksu mo˙zemy z tym samym skutkiem zredukowa´c beta-redeks. W pozosta lych przypadkach beta-redeks redukowany w drugim kroku ju˙z istnieje w termie M i mo˙ze zosta´c zredukowany zanim wykonana bedzie eta-redukcja. Potem dopiero wykonamy tyle eta-redukcji ile kopii_, naszego eta-redeksu (by´c mo˙ze zero) wystepuje w Q._,

Wniosek 4.7 Je´sli M βη P →β N to M →β Q βη N , dla pewnego Q. Graficznie:

·

β

·

βη @@ @@

β 

·

·

βη

@@ @@

Wniosek 4.8 Term ma niesko´nczona β-redukcj_, e wtedy i tylko wtedy gdy ma niesko´_, nczona_, βη-redukcje. (Inaczej: term ma w lasno´_, s´c β-SN wtedy i tylko wtedy, gdy ma w lasno´s´c βη-SN.)

Dow´od: Za l´o˙zmy, ˙ze mamy niesko´nczona βη-redukcj_, e. Je´_, sli beta-kroki wystepuj_, a w tej re-_, dukcji niesko´nczenie wiele razy, to wniosek 4.7 pozwala z niej uzyska´c niesko´nczona β-redukcj_, e_, (poprzez

”przesuwanie” beta-krok´ow w lewo). A nie mo˙ze by´c tak, ˙ze prawie wszystkie kroki sa typu eta. Implikacja w przeciwn_, a stron_, e jest oczywi´_, scie oczywista.

Nieco trudniej jest udowodni´c r´ownowa˙zno´s´c

”zwyk lej” β- i βη-normalizacji. Najpierw musimy pokaza´c, ˙ze ka˙zdy ciag beta-eta-redukcji mo˙zna_,

”posortowa´c” tak aby wszystkie eta-redukcje by ly na ko´ncu (twierdzenie 4.10 o odk ladaniu η-redukcji). Niech  oznacza najmniejsza relacj_, e_, w zbiorze term´ow, spe lniajac_, a warunki:_,

• x  x, dla dowolnej zmiennej x;

• je´sli M  M⁰ oraz x 6∈FV(M ), to λx.M x  M⁰;

• je´sli M  M⁰, to λx.M  λx.M⁰;

• je´sli M  M⁰ oraz N  N⁰, to M N  M⁰N⁰.

Relacja  tak sie ma do η-redukcji, jak relacja_, → do β-redukcji. Na przyk lad λx(λy. zy)x  z,¹ ale λxy. zxy 6 z, chocia˙z λxy. zxy η z. Mamy wiec znowu ostre inkluzje:_,

→_η  η. Lemat 4.9

(1) Je´sli M  M⁰ oraz N  N⁰, to M [x := N ]  M⁰[x := N⁰].

(2) Je´sli M  M⁰ →_β P to istnieje taki term Q, ˙ze M β Q  P .

Dow´od: Cze´_,s´c (1) mo˙zna udowodni´c przez latwa indukcj_, e ze wzgl_, edu na definicj_, e M  M_, ⁰. W cze´_,sci (2) najpierw udowodnimy szczeg´olny przypadek:

Je´sli L  λy R oraz N  N⁰, to istnieje takie Q, ˙ze LN β Q  R[y := N⁰], (*) przez indukcje ze wzgl_, edu na d lugo´_, s´c L. Sa tu dwa przypadki. Pierwszy, gdy L = λy L_{, 1} i L1  R; wtedy LN →_β L1[y := N ]  R[y := N⁰] z cze´_,sci (1). W drugim przypadku, gdy L = λz. L1z i L1 λy R, stosujemy indukcje._,

Majac (*) dowodzimy cz_, e´_,sci (2) przez indukcje ze wzgl_, edu na definicj_, e M  M_, ⁰.

Twierdzenie 4.10 (o odk ladaniu η-redukcji)

Je´sli M βη N to M β P η N , dla pewnego P .

Dow´od: Je´sli M βη N , to ka˙zdy krok eta-redukcji mo˙zna uwa˙za´c za krok typu , i”przesuwa´c” w prawo z pomoca lematu 4.9(2)._,

Lemat 4.11 Je´sli M  N oraz N jest w postaci β-normalnej, to M ma posta´c β-normalna._,

Dow´od: Przez indukcje ze wzgl_, edu na definicj_, e M  N dowodzimy, ˙ze posta´_, c β-normalna M⁰ termu M istnieje i ma w lasno´s´c M⁰ N .

Nieoczywisty przypadek jest wtedy, gdy M = P Q, N = P⁰Q⁰ oraz P  P⁰ i Q  Q⁰. Z za lo˙zenia indukcyjnego mamy postaci β-normalne P⁰⁰ i Q⁰⁰ term´ow P i Q i wszystko jest dobrze, je˙zeli P⁰⁰ nie jest abstrakcja._,

Je´sli P⁰⁰jest abstrakcja, to musimy skorzysta´_, c z za lo˙zenia indukcyjnego, ˙ze P⁰⁰ P⁰. Poniewa˙z term P⁰ abstrakcja nie jest, wi_, ec musi by´_, c tak: P⁰⁰= λu. P⁰⁰⁰u oraz P⁰⁰⁰  P⁰. Przy tym P⁰⁰⁰ te˙z nie jest abstrakcja, bo inaczej P_, ⁰⁰ nie jest β-normalne. I teraz mamy

P Q β (λu. P⁰⁰⁰u)Q⁰⁰ →_β P⁰⁰⁰Q⁰⁰ P⁰Q⁰. Pozosta le przypadki sa w zasadzie rutynowe._,

Lemat 4.12 Je´sli M  N oraz N ma posta´c β-normalna, to M te˙z ma._,

Dow´od: Tu jest indukcja ze wzgledu na liczb_, e krok´_, ow redukcji N do postaci normalnej.

Krok bazowy to lemat 4.11. W kroku indukcyjnym mamy M  N →_β N⁰ β N⁰⁰, gdzie N⁰⁰ jest normalne. Korzystamy z lematu 4.9 i stosujemy indukcje._,

Twierdzenie 4.13 Term ma posta´c beta-normalna wtedy i tylko wtedy, gdy ma posta´_, c beta-eta-normalna._,

Dow´od: Aby udowodni´c implikacje z lewej do prawej, wystarczy zauwa˙zy´_, c, ˙ze η-redu- kowanie postaci beta-normalnej nie tworzy nowych beta-redeks´ow (´cwiczenie 4), musi wiec_, w ko´ncu da´c posta´c βη-normalna._,

W dowodzie implikacji odwrotnej korzysta sie z twierdzenia o odk ladaniu eta-redukcji. Mamy_, wiec redukcj_, e M _, β N η P do postaci βη-normalnej. Poniewa˙z →_η jest zawarte w , wiec_, z lematu 4.12 wynika, ˙ze N (a wiec i M ) ma posta´_, c β-normalna._,

Cwiczenia´

1. W jaki spos´ob beta-redukcja mo˙ze spowodowa´c powstanie nowego beta-redeksu? Eta-redeksu?

2. Uzupe lni´c szczeg´o ly dowodu twierdzenia 4.10.

3. Dlaczego twierdzenie 4.10 nie wynika natychmiast z lematu 4.6?

4. Pokaza´c, ˙ze je´sli M jest w postaci β-normalnej oraz M →ηN to N jest w postaci β-normalnej.

5 Standaryzacja

W jednym termie mo˙ze wystepowa´_, c wiecej ni˙z jeden redeks. Mo˙zliwe s_, a wi_, ec r´_, o˙zne strategie redukcji . Jedna z nich polega na wybieraniu zawsze tego redeksu, kt´ory zaczyna sie najbar-_, dziej na lewo. M´owimy wtedy o redukcji lewostronnej . Okazuje sie, ˙ze strategia redukcji_, lewostronnej jest strategia normalizujac_, a, tj. t_, a metod_, a zawsze dojdziemy do postaci normal-_, nej, je´sli ona istnieje. Popatrzmy na przyk lad na term KzΩ. W zale˙zno´sci od wyboru strategii redukcji mo˙zemy doj´s´c do postaci normalnej lub redukowa´c ten term w niesko´nczono´s´c.

W istocie prawdziwe jest nieco silniejsze twierdzenie, zwane twierdzeniem o standaryzacji.

Powiemy, ˙ze wyprowadzenie

M₀ → M₁→ · · · → M_n

jest standardowe, je˙zeli dla dowolnego i = 0, . . . , n − 2, w kroku Mi → M_i+1 redukujemy redeks po lo˙zony³ nie dalej od poczatku termu ni˙z redeks, kt´_, ory redukujemy w nastepnym_, kroku M_i+1→ M_i+2. Na przyk lad ta redukcja jest standardowa:

(λ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).

a ta nie jest:

(λ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).

Twierdzenie 5.1 Je´sli M β N , to istnieje standardowa redukcja z M do N .

Zajmiemy sie teraz dowodem twierdzenia 5.1. Zaczniemy od tego, ˙ze ka˙zdy term M jest jednej_, z dw´och mo˙zliwych postaci:

1) λ~x.z ~R;

2) λ~x.(λy.P )Q ~R,

gdzie d lugo´s´c wektora ~x mo˙ze by´c zerem, a z mo˙ze wystepowa´_, c w ~x lub nie. W przypadku (1) m´owimy, ˙ze term jest w czo lowej postaci normalnej⁴. Natomiast w przypadku (2) m´owimy,

˙ze term ma redeks czo lowy (λy.P )Q. Krok redukcji

M = λ~x.(λy.P )Q ~R →_β λ~x.P [y := Q] ~R = N

nazywamy wtedy redukcja czo low_, a i zapisujemy M_, → N . Inne kroki redukcji nazywamy^h wewnetrznymi , a w takim przypadku u˙zywamy symbolu_, →. Kluczowy lemat 5.3 m´ⁱ owi, ˙ze redukcje czo lowe mo˙zna wykona´c przed wewnetrznymi. Dow´_, od tego lematu nie jest jednak tak oczywisty, jak mog loby sie wydawa´_, c (´cwiczenie 3) i wymaga pewnych przygotowa´n, w tym dw´och pomocniczych relacji. Idea dowodu polega na u˙zyciu redukcji postaci→, kt´¹ ore latwiej rozbi´c na cze´_,s´c czo lowa i wewn_, etrzn_, a._,

3Liczy sie pocz_, atek redeksu._,

4Uwaga: czo lowa posta´c normalna nie jest na og´o l postacia normaln_, a._,

• Napiszemy M → N , gdy istnieje ci¹ⁱ ag redukcji wewn_, etrznych z M do N , kt´_, ore jed- nocze´snie stanowia redukcj_, e postaci_, → (´cwiczenie 4).¹

• Natomiast M V N zachodzi wtedy gdy M  P^h → N , oraz ka˙zdy term Q wyst¹ⁱ

epuj, acy_, w redukcji M  P spe lnia warunek Q^h → N (´¹ cwiczenie 5).

Lemat 5.2

(1) Je´sli M → N¹ⁱ → P , to M^h → Q^h → P , dla pewnego Q.¹

·

h

·

1i

@@

h 

·

·

1

@@

(2) Je´sli M V M⁰ oraz N V N⁰ to M [x := N ] V M⁰[x := N⁰] (∗∗) (3) Je´sli M → N , to M V N.¹

Dow´od: Cwiczenie.´

Lemat 5.3 Je˙zeli M β N , to M  P^h  N , dla pewnego P .ⁱ

Dow´od: Relacja V rozk lada sie z definicji na_,  i^h →, i na dodatek zawiera relacj¹ⁱ e, →¹ (lemat 5.2(3)). Zatem,

je´sli M → N , to M¹  L^h → N , dla pewnego L,¹ⁱ czyli→ rozk lada si¹

e na faz, e czo low_, a i faz_, e postaci_, →. Z lematu 5.2(1) wynika taki obrazek:¹ⁱ

·

h

·

1i

@@

h +

·

·

1i

@@

A wiec relacje_, → i¹ⁱ  mo˙zna permutowa´c, a to ju˙z wystarczy, bo przecie˙z^h → ⊆ⁱ → ⊆¹ⁱ .ⁱ Dow´od twierdzenia: Na mocy lematu 5.3 mamy M  M^{h 0}  N . Po wykonaniu wszyst-ⁱ kich redukcji czo lowych, kszta lt termu sie cz_, e´_,sciowo

”ustala”, je´sli wiec M_, ⁰ = λ~x.z ~R albo M⁰ = ~x.(λy.P )Q ~R, to dalsze redukcje odbywaja si_, e wewn_, atrz P , Q i ~_, R. Stosujac indukcj_, e do_, term´ow P , Q i ~R, otrzymujemy standardowe redukcje, kt´ore wykonujemy

”od lewej” tj. naj- pierw w P , potem w Q i potem w kolejnych wyrazach ciagu ~_, R.

Udowodnili´smy wiec twierdzenie o standaryzacji. A oto najwa˙zniejszy wniosek z niego._,

Wniosek 5.4 Je´sli M ma posta´c normalna N , to istnieje lewostronna redukcja z M do N ._, Powy˙zszy wniosek⁵ mo˙zna odczyta´c tak: Je´sli istnieje niesko´nczona redukcja lewostronna za- czynajaca si_, e od M , to term M nie ma postaci normalnej. Mo˙zna to stwierdzenie wzmocni´_, c w taki spos´ob. Powiemy, ˙ze niesko´nczony ciag redukcji jest quasi-lewostronny, je´_, sli niesko´ncze- nie wiele razy nastepuje w tym ci_, agu redukcja redeksu po lo˙zonego najbardziej na lewo._, Fakt 5.5 Je´sli istnieje niesko´nczony quasi-lewostronny ciag redukcji zaczynaj_, acy si_, e od M ,_, to term M nie ma postaci normalnej.

Dow´od: Na potrzeby tego dowodu powiedzmy, ˙ze term jest wytrzyma ly, gdy ma redukcje_, quasi-lewostronna, w kt´_, orej wystepuje niesko´nczenie wiele krok´ow postaci →. Zauwa˙zmy, ˙ze^h je´sli N jest wytrzyma ly, to N→ N^{h 0} dla pewnego wytrzyma lego termu N⁰ (´cwiczenie 6).

Za l´o˙zmy teraz, ˙ze M ma posta´c normalna. Przez indukcj_, e ze wzgl_, edu na jej d lugo´_, s´c udowod- nimy, ˙ze M nie mo˙ze mie´c niesko´nczonej redukcji quasi-lewostronnej. Przypu´s´cmy naj- pierw, ˙ze M jest termem wytrzyma lym. U˙zywajac ´_, cwiczenia 6 mo˙zna wtedy zdefiniowa´c ciag wytrzyma lych term´_, ow N_i, takich ˙ze N₀ = M oraz N_i^h+N_i+1dla dowolnego i ∈ N. Ina- czej m´owiac,_,

”wyciagaj_, ac na pocz_, atek” redukcje czo lowe otrzymamy niesko´_, nczona redukcj_, e_, czo lowa (w szczeg´_, olno´sci lewostronna) termu M . Nie mo˙ze wi_, ec istnie´_, c posta´c normalna.

Zatem je´sli M = M₀→ M₁ → M₂→ · · · jest niesko´nczona redukcj_, a quasi-lewostronn_, a, to od_, pewnego miejsca mamy tylko redukcje wewnetrzne postaci λ~_, z.y ~P → λ~ⁱ z.y ~P⁰→ λ~ⁱ z.y ~P⁰⁰→ · · ·ⁱ Spo´sr´od redukcji lewostronnych wystepuj_, acych w tym ci_, agu, niesko´_, nczenie wiele dotyczy tej samej sk ladowej wektora ~P , wiec wystarczy u˙zy´_, c za lo˙zenia indukcyjnego.

Cwiczenia´

1. Jaki jest parametr indukcji w dowodzie twierdzenia 5.1?

2. Pokaza´c, ˙ze niepusta redukcja jest standardowa wtedy i tylko wtedy, gdy jest jednej z postaci:

• (λx P )Q → P [x := Q] = M1→ · · · → Mn;

• λx M1→ λx M2→ · · · → λx Mn;

• M₁N₁→ · · · → M_nN₁→ · · · → M_nN_m,

gdzie ciagi M_{, 1}→ · · · → M_n i N₁→ · · · → N_msa standardowymi redukcjami._,

3. Diagram poni˙zej przedstawia naiwna pr´_, obe dowodu lematu 5.3. Na czym polega b l_, ad?_,

·

h

·

i @@ @@

h

·

·

i @@ @@

5Ten fakt bywa nazywany twierdzeniem o normalizacji . Obecnie rzadziej u˙zywa sie tej nazwy, bo_,

”norma- lizacja” zwykle oznacza istnienie postaci normalnych.