Lambda hesablaması üçün mənbəyə bax

'''Lambda hesablanması''' (''λ-hesablama'') — [[hesab]]lama anlayışını formalaşdırmaq və təhlil etmək üçün [[Amerika]] [[riyaziyyatçı]]sı [[Alonzo Çörç]] tərəfindən hazırlanmış rəsmi bir [[sistem]].

== Saf <math>\lambda</math>- hesablama ==
'''Saf <math>\lambda</math>- hesablaması'''şərtləri həmçinin , obyektləri ("obami")və ya Lambda ''(hərf-λ)'' şərtləri adlanan tətbiq və [[abstraksiya]] istifadə edərək yalnız dəyişənlərdən qurulmuşdur. Əvvəlcə hər hansı bir sabitliyin olması [[ehtimal]] edilmir.

== Tətbiq və abstraksiya ==
Əsasən '''λ-hesablama''' iki əsas əməliyyata əsaslanır:
* {{Anchor|Tətbiq}} ''Tətbiq'' ({{Dil-lat|applicatio}} — qoşma, qoşulmaq) müəyyən bir dəyərlə əlaqədar bir funksiyanı tətbiq etmək və ya çağırmaq deməkdir. Adətən onun işarəsi<math>f\ a</math>,hardaki, <math>f\ a</math> — funksiya, a isə <math>a</math> — arqumentdir.Bu riyaziyyatda ümumi olan <math>f(a)</math> notasiyaya uyğun gəlir,bəzən də həmçinin də istifadə olunur,lakin, λ-hesablama üçün <math>f</math>-in nəticəni verilən giriş dəyərindən hesablayan [[alqoritm]] kimi qəbul etməsi vacibdir. Bu mənada <math>f</math>,<math>a</math> tətbiqinə iki cür baxmaq olar: tətbiqi nəticəsində <math>f</math> -dan <math>a</math> -ya və yaxudda hesablama prosesi olaraq <math>f\ a</math>. Tətbiqin son şərhi ''β-azalma'' [[anlayış]]ı ilə əlaqədardır.
* {{Anchor|Abstraksiya}}''Abstraksiya'' və ya ''λ-abstraksiya'' ({{Dil-lat|abstractio}} — yayındırma,bölmə) öz növbəsində verilmiş ifadələrə uyğun olaraq funksiyalar qurur. Eynilə,əgər <math>t\equiv t[x]</math> — ifadəsi sərbəst olan <math>x</math>, onda qeyd <math>\ \lambda x.t[x]</math> bu mənanı verir: <math>\lambda</math> arqumentdən funksiyası <math>x</math>, formaya sahibdir <math>t[x]</math>,bir funksiyanı ifadə edir <math>x\mapsto t[x]</math>. Beləliklə, ''abstraksiya'' istifadə edərək yeni funksiyalar qura bilərsiniz. Tələb belə ki,<math>x</math> sərbəst şəkildə <math>t</math> -ya,daxil edilirsə, çox əhəmiyyətli deyil — fərz etmək kifayətdir<math>\lambda x.t\equiv t</math>,əgər bu belə deyilsə.

== α-ekvivalentlik ==
Lambda baxımından müəyyən edilən ekvivalentliyin əsas forması [[alfa]] ekvivalentliyidir. Məsələn, <math>\lambda x.x</math> və <math>\lambda y.y</math> : alfa ekvivalent lambda şərtləri və hər ikisi eyni funksiyanı [[təmsil]] edir: alfa ekvivalent lambda terminləri və hər ikisi eyni funksiyanı [[təmsil]] edir. Lambda [[abstraksiya]]sında olmadığı üçün <math>x</math> və <math>y</math> şərtləri alfa [[ekvivalent]]i deyildir.

== β-reduksiyası ==
<math>\lambda x. 2\cdot x + 1</math> ifadəsi bu funksiyanı ifadə edir,qəbulu hər birinə görə <math>x</math> dəyəri <math>2\cdot x + 1</math>, sonra ifadəni hesablamaq üçün <center><math>(\lambda x. 2\cdot x + 1)\ 3</math>,</center> həm tətbiqi, <math>x</math> dəyişən əvəzinə həm də mücərrədliyi ehtiva edən müddətdə 3 sayının dəyişdirilməsini yerinə <math>2\cdot x + 1</math> yetirmək lazımdır. Nəticədə <math>2\cdot 3+1=7</math> alınır. Bu mülahizə ümumi şəkildə <center><math>(\lambda x.t)\ a = t[x:=a],</math></center> yazılır və ''β-azalma'' adlanır. İfadənin növü {\displaystyle (\lambda x.t)\ a}(\lambda x.t)\ a-ya, yəni müəyyən bir müddətə bir [[abstraksiya]] tətbiq etmək, redex adlanır (redex). Baxmayaraq ki,sonra, o ''β-azalma'' lambda — hesablanmasının əslində çox əsaslı və mürəkkəb bir nəzəriyyəyə səbəb olan yeganə "əsas" [[aksiom]]adır{\displaystyle \lambda }\. Onunla birlikdə <math>\lambda</math>- hesablaması Tyurinq tamlıq xüsusiyyətinə malikdir və buna görə də ən sadə [[proqramlaşdırma]] dilidir.

