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.

Inpormal na deskripsiyon

Motibasyon

Tignan ang sumusunod na dalawang halimbawa: Ang punsiyong identidad na

I(x) = x

ay kumukuha ng isang input na x at agad na nagbabalik ng x (i.e. ang identidad ay walang ginagawa sa input nito) samantalang ang punsiyong

sqsum(x, y) = x*x + y*y

ay kumukuha ng pares ng mga input na x at y at nagbabalik ng suma ng mga kwadrado na x*x + y*y. Gamit ang dalawang mga halimbawang ito, maaari tayong makagawa ng magagamit na mga obserbasyon na nag-uudyok sa mga ideya ng kalkulong lambda.

Ang unang obserbasyon ay ang mga punsiyon ay hindi kinakailangang hayagang pinapangalanan. Ang ibig sabihin nito, ang punsiyong

sqsum(x, y) = x*x + y*y

ay maaaring muling isulat sa anyong anonimo bilang

(x, y) ↦ x*x + y*y

(na binabasa bilang "ang pares na x at y at minamapa sa x*x + y*y”). Sa katulad na paraan, ang

I(x) = x

ay maaaring muling isulat sa anyong anonimo bilang x ↦ x kung saan ang input ay simpleng minamapa sa sarili nito.

Ang ikalawang obserbasyon ay ang spesipikong pagpipilian ng pangalan para sa mga argumento ng punsiyon ay hindi mahalaga. Ang ibig sabihin ay

x ↦ x at

y ↦ y

ay naghahayag ng parehong punsiyon: ang identidad. Gayundin, ang

(x, y) ↦ x*x + y*y at

(u, v) ↦ u*u + v*v

ay naghahayag rin ng parehong punsiyon

Sa huli, ang anumang punsiyon na nangangailangan ng dalawang input halimbawa, ang nabanggit na punsiyong sqsum ay maaaring muling ayusin sa isang katumbas ng punsiyon na tumatanggap ng isang input at sa output ay nagbabalik ng isa pang punsiyon na tumatanggap naman ng isang input. Halimbawa,

(x, y) ↦ x*x + y*y

ay maaaring muling isaayos sa

x ↦ (y ↦ x*x + y*y)

Ang transpormasyong ito ay tinatawag na currying at maaaring lahatin sa mga punsiyon na tumatanggap ng arbitraryong bilang ng mga argumento.

Ang currying ay intwitibong mauunawan sa pamamagitan ng paggamit ng halimbawa. Ikumpara ang punsiyon na

(x, y) ↦ x*x + y*y

sa anyong curried nito na

x ↦ (y ↦ x*x + y*y)

Sa ibinigay na dalawang argumento, meron tayong:

((x, y) ↦ x*x + y*y)(5, 2)

= 5*5 + 2*2 = 29

Ngunit kung gagamitin ang currying, meron tayong:

((x ↦ (y ↦ x*x + y*y))(5))(2)

= (y ↦ 5*5 + y*y)(2)

= 5*5 + 2*2 = 29

makikita nating ang anyong hindi-curried at curried ay kumukwenta ng parehong resulta. Pansinin na ang x*x ay naging konstante.

Mga terminong lambda

Ang sintaks ng mga terminong lambda ay partikular na simple. May tatlong mga paraan upang makamit ang mga ito:

ang isang terminong lambda ay maaaring maging bariabulong x;
kung ang t ang terminong lambda at ang x ang bariabulo, kung gayon ang λx.t ang terminong lambda(na tinataag na abstraksiyong lambda);
kung ang t at s ang mga terminong lambda, kung gayon ang ts ang terminong lambda na tinatawag na aplikasyon.

Wala ng iba pa ang terminong lambda, bagaman ang pagba-braket ay maaaring gamitin upang linawin ang mga termino.

Sa intwitibong paglalarawan, ang isang abstraksiyong lambda na λx.t ay kumakatawan sa isang punsiyong anonimo na kumukuha ng isang input at ang λ ay sinasabing nagbibigkis(bind) ng x sa t at ang aplikasyong ts ay kumakatawan sa aplikasyon ng input na s sa isang punsiyongt. Sa kalkulong lambda, ang mga punsiyon ay inuunawang mga unang-klaseng halaga upang ang mga punsiyon ay magamit na input sa ibang mga punsiyon at ang mga punsiyon ay magbalik ng mga punsiyon bilang mga output nito.

Halimbawa, ang λx.x ay kumakatawan sa punsiyong identidad na x ↦ x at ang (λx.x)y ay kumakatawan sa punsiyong identidad na nilalapat sa y. Sa karagdagan, ang (λx.y) ay kumakatawan sa punsiyong konstante na x ↦ y na punsiyong palaging nagbabalik ng y kahit ano pa ang input. Dapat pansinin na ang punsiyong aplikasyon ay asosiyatibo sa kaliwa upang ang (λx.x)y z = ((λx.x)y)z.

Ang mga terminong lambda sa kanilang sarili ay hindi partikular na interasante. Ang gumagawa sa kanilang interasante ang iba't ibang mga nosyon ng 'pagkakatumbas(equivalence at reduksiyon(pagpapaliit) na mailalarawa sa mga ito.

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.

Umiiwas sa pagkakabihag na mga substitusyon

Kung gagamitin ang depinisyon ng mga malayang bariabulo, maaari na nating ilarawan ang umiiwas sa pagkakabihag na substitusyon. Ipagpalagay na ang t, s at r ang mga terminong lambda at ang x at y ang mga bariabulo.

Isusulat natin ang t[x := r] para sa substitusyon ng r para sa x sa t sa paraang umiiwas sa pagkakabihag.

x[x := r] = r;
y[x := r] = y if x ≠ y;
(ts)[x := r] = (t[x := r])(s[x := r]);
(λx.t)[x := r] = λx.t;
(λy.t)[x := r] = λy.(t[x := r]) kung x ≠ y at ang y ay wala sa mga malayang bariabulo ng r (na minsang sinasbi na ang "y ay sariwa para sar").

Halimbawa, ang (λx.x)[y := y] = λx.(x[y := y]) = λx.x, and ((λx.y)x)[x := y] = ((λx.y)[x := y])(x[x := y]) = (λx.y)y.

Ang kondisyon ng pagiging sariwa(na nag-aatas na ang y ay wala sa mga malayang bariabulo ng r) ay mahalaga upang masigurado na ang substitusyon ay hindi nagpapabago ng kahulugan ng mga punsiyon.

Halimbawa, ipagpalagay na naglalarawan tayo ng isa pang aksiyong substitusyon na walang kondisyon ng pagiging sariwa. Kung gayon, ang (λx.y)[y := x] = λx.(y[y := x]) = λx.x at ang konstanteng punsiyon na λx.y ay nagiging identidad na λx.x sa pamamagitan ng substitusyon.

Kung ang kondisyon ng pagiging sariwa ay hindi matatagpo, kung gayon maaaring simpleng muling pangalan ang alpha ng isang angkop na sariwang bariabulo. Halimbawa, kung babalik tayo sa ating tamang nosyon ng substitusyon sa (λx.y)[y := x], ang abstraksiyong lambda ay maaaring muling pangalanan ng isang sariwang bariabulong z upang makamit ang (λz.y)[y := x] = λz.(y[y := x]) = λz.x at ang kahulugan ng punsiyon ay naiingatan ng substitusyon.

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.

Pormal na depinisyon

Depinisyon

Ang mga ekspresyong lambda ay binubuo ng

mga bariabulong v₁, v₂, ..., v_n, ...

mga simbolo ng abstraksiyon na λ at .

mga parentesis ( )

Ang mga hanay ng ekspresyong lambda na Λ ay maaaring ilarawan na

Kung ang x ang bariabulo, kung gayong ang x ∈ Λ
Kung ang x ang bariabulo at ang M ∈ Λ, kung gayon ang (λx.M) ∈ Λ
Kung ang M, N ∈ Λ, kung gayon ang (M N) ∈ Λ

Ang mga instansiya ng patakarang 2 ay kilala bilang mga abstraksiyon at ang mga instansiya ng patakarang 3 ay kilala bilang mga aplikasyon.^[1]

Notasyon

Upang maiwasan ang notasyon ng mga ekspresyong lambda na maging magulo, ang sumusunod na mga kumbensiyon ay karaniwang nilalapat.

Ang pinakalabas na mga parentesis ay inaalis: M N imbis na (M N).
Ang mga aplikasyon ay pinagpapalagay na asosiyatibo sa kaliwa: Ang M N P ay maaaring isulat imbis na ((M N) P).^[2]
Ang katawan ng abstraksiyon ay lumalawig sa pinaka-kanan hanggang posible: ang λx.M N ay nangangahulugang λx.(M N) at hindi (λx.M) N.
Ang sekwensiya ng mga abstraksiyon ay pinaliit: ang λx.λy.λz.N ay pinaliit bilang λxyz.N.^[3]^[4]

Malaya at nakabigkis na mga bariabulo

Ang operador ng abstraksiyon na λ ay sinasabing nagbibigkis ng bariabulo saan man ito makita sa katawan ng abstraksiyon. Ang mga bariabulong nahuhulog sa loob ng sakop ng lamba ay sinasabing nakabigkis(bound). Ang ibang mga bariabulo ay tinatawag na malaya. Halimbawa sa sumusunod na ekpresyon, ang y ay isang nakabigkis na bariabulo at ang x ay malaya: λy.x x y. Tandaan din na angbariabulo ay nagbibigkis sa "pinakamalapit" nitong lambda. Sa sumusunod na mga ekspresyon, ang isang makikitang x ay nakabigkis sa ikalawang lambda: λx.y (λx.z x)

Ang hanay ng mga malalayang bariabulo ng ekspresyong lambda na M ay tinutukoy bilang FV(M) at inilalarawan sa pamamagitan ng rekursiyon sa straktura ng mga termino gaya ng sumusunod:

FV(x) = {x}, kung saan ang x ay isang bariabulo
FV(λx.M) = FV(M) \ {x}
FV(M N) = FV(M) ∪ FV(N)^[5]

Ang isang ekspresyong hindi naglalaman ng malayang mga bariabulo ay sinasabing sarado. Ang saradong mga ekspresyong lambda ay kilala rin bilang mga kombinador(combinator) at katumbas ng mga termino sa kombinatoryong lohika.

Reduksiyon

Ang kahulugan ng mga ekspresyong lambda ay inilalarawan kung paanong ang mga ekspresyon ay mapapaliit.^[6]

May tatlong uri ng reduksiyon(pagpapaliit):

α-konbersiyon: pagbabago ng mga nakagbigkis na bariabulo;
β-reduksiyon: paglalapat ng mga punsiyon sa mga argumento nito;
η-konbersiyon: na bumibihag ng nosyon ng ekstensiyonalidad;

Ating sasalitain ang mga nagresultang mga pagkakatumbas: ang dalawang mga ekspresyon ay β-magkatumbas kung ang mga ito ay ma-β-konberte(baguhin) sa parehong ekspresyon at ang α/η-pagkakatumbas ay inilalarawan ng pareho.

Ang terminong redex, na pinaikling reducible expression(mapapaliit na ekspresyon), ay tumutukoy sa pang-ilalim na mga termino(subterms) na maaaring mapaliit sa pamamagitan ng isa sa mga patakarang reduksiyon. Halimbawa, ang (λx.M) N ay isang beta-redex; kung ang x ay hindi malaya sa M, ang λx.M x ay isang eta-redex. Ang ekspresyon kung saan ang redex ay lumiliit ay tinatawag na reduct nito. Kung gagamitin ang nakaraang halimbawa, ang mga reduct ng mga ekspresyong ito ay M[x:=N] at M.

α-konbersiyon

Ang Alpha-konbersiyon na minsang kilala bilang alpha-renaming(alpha-muling pagpapangalan),^[7] 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).

Substitusyon

Ang substitusyon na isinusulat na E[V := E′] ang proseso ng pagpapalit ng lahat ng malayang instansiya ng bariabulong V sa pamamagitan ng ekspresyong E′. Ang substitusyon sa mga termino ng λ-kalkulo ay inilalarawan ng rekursiyon sa straktura ng mga termino gaya ng sumusunod:

x[x := N] ≡ N

y[x := N] ≡ y, if x ≠ y

(M₁ M₂)[x := N] ≡ (M₁[x := N]) (M₂[x := N])

(λx.M)[x := N] ≡ λx.(M)

(λy.M)[x := N] ≡ λy.(M[x := N]), if x ≠ y, sa kondisyong y ∉ FV(N)

Upang maghalili sa isang abstaksiyong lambda, minsan ay kinakailangang i-α-konberte ang ekspresyon. Halimbawa, hindi tama para sa (λx.y)[y := x] na magresulta sa (λx.x) dahil ang hinaliling x ay dapat malaya ngunit naging nabigkis(bound). Ang tamang substitusyon sa kasong ito ay (λz.x) hanggang sa α-pagkakatumbas. Pansinin na ang substitusyon at inilalarawan ng walang kagaya hanggang sa α-pagkakatumbas.

β-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.

Aritmetika sa kalkulong kalkulo

Mayroong ilang mga posibleng paraan upang ilarawan ang natural na bilang sa kalkulong lambda, ngunit sa kasalukuyan ang pinakakaraniwan ang mga numeral ni Church na maaaring ilarawan sa mga sumusunod:

0 := λf.λx.x

1 := λf.λx.f x

2 := λf.λx.f (f x)

3 := λf.λx.f (f (f x))

at tuloy tuloy pa. O kung gagamitin ang alternatibong sintaks na pinakita sa itaas na notasyon:

0 := λfx.x

1 := λfx.f x

2 := λfx.f (f x)

3 := λfx.f (f (f x))

Ang isang numeral na Church ay isang mataas na antas na punsiyon—ito ay kumukuha ng isang-argumentong punsiyong f at nagbabalik ng isang-argumentong punsiyong. Ang numeral na Church na n ay isang punsiyon na kumukuha ng na f bilang argumento at nagbabalik ng ika-n na komposisyon ng f, i.e. ang punsiyong f ay binubuo ng sarili nito ng n beses. Ito ay tinutukoy ng f⁽ⁿ⁾ at sa katunayan ay ang ikan kapangyarihan ng f (na tinuturing bilang operador); Ang f⁽⁰⁾ ay inilalarawan bilang punsiyong identidad. Ang mga gayong paulit ulit na komposisyon(ng isang punsiyong f) ay sumusunod sa mga batas ng eksponente kaya ang numeral na ito ay maaaring gamitin para sa aritmetika. (Sa orihinal na kalkulong lambda ni Church, ang pormal na paremetro ng isang ekspresyong lambda ay inaaatasan makita ng kahit isang beses sa katawan ng punsiyon na gumawa sa taas na depinisyon ng 0 na imposible.)

Tayo ay maglalarawan ng kahaliling punsiyon na kumukuha ng bilang na n at nagbabalik ng n + 1 sa pamamagitan ng pagdaragdag ng karagdagang aplikasyon ng f:

SUCC := λnfx.f (n f x)

Dahil ang ika-m komposisyon ng f na binubuo ng ika=n komposisyon ng f ay nagbibigay ng ika-m+n komposisyon ng f, ang adisyon ay maaaring ilarawan ng sumusunod:

PLUS := λmnfx.m f (n f x)

PLUS ay maaaring unawain bilang punsiyong kumukuha ng dalawang natural na bilang bilang mga argumento at nagbabalik ng isang natural na bilang; maaaring mapatunayan na ang

PLUS 2 3 at

5

ay magkatumbas ng mga ekspresyong lambda. Dahil sa pagdaragdag ng m sa bilang na n ay maisasagawa sa pamamagitan ng pagdadagdag ng 1 na m beses, ang isang katumbas na depinsiyon ay:

PLUS := λmn.m SUCC n^[8]

Gayundin, ang multiplikasyon ay maaaring ilarawan bilang

MULT := λmnf.m (n f)^[9]

Sa alternatibong paraan ang

MULT := λmn.m (PLUS n) 0

dahil ang pagpaparami ng m at n ay kapareho ng paguulit ng pagdaragdag na n punsiyon na m beses at pagkatapos ay paglalapat nito sa sero.

Ang eksponensiyasiyon ay may simpleng paglalarawan sa mga numeral na Church na

POW := λbe.e b

Ang pangunang punsiyong inilalarawan ng PRED n = n - 1 para sa positibong intedyer na n and PRED 0 = 0 ay itinuturing na mas mahirap. Ang pormulang

PRED := λnfx.n (λgh.h (g f)) (λu.x) (λu.u)

ay maaaring mapatunayan sa pamamagitan sa paaraang induksiyon na kung ang T ay tumutukoy sa (λgh.h (g f)), kung gayon, ang T⁽ⁿ⁾(λu.x) = (λh.h(f^(n-1)(x))) for n > 0. Ang dalawang iba pang mga depinisyon ng PRED ay ibinibigay sa ibaba. Ang isa gamit ang mga kondisyonal at isa gamit ang mga pares. Sa paggamit ng pangunang punsiyon, ang substraksiyon ay diretso. Kung ilalaare given below, one using conditionals and the other using pairs. With the predecessor function, subtraction is straightforward. Kung ilalarawan ang

SUB := λmn.n PRED m,

Ang SUB m n ay nagbibigay na m - n kung ang m > n at 0 kung hindi.

Lohika at predikato

Sa konserbasyon, ang mga sumusunod na depinisyon(na kilala bilang mga boolean na Church) ay ginagamit para sa mga halagang boolean na TRUE and FALSE:

TRUE := λxy.x

FALSE := λxy.y

(Tandaan na ang FALSE ay katumbas ng numeral na Church na sero na inilalarawan sa itaas)

Ngayon, gamit ang dalawang mga λ-termino, maaari nating ilarawan ang ilang operador na lohika (ang mga ito ay pawang mga posibleng pormula; ang ibang mga ekspresyon ay parehong tama):

AND := λpq.p q p

OR := λpq.p p q

NOT := λpab.p b a

IFTHENELSE := λpab.p a b

Ngayon, makukwenta na nating ang ilang punsiyong lohika halimbawa ang:

AND TRUE FALSE

≡ (λpq.p q p) TRUE FALSE →_β TRUE FALSE TRUE

≡ (λxy.x) FALSE TRUE →_β FALSE

at makikita nating ang AND TRUE FALSE ay katumbas ng FALSE.

Ang isang predikato(predicate) ay isang punsiyon na nagbabalik ng isang halagang boolean. Ang pinaka pundamental na predikato ang ISZERO na nagbabalik ng TRUE kung ang argumento nito ay ang numeral na Church na0, at FALSE kung ang argumento nito ay iba pang numeral na Church:

ISZERO := λn.n (λx.FALSE) TRUE

Ang sumusunod na predikato ay sumusubok(test) kung ang unang argumento ay mas-maliit o katumbas ng ikalawa:

LEQ := λmn.ISZERO (SUB m n),

At dahil ang m = n, kung ang LEQ m n at LEQ n m, tuwid na malilikha ang predikato para sa numerikal na pagtutumbas.

Ang pag-iral ng mga magagamit ng mga predikato at ang nasa taas na depinisyon ng TRUE and FALSE ay gumagawa nito na konbinyenteng maisulat ang mga ekspresyong "if-then-else" sa kalkulong lambda.

PRED := λn.n (λgk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) 0

na maaaring mapatunayan sa pamamagitan ng induksiyon na ang n (λgk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) ang dagdag n - 1 punsiyon para sa n > 0.

Mga pares

Ang isang pares(2-tuple) ay maaaring ilarawan sa mga termino ng TRUE at FALSE sa pamamagitan ng pagkokodang Church para sa mga pares. Halimbawa, ang PAIR ay bumabalot sa pares na (x,y); ang FIRST ay nagbabalik ng unang elemento ng pares at ang SECOND ay nagbabalik ng ikalawang elemento.

PAIR := λxyf.f x y

FIRST := λp.p TRUE

SECOND := λp.p FALSE

NIL := λx.TRUE

NULL := λp.p (λxy.FALSE)

Ang listahang pinagdugtong(linked list) ay maaaring ilarawa na NIL para sa walang lamang na listahan o ng PAIR ng elemento at isang mas maliit na listahan. Ang predikatong NULL ay sumusubok para sa halagang NIL. (Sa alternatibong paglalarawan gamit ang NIL := FALSE ang konstruktong l (λhtz.deal_with_head_h_and_tail_t) (deal_with_nil) ay nag-aalis ng pangangailangan para sa isang hayagang pagsubok na NULL).

Bilang halimbawa ng paggamit ng mga pares, ang punsiyong lipat-at-dagdag(shift-and-increment) na nagmamapa ng (m, n) sa (n, n + 1) ay maaaring ilarawan bilang

Φ := λx.PAIR (SECOND x) (SUCC (SECOND x))

na nagpapayag sa atin na magbigay ng marahil na pinakamalinaw na bersiyon ng pangunang punsiyon:

PRED := λn.FIRST (n Φ (PAIR 0 0)).

Rekursiyon at mga nakapirmeng punto

Ang rekursiyon ang depinisyon ng punsiyon na gamit ang mismong punsiyon. Kung titingnan sa hitsura nito, ang kalkulong lambda ay mukhang hindi pumapayag nito. Ngunit ang impresyong ito ay nakakapagligaw. Ituring na halimbawa ang punsiyong paktoryal na f(n) na rekursibong inilalarawan ng

f(n) = 1, if n = 0; else n × f(n - 1).

Sa kalkulong lambda, ang isang punsiyon ay hindi maaaring direktang tumukoy sa sarili nito. Gayunpaman, ang punsiyon ay maaaring tumanggap ng paremetro na ipinagpapalagay na sarili nito. Bilang inbarianto(hindi nagbabago), ang argumentong ito ay karaniwang una. Kung ibibigkis(binding) ito sa punsiyon, ito ay nagbibigay ng bagong punsiyon na maaaring magsagawa ng rekursiyon. Upang makamit ang rekursiyon, ang argumentong nagrereperensiya sa sarili(na tinatawag na r dito) ay dapat palaging ipinapasa sa sarili nito sa loob ng katawan ng punsiyon.

g := λr. λn.(1, if n = 0; else n × (r r (n-1)))

f := g g

Ito ay lumulutas ng spesipikong problema ng punsiyong paktoryal ngunit ang isang henerikong solusyon ay posible rin. Kung binigyan ng terminong lambda na kumakatawan sa katawan ng punsiyong rekursibo o ikot(loop), kung kukunin ang sarili nito bilang unang argumento, ang operador na nakapirmeng-punto ay magbabalik ng ninanais na punsiyong rekursibo o loop. Ang punsiyon ay hindi kailangang hayagan na ipasa sa sarili nito sa anumang punto. Ang katunayan, maraming mga posibleng depinisyon para sa operador na na tinuturing na tayp(uri) ng nga kombinador na nakapirmeng-punto. Ang pinakasimple ay inilalarawan bilang:

Y = λg.(λx.g (x x)) (λx.g (x x))

Sa kalkulong lambda, ang Y g ay isang nakapirmeng-punto ng g habang lumalawig ito sa:

Y g

λh.((λx.h (x x)) (λx.h (x x))) g

(λx.g (x x)) (λx.g (x x))

g ((λx.g (x x)) (λx.g (x x)))

g (Y g).

Ngayon, upang kompletuhin ang ating pagtawag na rekursibo sa punsiyong paktoryal, ating tatawagin ang g (Y g) n, kung saan ang n ang bilang na kinukwenta natin ang paktoryal nito. Halimbawa, sa ibinigay na n = 4, ito ay nagbibigay ng:

g (Y g) 4

(λfn.(1, kung ang n = 0; at n·(f(n-1)), kung ang n > 0)) (Y g) 4

(λn.(1, kung ang n = 0; at n·((Y g) (n-1)), kung ang n > 0)) 4

1, kung ang 4 = 0; at 4·(g(Y g) (4-1)), kung ang 4 > 0

4·(g(Y g) 3)

4·(λn.(1, kung ang n = 0; at n·((Y g) (n-1)), kung ang n > 0) 3)

4·(1, kung ang 3 = 0; at 3·(g(Y g) (3-1)), kung ang 3 > 0)

4·(3·(g(Y g) 2))

4·(3·(λn.(1, kung ang n = 0; at n·((Y g) (n-1)), kung ang n > 0) 2))

4·(3·(1, if 2 = 0; and 2·(g(Y g) (2-1)), kung ang 2 > 0))

4·(3·(2·(g(Y g) 1)))

4·(3·(2·(λn.(1, kung ang n = 0; at n·((Y g) (n-1)), kung ang n > 0) 1)))

4·(3·(2·(1, kung ang 1 = 0; at 1·((Y g) (1-1)), kung ang 1 > 0)))

4·(3·(2·(1·((Y g) 0))))

4·(3·(2·(1·((λn.(1, kung ang n = 0; at n·((Y g) (n-1)), kung ang n > 0) 0))))

4·(3·(2·(1·(1, kung ang 0 = 0; at 0·((Y g) (0-1)), kung ang 0 > 0))))

4·(3·(2·(1·(1))))

24

Ang bawat rekursibong inilalarawan na punsiyon ay maaaring maunawaan bilang isang nakapirmeng punto ng ilang mga iba pang mga angkop ng punsiyon kaya kung gagamitin ang Y, ang bawat rekursibong inilalarawan na punsiyon ay maaaring ihayag bilang isang ekspresyong lambda. Sa partikular, maaari na nating malinis na ilarawan ang subtraksiyon, multiplikasyon, at pagkukumpara na predikator ng mga natural na bilang sa paraang rekursibo.

Mga pamantayang termino

Ang ilang mga termino ay may karaniwang tinatanggap na mga pangalan:

I := λx.x

K := λxy.x

S := λxyz.(x z (y z))

ω := λx.(x x)

Ω := ω ω

Sanggunian

↑ Barendregt, Hendrik Pieter (1984), The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, bol. 103 (ika-Revised (na) edisyon), North Holland, Amsterdam. Corrections, ISBN 0-444-87508-5 {{citation}}: External link in |publisher= (tulong)CS1 maint: date auto-translated (link)
↑ Example for Rules of Associativity
↑ Selinger, Peter, Lecture Notes on the Lambda Calculus (PDF), Department of Mathematics and Statistics, University of Ottawa, p. 9
↑ Example for Rule of Associativity
↑ Barendregt, Henk; Barendsen, Erik (Marso 2000), Introduction to Lambda Calculus (PDF){{citation}}: CS1 maint: date auto-translated (link)^{[patay na link]}
↑ de Queiroz, Ruy J.G.B. "A Proof-Theoretic Account of Programming and the Role of Reduction Rules." Dialectica 42(4), pages 265-282, 1988.
↑ Turbak, Franklyn; Gifford, David (2008), Design concepts in programming languages, MIT press, p. 251, ISBN 9780262201759{{citation}}: CS1 maint: date auto-translated (link)
↑ Felleisen, Matthias; Flatt, Matthew (2006), Programming Languages and Lambda Calculi (PDF), p. 26{{citation}}: CS1 maint: date auto-translated (link)
↑ Selinger, Peter, Lecture Notes on the Lambda Calculus (PDF), Department of Mathematics and Statistics, University of Ottawa, p. 16

[1] Barendregt, Hendrik Pieter (1984), The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, bol. 103 (ika-Revised (na) edisyon), North Holland, Amsterdam. Corrections, ISBN 0-444-87508-5 {{citation}}: External link in |publisher= (tulong)CS1 maint: date auto-translated (link)

[2] Example for Rules of Associativity

[Selinger-3] Selinger, Peter, Lecture Notes on the Lambda Calculus (PDF), Department of Mathematics and Statistics, University of Ottawa, p. 9

[4] Example for Rule of Associativity

[BarendregtBarendsen-5] Barendregt, Henk; Barendsen, Erik (Marso 2000), Introduction to Lambda Calculus (PDF){{citation}}: CS1 maint: date auto-translated (link)^{[patay na link]}

[6] Queiroz, Ruy J.G.B. "A Proof-Theoretic Account of Programming and the Role of Reduction Rules." Dialectica 42(4), pages 265-282, 1988.

[7] Turbak, Franklyn; Gifford, David (2008), Design concepts in programming languages, MIT press, p. 251, ISBN 9780262201759{{citation}}: CS1 maint: date auto-translated (link)

[8] Felleisen, Matthias; Flatt, Matthew (2006), Programming Languages and Lambda Calculi (PDF), p. 26{{citation}}: CS1 maint: date auto-translated (link)

[9] Selinger, Peter, Lecture Notes on the Lambda Calculus (PDF), Department of Mathematics and Statistics, University of Ottawa, p. 16

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]