web counter


https://www.amazon.it/dp/B0CT9YL557

We support WINRAR [What is this] - [Download .exe file(s) for Windows]

CLASSICISTRANIERI HOME PAGE - YOUTUBE CHANNEL
SITEMAP
Audiobooks by Valerio Di Stefano: Single Download - Complete Download [TAR] [WIM] [ZIP] [RAR] - Alphabetical Download  [TAR] [WIM] [ZIP] [RAR] - Download Instructions

Make a donation: IBAN: IT36M0708677020000000008016 - BIC/SWIFT:  ICRAITRRU60 - VALERIO DI STEFANO or
Privacy Policy Cookie Policy Terms and Conditions
Rachunek lambda - Wikipedia, wolna encyklopedia

Rachunek lambda

Z Wikipedii

Rachunek lambda to 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 i Stephen Cole Kleene w 1930 roku.

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. Rachunek lambda z typami jest podstawą funkcyjnych języków programowania.

Spis treści

[edytuj] 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 wartości 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 albo 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) = xy, 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ć wg wzoru \lambda\, x\, y\, .\, x - y.

[edytuj] lambda-wyrażenia

Niech X będzie nieskończonym, przeliczalnym zbiorem zmiennych. Lambda-wyrażenie (lambda-term) definiuje się następująco:

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

Zbiór wszystkich lambda-wyrażeń oznacza się Λ.

Lambda-termy rozpatruje się najczęściej jako klasy abstrakcji relacji alfa-konwersji.

[edytuj] 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) \backslash \{x\}

[edytuj] 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:

  • true (prawda) to \lambda\;x\;.\;\lambda\;y\;.\;x,
  • false (fałsz) to \lambda\;x\;.\;\lambda\;y\;.\;y.

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

Rozwiniętą implikację "jeśli A, to B, w przeciwnym razie C" zapisać można jako A\;B\;C, czyli (A\;B)\;C.

[edytuj] Przykład

Obliczmy wartość wyrażenia "prawda i fałsz", czyli w rachunku lambda

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

czyli "fałsz" zgodnie z naszymi oczekiwaniami.

[edytuj] Struktury danych

Para złożona z Y i Z to λ x . x Y Z Pierwszy element wyciąga się za pomocą PARA PRAWDA, drugi przez PARA FAŁSZ.

Listy można konstruować następującym sposobem:

  • NIL to \lambda\;x\;.\;true
  • CONS to PARA wartość i lista

następująca funkcja zwraca true jeśli argumentem jest NIL i false jeśli to CONS: \lambda\;x\;.\;x\;(\lambda\;a\;b\;.\;{false})

[edytuj] Zobacz też

Static Wikipedia 2008 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu -

Static Wikipedia 2007 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu -

Static Wikipedia 2006 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu -

Sub-domains

CDRoms - Magnatune - Librivox - Liber Liber - Encyclopaedia Britannica - Project Gutenberg - Wikipedia 2008 - Wikipedia 2007 - Wikipedia 2006 -

Other Domains

https://www.classicistranieri.it - https://www.ebooksgratis.com - https://www.gutenbergaustralia.com - https://www.englishwikipedia.com - https://www.wikipediazim.com - https://www.wikisourcezim.com - https://www.projectgutenberg.net - https://www.projectgutenberg.es - https://www.radioascolto.com - https://www.debitoformtivo.it - https://www.wikipediaforschools.org - https://www.projectgutenbergzim.com