2015年莲都区政协第十四届四次会议重点提案目录

百度 　　据市交通委相关人士透露，作为无障碍出租车，目前这款“老爷车”的招投标工作已经完成，总共有200辆车，由强生出租中标。

Rachunek lambda – system formalny u?ywany do badania zagadnień zwi?zanych z podstawami matematyki jak rekurencja, definiowalno?? funkcji, obliczalno??, podstawy matematyki np. definicja liczb naturalnych, warto?ci logicznych itd. Rachunek lambda zosta? wprowadzony przez Alonzo Churcha w 1930 roku. Jest uniwersaln? reprezentacj? obliczeń i równoznaczny maszynie Turinga, tzn. dowolne wyra?enie w rachunku lambda mo?na przedstawi? jako program na maszynie Turinga i odwrotnie. Zosta? u?yty do udowodnienia hipotezy, nazwanej pó?niej hipotez? Churcha-Turinga.

Rachunek lambda jest przydatny do badania algorytmów. Wszystkie algorytmy, które dadz? si? zapisa? w rachunku lambda, dadz? si? zaimplementowa? na maszynie Turinga i odwrotnie.

Istnieje wiele rodzajów rachunku lambda, z czego najprostszym jest rachunek lambda bez typów, stanowi?cy pierwotn? inspiracj? dla powstania programowania funkcyjnego (Lisp). Rachunek lambda z typami jest podstaw? dzisiejszych systemów typów w j?zykach programowania.

Opis nieformalny

W rachunku lambda ka?de wyra?enie okre?la funkcj? jednoargumentow?. Z kolei argumentem tej funkcji jest równie? funkcja jednoargumentowa, warto?ci? funkcji jest znów funkcja jednoargumentowa. Funkcja jest definiowana anonimowo przez wyra?enie lambda, które opisuje, co funkcja robi ze swoim argumentem.

Funkcja $f$ zwracaj?ca argument powi?kszony o dwa, któr? mo?na by matematycznie zdefiniowa? jako $f(x)=x+2,$ w rachunku lambda ma posta? $\lambda \ x\,.\,x+2$ (nazwa parametru formalnego jest dowolna, wi?c $x$ mo?na zast?pi? inn? zmienn?). Z kolei warto?? funkcji w punkcie, np. $f(3)$ ma zapis $(\lambda \,x\,.\,x+2)\,3.$ Warto wspomnie? o tym, ?e funkcja jest ??czna lewostronnie wzgl?dem argumentu, tzn. $f\,x\,y=(f\,x)\,y.$

Poniewa? wszystko jest funkcj? jednoargumentow?, mo?emy zdefiniowa? zmienn? o zadanej warto?ci – nazwijmy j? $a.$ Funkcja $a$ jest oczywi?cie sta?a, cho? nic nie stoi na przeszkodzie, aby by?a to dowolna inna funkcja. W rachunku lambda $a$ jest dane wzorem $\lambda \,a\,.\,a\,3.$

Teraz jeste?my w stanie dokona? klasycznego otrzymania warto?ci w punkcie lub te? lepiej rzecz ujmuj?c, wykona? z?o?enie funkcji, mianowicie $f\circ a=f(a).$ Niech $f$ b?dzie dana jak poprzednio, wtedy: $(\lambda \,f\,.\,f\,3)(\lambda \,x\,.\,x+2)$ i dalej $(\lambda \,x\,.\,x+2)\,3,$ a wi?c otrzymujemy po prostu $3+2.$

Funkcj? dwuargumentow? mo?na zdefiniowa? za pomoc? techniki zwanej curryingiem, mianowicie jako funkcj? jednoargumentow?, której wynikiem jest znowu funkcja jednoargumentowa. Rozpatrzmy funkcj? $f(x,y)=x-y,$ której zapis w rachunku lambda ma posta? $\lambda \,x\,.\,\lambda \,y\,.\,x-y.$ Aby upro?ci? zapis stosuje si? powszechnie konwencj?, aby funkcje ?curried” zapisywa? wed?ug wzoru $\lambda \,x\,y\,.\,x-y.$

Wyra?enia lambda

Niech $X$ b?dzie nieskończonym, przeliczalnym zbiorem zmiennych. Wyra?enie lambda definiuje si? nast?puj?co:

• Je?eli $x\in X$ to $x$ jest wyra?eniem lambda,
• Je?eli $M$ jest wyra?eniem lambda i $x\in X,$ to napis $\lambda x.M$ jest wyra?eniem lambda,
• Je?eli $M$ oraz $N$ s? wyra?eniami lambda, to napis $(NM)$ jest wyra?eniem lambda,
• Wszystkie wyra?enia lambda mo?na utworzy? korzystaj?c z powy?szych regu?.

Zbiór wszystkich wyra?eń lambda oznacza si? $\Lambda .$

