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 - hesablamaRedaktə

Saf  - 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ə abstraksiyaRedaktə

Ə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 ,hardaki,   — funksiya, a isə   — arqumentdir.Bu riyaziyyatda ümumi olan   notasiyaya uyğun gəlir,bəzən də həmçinin də istifadə olunur,lakin, λ-hesablama üçün  -in nəticəni verilən giriş dəyərindən hesablayan alqoritm kimi qəbul etməsi vacibdir. Bu mənada  ,  tətbiqinə iki cür baxmaq olar: tətbiqi nəticəsində   -dan   -ya və yaxudda hesablama prosesi olaraq  . 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   — ifadəsi sərbəst olan  , onda qeyd   bu mənanı verir:   arqumentdən funksiyası  , formaya sahibdir  ,bir funksiyanı ifadə edir  . Beləliklə, abstraksiya istifadə edərək yeni funksiyalar qura bilərsiniz. Tələb belə ki,  sərbəst şəkildə   -ya,daxil edilirsə, çox əhəmiyyətli deyil - fərz etmək kifayətdir ,əgər bu belə deyilsə.

α-ekvivalentlikRedaktə

Lambda baxımından müəyyən edilən ekvivalentliyin əsas forması alfa ekvivalentliyidir. Məsələn,    : 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    şərtləri alfa ekvivalenti deyildir.

β-reduksiyasıRedaktə

  ifadəsi bu funksiyanı ifadə edir,qəbulu hər birinə görə   dəyəri  , sonra ifadəni hesablamaq üçün

 ,

həm tətbiqi,   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ə   yetirmək lazımdır. Nəticədə   alınır. Bu mülahizə ümumi şəkildə

 

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ə  - hesablaması Tyurinq tamlıq xüsusiyyətinə malikdir və buna görə də ən sadə proqramlaşdırma dilidir.

η-çevrilməsiRedaktə

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

Əyrilmə(Kurrinq)Redaktə

İki dəyişənin funksiyası   и     -ın bir dəyişənin funksiyası hesab edilə bilər, bir dəyişən funksiyasını qaytaran , yeni bir ifadə  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ı  — 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 -semantikasıRedaktə

Bu bir faktdır ki, — lambda hesablamasının şərtləri funksiyaları kimi fəaliyyət göstərir, — şərtlərə tətbiq olunur(bu bəlkə də,özü-özünə), — hesablaması adekvat semantikanın qurulmasında çətinliklərə səbəb olur.  — hesablanmasına hər hansı bir məna vermək üçün,  çoxluğunu almaq zəruridir,hansıki,onun funksional məkanına  sərmayə qoyulacaqdı. Bunun ümumi vəziyyətində    -dan  -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ı,  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  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ı[en] yaradıldı.

Rekursiv funksiyalarla əlaqəRedaktə

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   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,   — sabit nöqtə  ; 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 ,hardaki,   — nömrə hansıki faktorialın hesablandlğı nömrədir.   -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ə   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əRedaktə

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

İstinadlarRedaktə

  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.

ƏdəbiyyatRedaktə

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

Həmçinin baxRedaktə

Xarici keçidlərRedaktə