Kalkulong lambda

Sa lohikang matematikal at agham pangkompyuter, ang kalkulong lambda na isinusulat ding λ-kalkulo ang pormal na sistema para sa paglalarawan ng punsiyon, aplikasyon ng punsiyon at rekursiyon. Ang bahagi ng kalkulong lambda na mahalaga sa komputasyon ay tinatawag na walang-tayp na kalkulong lambda(untyped lambda calculus). Sa parehong may-tayp at walang-tayp na mga bersiyon, ang mga ideya mula sa kalkulong lambda ay nakatagpo ng aplikasyon sa larangan ng lohika, teoriya ng rekursiyon(komputabilidad) at linguistiks at may mahalagang papel na ginagampanan sa pagkakalikha ng teoriya ng mga wikang pamprograma kung saan ang walang-tayp ng kalkulong lambda ang orihinal na inspirasyon para sa pagpoprogramang punsiyonal partikular na ang Lisp at ang may-tayp na kalkulong lambda ay nagsisilbing pundasyon ng modernong mga sistemang tayp.

Pagkakatumbas na Alpha

Ang basikong anyon ng pagkakatumbas na mailalarawan sa mga terminong lambda ang pagkakatumbas na alpha. Ito ay nagsasaad na ang partikular na mapagpipilian ng binibigkis na bariabulo sa abstraksiyong lambda ay karaniwang hindi mahalaga.
Halimbawa, ang λx.x at λy.y ay magkatumbas-na-alpha na mga terminong lambda na kumakatawan sa parehong punsiyong identidad.
Pansinin na ang mga terminong x at y ay hindi magkatumbas na alpha dahil ang mga ito ay hindi binibigkis sa isang abstraksiyong lambda. 
Sa maramign mga presentasyon, karaniwan na tinutukoy ang mga magkatumbas na alpha na mga terminong lambda.
Ang mga sumusunod na depinisyon ay kinakailangan upang mailarawan ang reduksiyong beta.

Mga malayang bariabulo

Ang mga malayang bariabulo ng isang termino ang mga bariabulo na hindi binibigkis sa isang abstraksiyong lambda. Ang ibig sabihin nito, ang mga malayang bariabulo ng x ay tanging x; ang mga malayang bariabulo ng λx.t ang mga malayang bariabulo ng  t na ang x ay inalis at ang mga malayang bariabulo ng ts ang unyon ng mga malayang bariabulo ng t at s.
Halimbawa, ang terminong lambda na kumakatawan sa identidad na λx.x ay walang mga malayang bariabulo ngunit ang konstanteng punsiyon na  λx.y ay may isang malayang bariabulo na y.

Reduksiyong beta

Ang reduksiyong beta ay nagsasaad na ang ang aplikasyong may anyong (λx.t)s ay lumiliit sa t[x := s] (isinusulat ang (λx.t)s → t[x := s] bilang konbinyenteng maiklingkamay(shorthand) para sa “(λx.t)s ay lumiliit sa beta sat[x := s]”).
Halimbawa, sa bawat s meron tayong (λx.x)s → x[x := s] = s na nagpapakitang ang λx.x ang talagang identidad.
Gayundin, ang (λx.y)s → y[x := s] = y ay nagpapakitang ang λx.y ay talagang isang konstanteng punsiyon.
Ang kalkulong lambda ay maaaring maunawaan bilang ginawang ideyal na wika ng pagpoprogramang punsiyonal gaya ng Haskell o Pamantayang ML.
Sa ilalim ng pananaw na ito, ang reduksiyong beta ay tumutugon sa hakbang komputasyon at sa walang-tayp na kalkulong lambda na ipinapakita rito, ang reduksiyon ay hindi kailangang magwakas. 
Halimbawa, tingnan ang terminong (λx.xx)(λx.xx).
Dito, meron tayong (λx.xx)(λx.xx) → (xx)[x := λx.xx] = (x[x := λx.xx])(x[x := λx.xx]) = (λx.xx)(λx.xx).
Na ang ibig sabihin, ang termino ay lumiliit sa isang reduksiyong beta kaya ang reduksiyon ay hindi magwawakas.
Ang isa pang problem sa walang-tayp na kalkulong lambda ang kawalang kakayahan na makilala ang pagkakaiba sa pagitan ng iba't ibang uri ng data.
Halimbawa, maaari tayong magsulat ng punsiyon na tanging nagsasagawa ng operasyon sa mga bilang. Ngunit sa walang-tayp na kalkulong lambda, walang paraan upang maiwasan ang ating punsiyon na mailapat halimbawa sa mga katotohanang halaga(truth value) o mga tali(strings).
Ang may-tayp na kalkulong lambda na ay nagtatangkang alisin ang mga hindi nag-aasal na mga termino hangga't posible.

