8 Lambda-teorie i drzewa B¨ ohma

Jak ju˙z m´owili´smy, zwyk ly rachunek lambda mo˙zna uwa˙za´c (w uproszczeniu) za pewna teori_, e_, r´owno´sciowa. Inn_, a teori_, e otrzymamy, je´_, sli do aksjomat´ow beta-konwersji do lo˙zymy eksten-sjonalo´s´c w postaci regu ly (ext) lub aksjomatu (η). A co je´sli doda´c jako nowy aksjomat na przyk lad r´owno´s´c K = S? Wtedy dla dowolnego termu M wywnioskujemy

M = SI(KM )I = KI(KM )I = I,

a wiec takie rozszerzenie rachunku lambda by loby sprzeczne. Termy K i S to tylko przyk lad.

Okazuje sie, ˙ze sprzeczna musi by´_, c ka˙zda teoria, kt´ora skleja ze soba dwie r´_, o˙zne postaci βη-normalne. Wynika to z nastepuj_, acego twierdzenia B¨_, ohma:

Twierdzenie 8.1 (C. B¨ohm, 1968) Niech M i N bed_, a kombinatorami w postaci β-nor-_, malnej i niech M 6=_βη N . Wtedy istnieje taki ciag zamkni_, etych term´_, ow ~P , ˙ze M ~P =_β true oraz N ~P =β false.

Zobaczmy na przyk ladzie jak mo˙zna rozr´o˙zni´c dwa termy. Niech M = λxy.x(λz.xzy)y i N = λxy.x(λzv.xzxv)y. Wygodnie jest przedstawi´c te termy za pomoca drzew (Obrazek 10)._,

λxy. x λxy. x

λz. x y λzv. x y

z y z x v

Obrazek 10: Drzewa dla M = λxy.x(λz.xzy)y i N = λxy.x(λzv.xzxv)y

Istotna r´o˙znica pomiedzy tymi drzewami to li´_, scie odpowiadajace zmiennej y w termie M_, i zmiennej x w termie N . (Wystapienie v w termie N jest nieistotne, bo λzv.xzxv =_, η λz.xzx.) Aby wykorzysta´c te r´_, o˙znice do_,

”odseparowania” term´ow M i N nale˙zy zaaplikowa´c je do takich argument´ow, kt´ore wyciagn_, a z nich_,

”na wierzch” w la´snie te li´scie. Pos lu˙zymy sie trickiem,_, zwanym

”B¨ohm-out technique”. Niech P = λuw.hu, wi. Wtedy dla dowolnego Q zachodzi M P Q =_β hλz.hz, Qi, Qi. Dalej M P Q true R false =_β Q dla dowolnego R. Tymczasem N P Q true R false =β P . Wybierzmy wiec jakiekolwiek R oraz Q = λuvw. true i niech ~_, P oznacza ciag (P, Q, true, R, false, false, I, true). Wtedy M ~_, P =_β true oraz N ~P =_β false.

Dow´od twierdzenia B¨ohma

Przypomnijmy, ˙ze true = λxy. x, false = λxy. y oraz π^k_i = λx₁. . . x_k. x_i dla i ≤ k. Uog´ olnie-niem pary uporzadkowanej hM, N i = λf. f M N jest p-krotka:_,

hM₁, . . . , M_pi = λf. f M₁. . . M_p.

Przez T_p oznaczymy operator tworzenia krotki, tj. T_p = λx₁. . . x_pλf. f x₁. . . x_p.

Podstawienie postaci S = [xi := Tpi]i=1,...,n nazwiemy m-podstawieniem, gdy liczby p1, . . . pn

sa parami r´_, o˙zne i wieksze od m._, Termy M i N sa m-rozr´_, o˙znialne gdy dla dowolnego m-podstawienia S o dziedzinieFV(M ) ∪FV(N ) istnieje taki ciag kombinator´_, ow ~L, ˙ze:

M [S]~L β true oraz N [S]~L β false.

Termy rozr´o˙znialne, to takie, kt´ore sa m-rozr´_, o˙znialne dla pewnego m. Zauwa˙zmy, ˙ze rozr´ o˙z-nialno´s´c jest relacja symetryczn_, a. Je´_, sli bowiem M i N sa m-rozr´_, o˙znialne, to tak˙ze N i M sa_, m-rozr´o˙znialne, bo true false true β false oraz false false true β true.