Wyra?enia lambda rozpatruje si? najcz??ciej jako klasy abstrakcji relacji alfa-konwersji.

Zmienne wolne

Zbiór zmiennych wolnych definiuje si? nast?puj?co:

• $FV(x)=\{x\}$
• $FV(MN)=FV(M)\cup FV(N)$
• $FV(\lambda x.M)=FV(M)-\{x\}$

Logika

U?ycie warto?ci liczbowych do oznaczania warto?ci logicznych mo?e prowadzi? do nie?cis?o?ci przy operowaniu relacjami na liczbach, dlatego te? nale?y wyra?nie oddzieli? logik? od obiektów, na których ona operuje. Z tego powodu oczywistym staje si? fakt, ?e warto?ci logiczne prawdy i fa?szu musz? by? elementami skonstruowanymi z wyra?eń tego rachunku.

Warto?ciami logicznymi nazwiemy funkcje dwuargumentowe, z których jedna zawsze b?dzie zwraca? pierwszy argument, a druga – drugi:

• ${\mbox{true}}$ (prawda) to $\lambda xy.x,$
• ${\mbox{false}}$ (fa?sz) to $\lambda xy.y.$

Teraz chc?c ukonstytuowa? operacje logiczne stosujemy nasze ustalone warto?ci tak, by wyniki tych operacji by?y zgodne z naszymi oczekiwaniami, mamy:

• ${\mbox{not}}$ (negacja) to $\lambda x.x\;{\mbox{false true}},$
• ${\mbox{and}}$ (koniunkcja) to $\lambda xy.xy\;{\mbox{false}},$
• ${\mbox{or}}$ (alternatywa) to $\lambda xy.x\;{\mbox{true}}\;y.$

Rozwini?t? implikacj? ?je?li $A,$ to $B,$ w przeciwnym razie $C$” zapisa? mo?na jako $A\;B\;C,$ czyli $(A\;B)\;C.$

Przyk?ad

Obliczmy warto?? wyra?enia ?prawda i fa?sz”, czyli w rachunku lambda

${\mbox{and true false}}=(\lambda xy.xy\;{\mbox{false}})\;{\mbox{true false}}={\mbox{true false false}}=(\lambda xy.x)\;{\mbox{false false}}={\mbox{false}},$

czyli ?fa?sz” zgodnie z oczekiwaniami.

Struktury danych

Para $p$ z?o?ona z elementów $x$ i $y$ to $\lambda z.zxy$ Pierwszy element wyci?ga si? za pomoc? $p\;{\mbox{true}},$ natomiast drugi przez $p\;{\mbox{false}}.$

Listy mo?na konstruowa? nast?puj?cym sposobem:

• NIL to $\lambda x.{\mbox{true}}$
• CONS to PARA warto?? i lista

Nast?puj?ca funkcja zwraca ${\mbox{true}},$ je?li argumentem jest NIL, oraz ${\mbox{false}},$ je?li to CONS: $\lambda x.x(\lambda ab.{\mbox{false}})$

Rekurencja w rachunku lambda

Rachunek lambda z pozoru nie ma ?adnego mechanizmu, który umo?liwia?by rekurencj? – nie mo?na odwo?ywa? si? w definicji do samej funkcji. A jednak rekurencj? mo?na osi?gn?? poprzez operator paradoksalny Y.

Paradoks polega na tym ?e dla ka?dego F zachodzi:

Y F = F (Y F)

Tak wi?c np. funkcja negacji nie jest mo?liwa do zaimplementowania w postaci ogólnej, gdy?:

(Y nie) = nie (Y nie)

Funkcja rekurencyjna musi pobra? siebie sam? jako warto??.

Dzia?a to w nast?puj?cy sposób:

(Y f) n

f (Y f) n

λ f. λ n. cia?o_f

gdzie cia?o_f mo?e si? odwo?ywa? do siebie samej

Np.:

silnia = Y (λ f. λ n. if_then_else (is_zero n) 1 (mult n (f (pred n))))

Zobacz te?

• arytmetyka w rachunku lambda
• konwersja α
• rachunek kombinatorów
• redukcja β
• S-wyra?enie

Linki zewn?trzne

• JesseJ. Alama JesseJ., The Lambda Calculus, [w:] Stanford Encyclopedia of Philosophy, CSLI, Stanford University, 21 marca 2018, ISSN 1095-5054 [dost?p 2025-08-08]  (ang.). (Rachunek lambda)
• ShaneS. Steinert-Threlkeld ShaneS., Lambda Calculi, Internet Encyclopedia of Philosophy, ISSN 2161-0002 [dost?p 2025-08-08]  (ang.).
• Lambda calculus (ang.), Routledge Encyclopedia of Philosophy, rep.routledge.com [dost?p 2025-08-08].