α-konbersiyon

Ang Alpha-konbersiyon na minsang kilala bilang alpha-renaming(alpha-muling pagpapangalan), ay pumapayag sa mga pangalan ng mga nakabigkis(bound) na bariabulo na mabago. Halimbawa, ang alpha-konbersiyon ng λx.x ay maaaring magbigay ng λy.y. Ang terminong tanging magkaiba sa alpha-konbersiyon ay tinatawag na  α-magkatumbas. Sa kalimitang mga gamit sa kalkulong lambda, ang mga terminong α-magkatumbas ay tinuturing na magkatumbas.
Ang tiyak na mga patakaran para sa alpha-konbersiyon ay hindi buong walang kahalagahan. Una, kung alpha-kinokonberte(binabago) ang isang abstraksiyon, ang tanging mga bariabulong makikita na muling pinangalanan ang mga nakabigkis sa parehong abstraksiyon. Halimbawa, ang alpha-konbersiyon ng  λx.λx.x ay maaaring magresulta ng λy.λx.x, ngunit hindi ito maaaring magresulta ng λy.λx.y.  Ang huli ay may ibang kahulugan sa orihinal.
Ikalawa, ang ang alpha-konbersiyon ay hindi posible kung ito ay magreresulta sa bariabulong mabibihag ng ibang abstraksiyon. Halimbawa, kung papalitan natin ang x ng y sa λx.λy.x, ating makukuha ang λy.λy.y, na hindi pareho.
Sa mga wikang pamprograma na may statikong(hindi nagbabagong) sakop, ang alpha-konbersiyon ay maaaring gamitin upang gawin ang resolusyon ng pangalan na mas simple sa pamamagitan ng pagsisiguro na walang pangalan ng bariabulo ang nagtatakip(ang bariabulong idineklara sa isang loob na sakop(scope) ay may parehong pangalan sa panlabas na sakop) ng pangalan sa naglalamang sakop(scope).

β-reduksiyon

Ang beta-reduksiyon ay bumibihag ng ideyang ng aplikasyon ng punsiyon. ang beta-reduksiyon ay inilalarawan sa mga termino ng substitusyon: ang beta-reduksiyon ng 
B ((λV.E) E′)  is E[V := E′].
Halimbawa, kung ipagpalagay ang ilang pagkakoda ng 2, 7, *, meron tayong sumusunod na mga β-reduksiyon: ((λn.n*2) 7) → 7*2.

η-konbersiyon

Ang eta-konbersiyon ay naghahayag ng ideya ng ekstensiyonalidad na sa kontekstong ito ay ang dalawang mga punsiyon ay pareho kung at tanging kung ang mga ito ay nagbibigay ng parehong resulta sa lahat ng mga argumento. Ang eta-konbersiyon ay nag-kokonberte sa pagitan ng λx.f x at f sa tuwing ang x ay hindi lumalabas na malaya sa f.

Mga anyong normal at konpluwensiya

Para sa walang-tayp ng kalkulong lambda, ang β-reduksiyon bilang patakarang muling pagsulat ay hindi malakas na nagnonormalisa ni mahinang nagnonormalisa.
Gayunpaman, ang parehong malakas na nagnonormalisang mga termino at mga mahinang nagnonormalisang mga termino ay may unikong(unique o walang katulad) na anyong normal. Para sa mga malakas na nagnonormalisang mga termino, ang anumang stratehiyang reduksiyon ay ginagarantiya na magbibigay ng anyong normal samantalang para sa mahinang nagnonormalisang mga termino, ang ilang stratehiyang reduksiyon ay maaaring mabigong mahanap ito.

Pagkokoda ng mga tayp(type) ng data

Ang basikong kalkulong lambda ay maaaring gamitin upang imodelo ang mga boolean, aritmetika, mga straktura ng data, at rekursiyon gaya ng ipinapakita sa mga sumusunod na pang-ilalim na seksiyon.