Twierdzenie B¨ohma udowodnimy pokazujac, ˙ze eta-r´_, o˙zne postaci normalne musza by´_, c rozr´ o˙z-nialne (lemat 8.6).

Lemat 8.2 Je´sli termy M i N sa rozr´_, o˙znialne, to λx M i λx N te˙z sa rozr´_, o˙znialne.

Dow´od: Za l´o˙zmy, ˙ze M i N sa m-rozr´_, o˙znialne. We´zmy m-podstawienie S i niech p > m bedzie nowe (takie, ˙ze T_, p nie wystepuje w S). Wtedy S_, ⁰= S[x := Tp] jest m-podstawieniem, wiec M [S_, ⁰]~L β true oraz N [S⁰]~L β false dla odpowiedniego ciagu kombinator´_, ow ~L.

Zatem (λx M )[S]T_pL →~ _β M [S][x := T_p]~L = M [S⁰]~L β true i podobnie term (λx N )[S]T_pL~ redukuje sie do false._,

Lemat 8.3 Je´sli x 6∈FV(N ) i termy M i N x sa rozr´_, o˙znialne, to termy λx M i N te˙z.

Dow´od: Za l´o˙zmy, ˙ze M i N x sa m-rozr´_, o˙znialne. Niech S bedzie m-podstawieniem i niech_, S(x) = T_p. Istnieje taki ciag ~_, L, ˙ze M [S]~L β true oraz N [S]T_p~L β false. Poniewa˙z x jest zwiazane w termie λx M , wi_, ec (λx M )[S] = λx M [S_, ⁰] gdzie S⁰ to S ograniczone do zmiennych r´o˙znych od x. Zatem (λx M )[S]T_p~L = (λx M [S⁰])T_p~L →_β M [S]~L β true i ju˙z dobrze.

Lemat 8.4 Je´sli x 6= y i termy M = xP₁. . . P_k i N = yQ₁. . . Q_` sa w postaci normalnej,_, to M i N sa rozr´_, o˙znialne.

Dow´od: Wybierzmy m ≥ k, ` i rozpatrzmy dowolne m-podstawienie S. Niech S(x) = Tp

i S(y) = T_q. Wtedy M [S] = T_pP₁[S] . . . P_k[S] β λ~uf. f P₁[S] . . . P_k[S]~u, gdzie wektor zmien-nych ~u jest d lugo´sci p − k. Podobnie N [S] = T_qQ₁[S] . . . Q_{`</sub>[S] β λ~vg. gQ<sub>1</sub>[S] . . . Q<sub>`}[S]~v, gdzie wektor ~v ma d lugo´s´c q − `.

Za l´o˙zmy najpierw, ˙ze wektory ~u i ~v sa r´_, o˙znej d lugo´sci, np. p − k < q − `. Wtedy mo˙zemy bez straty og´olno´sci za lo˙zy´c, ˙ze ~v = ~uf ~w, czyli ˙ze N [S] β λ~uf ~w g. gQ<sub>1</sub>[S] . . . Q<sub>`</sub>[S]~u f ~w. Je´sli teraz ~L = L1. . . Lq−`+1 jest dowolnym ciagiem kombinator´<sub>,</sub> ow d lugo´sci q − ` + 1, to:

M [S]~L β L_p−k+1P1[S] . . . P_k[S]L1. . . L_p−kL_p−k+2. . . L_{q−`+1</sub>; N [S]~L β L<sub>q−`+1}Q₁[S] . . . Q_{`</sub>[S]L<sub>1</sub>. . . L<sub>q−`}.

Przy tym p − k + 1 6= q − ` + 1, wiec wystarczy wzi<sub>,</sub> a´<sub>,</sub>c L<sub>p−k+1</sub> = λy<sub>1</sub>. . . y<sub>q−l+k</sub>. true oraz L<sub>q−`+1</sub> = λz1. . . zq. false i dostaniemy M [S]~L β true i N [S]~L β false. Pozosta le termy L_i moga by´_, c jakiekolwiek, np. L_i = I dla i 6= p − k + 1, q − ` + 1.

Za l´o˙zmy teraz, ˙ze p − k = q − `. Mo˙zemy wtedy przyja´<sub>,</sub>c, ˙ze N [S] β λ~uf. f Q<sub>1</sub>[S] . . . Q<sub>`</sub>[S]~u.