== η-çevrilməsi ==
<math>\eta</math> — çevrilməsi iki funksiyanın eyni və yalnız olduqda eyni olduğunu düşüncəsini,nə zaman, hər hansı bir dəlil tətbiq olunanda eyni nəticələri ifadə edir. <math>\eta</math>- dönüşümü <math>\lambda x.f\ x</math> и <math>f</math> [[düstur]]larını bir-birinə çevirir(əgər ki,<math>x</math>-ın <math>f</math>-ya sərbəst girişi yoxdursa: əks halda sərbəst dəyişən <math>x</math> çevrilmədən sonra əlaqəli xarici [[abstraksiya]] və ya əksinə olacaq).

== Əyrilmə(Kurrinq) ==
İki dəyişənin funksiyası <math>x</math> и <math>y</math> <math>f(x,y) = x + y</math><math>x</math>-ın bir dəyişənin funksiyası hesab edilə bilər, bir dəyişən funksiyasını qaytaran<math>y</math>, yeni bir ifadə<math>\ \lambda x.\lambda y.x+y</math> olur. Bu texnika istənilən ariyanın funksiyaları üçün eyni şəkildə işləyir. Bu göstərir ki, bir çox dəyişənlərin funksiyaları <math>\lambda</math>— hesablaması ilə ifadə edilə bilər və "Sintaktik şəkər"dir. Bir çox dəyişkənliyin funksiyalarını bir dəyişənin funksiyasına çevirmək təsvir edilən [[proses]], [[Amerika]] [[riyaziyyatçı]]sı Haskell Kurrinin şərəfinə, ''karinq'' adlanır (M.E.Sheinfinkel (1924)).

== Tipsiz hesablama <math>\lambda</math>-semantikası ==
Bu bir faktdır ki,<math>\lambda</math>— lambda hesablamasının şərtləri funksiyaları kimi fəaliyyət göstərir,<math>\lambda</math>— şərtlərə tətbiq olunur(bu bəlkə də,özü-özünə),<math>\lambda</math>— hesablaması [[adekvat]] [[semantika]]nın qurulmasında çətinliklərə səbəb olur. <math>\lambda</math>— hesablanmasına hər hansı bir məna vermək üçün,<math>D</math> çoxluğunu almaq zəruridir,hansıki,onun [[funksional]] məkanına<math>D \to D</math> sərmayə qoyulacaqdı. Bunun ümumi vəziyyətində<math>D</math> <math>D</math> və <math>D</math>-dan <math>D</math>-yə qədər funksiyalarbu iki çoxluğun gücünün məhdudlaşdırılması səbəbindən mövcud deyildir: ikincisi birincisindən daha çox gücə malikdir.

Bu çətinliyi 1970-ci illərin əvvəllərində Dana Skott aradan qaldırdı,<math>D</math> bir [[domen]] anlayışını quraraq (əvvəlcə tam rəflərdə<ref>''Scott D.S.'' The lattice of flow diagrams.-- Lecture Notes in Mathematics, 188, Symposium on Semantics of Algorithmic Languages.-- Berlin, Heidelberg, New York: Springer-Verlag, 1971, pp. 311–372.</ref>,daha sonra tam bir qismən sifariş edilmiş xüsusi bir topologiya ilə ümumiləşdirərək) və kəsərək ''<math>D \to D</math>''davamlı olaraq bu funksiyasını yaratdı<ref>''Scott D.S.'' Lattice-theoretic models for various type-free calculi. — In: Proc. 4th Int. Congress for Logic, Methodology, and the Philosophy of Science, Bucharest, 1972.</ref>. Bu konstruksiyaların əsasında,bunların köməyi ilə [[proqramlaşdırma dilləri]]nin rekursion və məlumat növləri kimi [[iki]] vacib quruluşa dəqiq məna verə bilməsi üçün xüsusən [[proqramlaşdırma dilləri]]nin {{Tərcüməsiz 5|Denotasiya semantikası||en|Denotational semantics}} yaradıldı.

== Rekursiv funksiyalarla əlaqə ==
[[Rekursiya]] — özü vasitəsilə bir funksiyanın tərifidir; ilk baxışdan lambda hesablaması buna imkan vermir,lakin bu təəssürat yanıldır. Məsələn, [[faktorial]] hesablayan bir rekursiv funksiyasını nəzərdən keçirək:

: <tt>f(n) = 1, if n = 0; else n × f(n - 1).</tt>

