Lambda hesablaması

Lambda hesablanması (λ-hesablama) — hesablama 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 $\lambda$ - hesablama

Saf $\lambda$ - 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:

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

α-ekvivalentlik

Lambda baxımından müəyyən edilən ekvivalentliyin əsas forması alfa ekvivalentliyidir. Məsələn, $\lambda x.x$ və $\lambda y.y$ : 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 abstraksiyasında olmadığı üçün $x$ və $y$ şərtləri alfa ekvivalenti deyildir.

β-reduksiyası

$\lambda x.2\cdot x+1$ ifadəsi bu funksiyanı ifadə edir,qəbulu hər birinə görə $x$ dəyəri $2\cdot x+1$ , sonra ifadəni hesablamaq üçün

(\lambda x.2\cdot x+1)\ 3

,

həm tətbiqi, $x$ 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ə $2\cdot x+1$ yetirmək lazımdır. Nəticədə $2\cdot 3+1=7$ alınır. Bu mülahizə ümumi şəkildə

(\lambda x.t)\ a=t[x:=a],

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" aksiomadır{\displaystyle \lambda }\. Onunla birlikdə $\lambda$ - hesablaması Tyurinq tamlıq xüsusiyyətinə malikdir və buna görə də ən sadə proqramlaşdırma dilidir.

η-çevrilməsi

$\eta$ — ç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. $\eta$ - dönüşümü $\lambda x.f\ x$ и $f$ düsturlarını bir-birinə çevirir(əgər ki, $x$ -ın $f$ -ya sərbəst girişi yoxdursa: əks halda sərbəst dəyişən $x$ çevrilmədən sonra əlaqəli xarici abstraksiya və ya əksinə olacaq).

Əyrilmə(Kurrinq)

İki dəyişənin funksiyası $x$ и $y$ $f(x,y)=x+y$ $x$ -ın bir dəyişənin funksiyası hesab edilə bilər, bir dəyişən funksiyasını qaytaran $y$ , yeni bir ifadə $\ \lambda x.\lambda y.x+y$ 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ı $\lambda$ — 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 $\lambda$ -semantikası

Bu bir faktdır ki, $\lambda$ — lambda hesablamasının şərtləri funksiyaları kimi fəaliyyət göstərir, $\lambda$ — şərtlərə tətbiq olunur(bu bəlkə də,özü-özünə), $\lambda$ — hesablaması adekvat semantikanın qurulmasında çətinliklərə səbəb olur. $\lambda$ — hesablanmasına hər hansı bir məna vermək üçün, $D$ çoxluğunu almaq zəruridir,hansıki,onun funksional məkanına $D\to D$ sərmayə qoyulacaqdı. Bunun ümumi vəziyyətində $D$ $D$ və $D$ -dan $D$ -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ı, $D$ bir domen anlayışını quraraq (əvvəlcə tam rəflərdə^[1],daha sonra tam bir qismən sifariş edilmiş xüsusi bir topologiya ilə ümumiləşdirərək) və kəsərək $D\to D$ davamlı olaraq bu funksiyasını yaratdı^[2]. Bu konstruksiyaların əsasında,bunların köməyi ilə proqramlaşdırma dillərinin 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ərinin Denotasiya semantikası^[ing.] 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:

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

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 $r$ olaraq təyin olunur),funksiya orqanına ötürülməlidir.

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

f := g g

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:

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

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). İndi faktorialı müəyyən etmək üçün, rekursiv funksiyası olaraq sadəcə yaza bilərik

\operatorname {g\ (Y\ g)} n

,hardaki,

n

— nömrə hansıki faktorialın hesablandlğı nömrədir.

n=4

-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ə $\operatorname {Y}$ 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ərin müqayisəsini rekursiv olaraq təyin edə bilərik.

Proqramlaşdırma dillərində

Proqramlaşdırma dillərində " $\lambda$ -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

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

Ədəbiyyat

Барендрегт X. Ламбда-исчисление. Его синтаксис и семантика. M.: Мир. 1985. səh. 606 .

Həmçinin bax

Xarici keçidlər

λ-Hesablama: Sonra & İndi (ing.)
Lambda hesablaması (ing.)
Lambda Hesablamasına qısa bir giriş (ing.)
Lambda hesablaması — addımbaaddım (ing.)

[1] 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.

[2] 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.

[1]

[2]