Poniewa˙z p 6= q, wiec k 6= `; przypu´<sub>,</sub> s´cmy, ˙ze k > ` i p > q. Niech ~L = L1. . . Lp−k, gdzie L₁ = λz₁. . . z_{k−`</sub>. true, oraz L<sub>k−`+1} = false. (Uwaga: k − ` + 1 ≤ p − k = q − `, bo k < q.) Pozosta le termy L_i sa nieistotne. Aplikuj_, ac M [S] i N [S] do argument´_, ow ~Lπ^p_k+1, dostajemy:

M [S]~Lπ^p_k+1β π^p_k+1P₁[S] . . . P_k[S]~L β L₁, poniewa˙z ciag P_{, 1}[S] . . . P_k[S]~L ma d lugo´s´c p.

N [S]~Lπ^p_k+1β π_k+1^p Q₁[S] . . . Q_{`</sub>[S]~L β λ ~w. L<sub>k−`+1}, bo teraz ciag argument´_, ow jest kr´otszy.

Wektor zmiennych ~w jest d lugo´sci k − `. Dlatego nasze termy zaaplikujemy jeszcze do k − ` egzemplarzy kombinatora I i dostaniemy:

M [S]~Lπ_{`+1</sub><sup>p</sup> I . . . I β L1I . . . I β true oraz N [S]~Lπ<sup>p</sup><sub>`+1}I . . . I β L_k−`+1= false.

Lemat 8.5 Je´sli k 6= ` i termy M = xP<sub>1</sub>. . . P<sub>k</sub> i N = xQ<sub>1</sub>. . . Q<sub>`</sub> sa w postaci normalnej,_, to M i N sa rozr´_, o˙znialne.

Dow´od: Za l´o˙zmy, ˙ze k < `. Wybierzmy m ≥ k, ` i niech S bedzie m-podstawieniem._, Wtedy S(x) = Tp, przy czym p > k, `. Zatem

M [S] β λ~u f. f P₁[S] . . . P_k[S]~u oraz N [S] β λ~v g. gQ₁[S] . . . Q<sub>`</sub>[S]~v, gdzie wektory ~u i ~v sa odpowiednio d lugo´<sub>,</sub> sci p − k i p − `. Wektor ~u jest d lu˙zszy i mo˙zemy przyja´_,c ~u = ~v g ~w. A wiec M [S] _, β λ~v g ~w f. f P1[S] . . . Pk[S]~v g ~w. Niech ~L = L1. . . Lp−k+1, gdzie L_p−k+1 = λy1. . . yp. true, L_{p−`+1</sub> = λz1. . . z<sub>p−k+`}. false, oraz Lj = I w przeciwnym przypadku. Wtedy