Lambda hesablamasında bir funksiya birbaşa özünə [[istinad]] edə bilməz. Bununla birlikdə, bir funksiya funksiyaya ötürülə bilər. Bir qayda olaraq, bu [[mübahisə]] əvvəlcə gəlir.Bir funksiya ilə əlaqələndirərək yeni, onsuz da təkrarlanan bir funksiya əldə edirik. Bunun üçün özünə istinad edən bir dəlil (burada <math>r</math> olaraq təyin olunur),funksiya orqanına ötürülməlidir.

: <tt>g := λr. λn.(1, if n = 0; else n × (r r (n-1)))</tt>
: <tt>f := g g</tt>

Bu, [[faktorial]] hesablama problemini həll edir, lakin ümumi bir [[həll]] də mümkündür. Rekursiv bir funksiya və ya dövrü təmsil edən bir lambda müddəti alaraq, özünü ilk dəlil olaraq keçərək sabit nöqtəli kombinator lazımi rekursiv funksiyanı və ya dövrü geri qaytaracaqdır. Funksiyaların hər dəfə açıq şəkildə özlərini keçməsinə ehtiyac yoxdur.

[[Sabit]] nöqtəli kombinatorların bir neçə tərifi var. Onlardan ən sadəsi:

: <tt>Y = λg.(λx.g (x x)) (λx.g (x x))</tt><tt> lambda hesablamasında, <math>\operatorname{Y\ g}</math> — sabit nöqtə <math>\operatorname{g}</math>; bunu nümayiş etdirir:</tt>

:Y g</tt>
:(λ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).</tt> İndi [[faktorial]]ı müəyyən etmək üçün, rekursiv funksiyası olaraq sadəcə yaza bilərik<math>\operatorname{g\ (Y\ g)} n</math>,hardaki, <math>n</math> — nömrə hansıki [[faktorial]]ın hesablandlğı nömrədir. <math>n = 4</math> -dən,əldə edirik:

g (Y g) 4
    (λfn.(1, if n = 0; and n·(f(n-1)), if n>0)) (Y g) 4
    (λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0)) 4
    1, if 4 = 0; and 4·(g(Y g) (4-1)), if 4>0
    4·(g(Y g) 3)
    4·(λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 3)
    4·(1, if 3 = 0; and 3·(g(Y g) (3-1)), if 3>0)
    4·(3·(g(Y g) 2))
    4·(3·(λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 2))
    4·(3·(1, if 2 = 0; and 2·(g(Y g) (2-1)), if 2>0))
    4·(3·(2·(g(Y g) 1)))
    4·(3·(2·(λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 1)))
    4·(3·(2·(1, if 1 = 0; and 1·((Y g) (1-1)), if 1>0)))
    4·(3·(2·(1·((Y g) 0))))
    4·(3·(2·(1·((λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 0))))
    4·(3·(2·(1·(1, if 0 = 0; and 0·((Y g) (0-1)), if 0>0))))
    4·(3·(2·(1·(1))))
    24

Bir rekursiv funksiyanın hər tərifi müvafiq funksiyanın sabit bir nöqtəsi kimi göstərilə bilər, buna görə də <math>\operatorname{Y}</math> istufadə edilərək,hər rekursiv tərif lambda ifadəsi kimi ifadə edilə bilər. Xüsusilə, toplama işlənməsini, [[vurma]], [[natural ədədlər]]in müqayisəsini rekursiv olaraq təyin edə bilərik.

== Proqramlaşdırma dillərində ==
Proqramlaşdırma dillərində "<math>\lambda</math>-hesablaması" tez-tez " anonim funksiyaların" mexanizmi başa düşülür — callback funksiyaları,hansı ki,istifadə edildikləri yerlərdə və cari funksiyanın (dəyişmə) lokal dəyişənlərinə giriş imkanı olan yerlərdə müəyyən edilə bilər.

== İstinadlar ==
{{İstinad siyahısı}}

== Ədəbiyyat ==
{{Kitab3 |автор=Барендрегт X |заглавие=Ламбда-исчисление. Его синтаксис и семантика |место=M. |издательство=Мир |год=1985|страница=606&nbsp;}}

== Həmçinin bax ==
* [[Lambda-CDM model]]
* [[Standart Model]]
* [[Lambda-zond]]

== Xarici keçidlər ==
* [https://turing100.acm.org/lambda_calculus_timeline.pdf λ-Hesablama: Sonra & İndi]{{ref-en}}
* [https://www.encyclopediaofmath.org/index.php/Lambda-calculus Lambda hesablaması]{{ref-en}}
* [http://www.cs.bham.ac.uk/~axj/pub/papers/lambda-calculus.pdf Lambda Hesablamasına qısa bir giriş]{{ref-en}}
* [https://www.dropbox.com/s/i0qgfoye6artcp8/untyped_lambda.pdf?dl=0 Lambda hesablaması — addımbaaddım]{{ref-en}}
{{Vikianbar kateqoriyası|Lambda hesablaması}}
{{Xarici istinadlar}}

[[Kateqoriya:Alqoritmlər nəzəriyyəsi]]