M [S]~L β Lp−k+1P1[S] . . . Pk[S]I . . . ILp−`+1I . . . I β true, N [S]~L β L<sub>p−`+1</sub>Q1[S] . . . Q_`[S]I . . . IL_p−k+1 β false.

Twierdzenie B¨ohma wynika bezpo´srednio z nastepnego lematu._,

Lemat 8.6 Je´sli M i N sa postaciami β-normalnymi i M 6=_{, η} N , to M i N sa rozr´_, o˙znialne.

Dow´od: Indukcja ze wzgledu na sum_, e d lugo´_, sci term´ow M i N , liczona bez nawias´_, ow i kropek, ale za to z lambdami, np. term λxy. x ma d lugo´s´c 4, a term x(yz) ma d lugo´s´c 3.

Je´sli oba termy M i N sa abstrakcjami, to teza wynika z za lo˙zenia indukcyjnego i lematu 8.2._, Je´sli M = λx M⁰ jest abstrakcja, ale N nie, to we´_, zmy x 6∈ FV(M ) ∪FV(N ) i rozpatrzmy termy M = λx M⁰i N⁰ = N x. Wtedy M⁰6=_η N x, a poniewa˙z suma d lugo´sci term´ow M⁰ i N x jest mniejsza o jeden od sumy d lugo´sci term´ow M i N (z powodu usuniecia lambdy), wi_, ec_, mo˙zemy zastosowa´c za lo˙zenie indukcyjne do M⁰ i N x, a nastepnie odwo la´_, c sie do lematu 8.3._, Za l´o˙zmy wiec, ˙ze ani M ani N nie jest abstrakcj_, a. Je´_, sli termy M i N maja inne zmienne_, czo lowe, to stosuje sie lemat 8.4, je´_, sli zmienna czo lowa jest ta sama, ale liczba argument´ow jest inna, to u˙zyjemy lematu 8.5. Pozostaje przypadek, gdy jedno i drugie jest takie samo. A wiec_, M = xP1. . . Pki N = xQ1. . . Qk. Skoro M 6=η N , to jest takie i ≤ k, ˙ze Pi6=_η Qi. Z za lo˙zenia indukcyjnego jest takie m, ˙ze termy Pi i Qi sa m-rozr´_, o˙znialne, a wiec tak˙ze m_, ⁰-rozr´o˙znialne gdy m⁰ ≥ m. We´zmy m⁰ ≥ m, k i dowolne m⁰-podstawienie S, takie ˙ze S(x) = T_p jest okre´slone. Wtedy P_i[S]~L β true i Q_i[S]~L β false, dla pewnego ~L. Ponadto:

M [S] = TpP1[S] . . . Pk[S] β λ~uf. f P1[S] . . . Pk[S]~u;

N [S] = TpQ1[S] . . . Q_k[S] β λ~uf. f Q1[S] . . . Q_k[S]~u, gdzie wektor ~u jest d lugo´sci p − k. Stad_,

M [S]I . . . Iπ_i^pL ~ β π_i^pP1[S] . . . Pk[S]I . . . I~L β Pi[S]~L β true i podobnie N [S]I . . . Iπ_i^pL ~ β false.

Rozwiazalno´_, s´c

Pierwsza intuicja zwiazana z rachunkiem lambda (rozumianym jako abstrakcyjny j_, ezyk pro-_, gramowania) jest taka:

”warto´scia” termu jest jego posta´_, c normalna. A zatem term, kt´ory nie ma postaci normalnej jest pozbawiony warto´sci. Ka˙zdy taki term jest r´ownie dobry, albo

raczej r´ownie z ly, i nie powinno by´c przeszk´od w uto˙zsamieniu ich wszystkich ze soba. Nie-_, stety, uto˙zsamienie na przyk lad term´ow λx.xKΩ i λx.xSΩ daje w wyniku sprzeczna teori_, e_,

— wystarczy oba zaaplikowa´c do K. Dostajemy konkretne i r´o˙zne rezultaty: K i S.

Term bez postaci normalnej mo˙ze wiec czasem objawia´_, c dobrze okre´slone dzia lanie, czyli w pewnym sensie mie´c

”warto´s´c”. Mo˙zna uwa˙za´c, ˙ze ta warto´_, scia jest czo lowa posta´_, c nor-malna, o ile istnieje. Przypomnijmy, ˙ze czo lowa posta´c normalna to ka˙zdy term postaci λ~x.z ~R.

Term M ma czo lowa posta´_, c normalna N gdy M =_{, β} N i N jest w czo lowej postaci normalnej.

Lemat 8.7 Je´sli term M N ma czo lowa posta´_, c normalna to M te˙z._,

Dow´od: Je´sli term M nie ma czo lowej postaci normalnej, to ciag redukcji czo lowych_, M = M₀ → M^h ₁ → · · · jest niesko´^h nczony. Je´sli ˙zadne M_i nie jest abstrakcja, to mamy_, te˙z niesko´nczona redukcj_, e M N = M_, 0N → M^h ₁N → · · · Niech wi^h ec M_, i bedzie pierwsz_, a_, abstrakcja, tj. M_, i = λu.Ni h

→ λu.N_i+1 → λu.N^h _i+2 → · · · gdzie N^h _i → N^h _i+1 → N^h _i+2· · · Wtedy M N  M^h iN → N^h _i[u := N ] → N^h _i+1[u := N ] → · · · , bo N^h _i → N^h _i+1 implikuje Ni[u := N ]→ N^h _i+1[u := N ].

Powiemy, ˙ze term zamkniety M jest rozwi_, azalny je˙zeli M ~_, P =_β I dla pewnych kombinato-r´ow ~P . Term ze zmiennymi wolnymi ~x jest rozwiazalny je˙zeli rozwi_, azalne jest jego domkni_, ecie,_, czyli kombinator λ~x.M

Wniosek 8.8 Term jest rozwiazalny wtedy i tylko wtedy, gdy ma czo low_, a posta´_, c normalna._, Dow´od: Bez straty og´olno´sci mo˙zna za lo˙zy´c, ˙ze mowa o termie zamknietym._,

Je´sli M =_β λx₁x₂. . . x_n.x_iR₁. . . R_m, to oczywi´scie M P₁P₂. . . P_n=_β I, gdzie P_i = λy₁. . . y_m.I.

Na odwr´ot, je˙zeli M ~P =β I, to w istocie M ~P β I. Skoro wiec M ~_, P ma czo lowa posta´_, c normalna I, to i M musi mie´_, c czo lowa posta´_, c normalna (lemat 8.7 plus indukcja)._,

Je´sli termy nierozwiazalne (niezdolne do dobrze okre´_, slonego zachowania) uznamy za pozba-wione warto´sci, to znaczy, ˙ze postulujemy teorie r´_, owno´sciowa, w kt´_, orej te wszystkie termy sa_, r´owne. Jakie rozwiazalne termy powinny by´_, c r´owne w tej teorii? Te, kt´orych zachowanie jest jednakowe. Zdolno´s´c do sensownego zachowania przejawia sie istnieniem czo lowej postaci nor-_, malnej, ale nie mo˙zemy identyfikowa´c term´ow za pomoca ich czo lowych postaci normalnych,_, bo term rozwiazalny mo˙ze ich mie´_, c nawet niesko´nczenie wiele. Nie mo˙zemy sie te˙z pos lu˙zy´_, c beta-r´owno´scia, bo chcemy aby xΩ by lo w naszej teorii r´_, owne x(Ωy). Pozostaje obserwowa´c zachowanie term´ow w r´o˙znych sytuacjach. Je´sli jest ono zawsze takie samo, to powinni´smy dane termy uto˙zsami´c.

Niech M i N bed_, a dowolnymi termami i niech_, FV(M ) ∪FV(N ) = ~x. Powiemy, ˙ze M i N sa_, obserwacyjnie r´ownowa˙zne, i napiszemy M ≡ N , gdy dla dowolnego kombinatora P ,

P (λ~x.M ) jest rozwiazalny_, ⇐⇒ P (λ~x.N ) jest rozwiazalny._,

Nietrudno zauwa˙zy´c, ˙ze ≡ jest rozszerzeniem ekstensjonalnej teorii r´owno´sciowej λβη, i ˙ze M ≡ N dla dowolnych nierozwiazalnych M i N (´_, cwiczenie 3). Ponadto, z twierdzenia B¨ohma wynika, ˙ze dla term´ow w postaci normalnej zachodzi r´ownowa˙zno´s´c

M ≡ N ⇐⇒ M =_βη N.

Drzewa B¨ohma

Drzewo B¨ohma termu M , oznaczane przez BT (M ), definiujemy przez ko-indukcje._,

• Je´sli term M jest nierozwi

azalny, to BT (M ) sk lada si, e tylko z jednego wierzcho lka,_, oznaczonego przez Ω.

• Je´sli term M ma czo lowa posta´_, c normalna λ~_, x.yP₁. . . P_n, to drzewo BT (M ) jest zbu-dowane jak na Obrazku 11.

λ~x. y

BT (P₁) BT (P₂) . . . BT (P_n)

Obrazek 11: Drzewo BT (λ~x.yP1. . . Pn)

Drzewo B¨ohma to uog´olnienie postaci normalnej. Zwyk la posta´c normalna to sko´nczone drzewo B¨ohma bez wystapie´_, n Ω.

Chcemy teraz uog´olni´c pojecie eta-redukcji i eta-r´_, owno´sci na drzewa B¨ohma. Oczywi´scie B →η B⁰ oznacza jeden krok redukcji. Jednak definicja eta-r´owno´sci powinna uwzglednia´_, c to,

˙ze niesko´nczone drzewa moga mie´_, c niesko´nczenie wiele eta-redeks´ow. Musimy wiec pozwoli´_, c na to, ˙ze eta-r´ownowa˙zne drzewa r´o˙znia si_, e w niesko´_, nczenie wielu miejscach.

Oczywi´scie drzewo B¨ohma mo˙zna uwa˙za´c za

”granice” ci_, agu term´_, ow sko´nczonych, w kt´orych mo˙ze wystepowa´_, c sta la Ω. ´Sci´slej, powiemy, ˙ze ciag drzew T_, n jest zbie˙zny do drzewa B je˙zeli dla dowolnego n istnieje takie m, ˙ze wszystkie drzewa T_m, T_m+1, . . . sa do g l_, eboko´_, sci n identyczne z drzewem B. Ciag sko´_, nczony jest za´s zbie˙zny do swojego ostatniego elementu.

Powiemy, ˙ze drzewa B¨ohma B i B⁰ sa η-r´_, ownowa˙zne (B ≈η B⁰), gdy istnieja (sko´_, nczone lub niesko´nczone) ciagi eta-ekspansji:_,

B = B_{0 η}← B_{1 η}← B_{2 η}← B_{3 η}← · · · oraz B⁰ = B⁰_{0 η}← B_{1 η}⁰ ← B_{2 η}⁰ ← B_{3 η}⁰ ← · · · zbie˙zne do tego samego drzewa. Przebrnawszy przez t_, e ostatni_, a definicj_, e, mo˙zemy sfor-_, mu lowa´c twierdzenie Wadswortha:

Twierdzenie 8.9 (Wadsworth, 1975) Termy M i N sa obserwacyjnie r´_, ownowa˙zne wtedy i tylko wtedy, gdy BT (M ) ≈_η BT (N ).

Dow´od z lewej do prawej polega na zastosowaniu techniki

”B¨ohm-out ”. W przeciwna stron_, e_, stosuje sie metody semantyczne._,

Cwiczenia´

1. Skonstruowa´c takie X, ˙ze X(λyz.y(yz(yy))z) βηK oraz X(λyz.y(yz(yz))z) βη S.

2. Udowodni´c, ze je´sli M nie ma czo lowej postaci normalnej, to ˙zaden term postaci M [x := P ] nie ma czo lowej postaci normalnej. Wskaz´owka: Je´sli M→ N , to M [x := P ]^h → N [x := P ].^h 3. Udowodni´c, ze je´sli M nie ma czo lowej postaci normalnej, ale P M ma czo lowa posta´_, c normalna,_,

to ka˙zdy term postaci P N ma czo lowa posta´_, c normalna. Wskaz´_, owka: Jak wyglada czo lowa_, posta´c normalna termu P ?

4. Tradycyjna definicja obserwacyjnej r´ownowa˙zno´sci pos luguje sie poj_, eciem kontekstu czyli termu_, z ”dziura”. Umieszczenie termu M w kontekscie C[ ] (czyli w lo˙zenie go do_,

”dziury” [ ]) daje w wyniku term C[M ], w kt´orym zmienne wolne M moga zosta´_, c zwiazane abstrakcjami w C[ ]._, Pokaza´c, ˙ze M ≡ N wtedy i tylko wtedy, gdy dla dowolnego kontekstu C[ ],

C[M ] jest rozwiazalny_, ⇐⇒ C[N ] jest rozwiazalny._,

5. Za l´o˙zmy, ˙ze kombinatory M i N sa obserwacyjnie r´_, ownowa˙zne, i ˙ze P M =βη λx1. . .xn. xiA1. . .Ak, dla pewnych A₁, . . . , A_k. Udowodni´c, ˙ze P N =_βη λx₁. . .x_n. x_iB₁. . .B_k dla pewnych B₁, . . . , B_k. 6. Znale´z´c term, kt´orego drzewo B¨ohma to jedna niesko´nczona ga la´_,z postaci λx₁.x₁(λx₂.x₂(λx₃. . .

Wskaz´owka: u˙zy´c kombinatora Y.

7. Skonstruowa´c term M o takiej w lasno´sci: drzewo B¨ohma BT (M ) jest niesko´nczone i ka˙zdy jego wierzcho lek ma wiecej syn´_, ow ni˙z mia l jego ojciec.

Rozwiazanie: M = YF 1, gdzie F = λV λnλx.n(λy.y(V (succ n))x)._,

8. Czy istnieje taki term M , ˙ze drzewo BT (M ) ma kszta lt λx0.x1(λx2.x3(λx4. . . . ? 9. Niech J = Y(λf xy. x(f y)). Opisa´c drzewo BT (J). Czy BT (J) ≈ηBT (I)?