Lambda hesabı abstraksiyaya əsaslanan hesablamaları ifadə etmək və bağlama və dəyişən əvəzetmədən istifadə edərək funksiyaları tətbiq etmək üçün riyazi məntiqdə formal sistemdir. Bu, istənilən Turing maşınının dizaynına tətbiq oluna bilən universal modeldir. Lambda hesabı ilk dəfə 1930-cu illərdə məşhur riyaziyyatçı Çörç tərəfindən təqdim edilmişdir.
Sistem lambda üzvlərinin qurulmasından və onlar üzərində azalma əməliyyatlarının yerinə yetirilməsindən ibarətdir.
İzahlar və Tətbiqlər
Yunan hərfi lambda (λ) funksiyada dəyişənin bağlanmasını ifadə etmək üçün lambda ifadələrində və lambda terminlərində istifadə olunur.
Lambda hesablaması tipsiz və ya çap edilə bilər. Birinci variantda funksiyalar yalnız bu tip məlumatları qəbul etmək qabiliyyətinə malik olduqda istifadə edilə bilər. Yazılan lambda hesabları daha zəifdir, daha kiçik bir dəyər ifadə edə bilər. Lakin, digər tərəfdən, onlar sizə daha çox şeyi sübut etməyə imkan verir.
Bu qədər müxtəlif növlərin olmasının bir səbəbi alimlərin güclü lambda hesablama teoremlərini sübut etmək fürsətindən əl çəkmədən daha çox iş görmək istəyidir.
Sistem riyaziyyat, fəlsəfə, dilçilik və kompüter elminin bir çox müxtəlif sahələrində tətbiqlərə malikdir. Əvvəla, lambda hesablaması proqramlaşdırma dilləri nəzəriyyəsinin inkişafında mühüm rol oynamış hesablamadır. Sistemlərin həyata keçirdiyi funksional yaratma üslublarıdır. Onlar həmçinin bu kateqoriyaların nəzəriyyəsində ən çox yayılmış tədqiqat mövzusudur.
Butaylalar üçün
Lambda hesablaması riyaziyyatçı Alonzo Kilsəsi tərəfindən 1930-cu illərdə elmin əsaslarına dair araşdırmalarının bir hissəsi kimi təqdim edilmişdir. 1935-ci ildə Stiven Klin və J. B. Rosser Kleene-Rosser paradoksunu inkişaf etdirdikdə, orijinal sistemin məntiqi cəhətdən uyğunsuz olduğu göstərildi.
Daha sonra, 1936-cı ildə Church yalnız hesablamalara aid olan hissəni, indi tipsiz lambda hesabı adlanan hissəni ayırdı və nəşr etdi. 1940-cı ildə o, həmçinin əsas tip sistem kimi tanınan daha zəif, lakin məntiqi cəhətdən ardıcıl bir nəzəriyyə təqdim etdi. O, öz işində bütün nəzəriyyəni sadə dillərlə izah edir, ona görə də demək olar ki, Church dummies üçün lambda hesabını nəşr edib.
1960-cı illərə qədər onun proqramlaşdırma dilləri ilə əlaqəsi aydınlaşana qədər λ sadəcə formalizm idi. Riçard Montaqunun və digər dilçilərin təbii dilin semantikasındakı tətbiqləri sayəsində hesablama həm dilçilikdə, həm də kompüter elmində qürurlu yer tutdu.
Simvolun mənşəyi
Lambda bir söz və ya qıs altma mənasını vermir, o, Russell's Principal Mathematics kitabında iki mətbəə dəyişikliyindən qaynaqlanır. Qeyd nümunəsi: f (y)=2y + 1 olan f funksiyası üçün 2ŷ + 1-dir. Və burada giriş dəyişənini etiketləmək üçün y üzərində işarə (“şapka”) istifadə edirik.
Kilsə əvvəlcə oxşar simvollardan istifadə etməyi nəzərdə tutmuşdu, lakin yazıçılar "şapka" simvolunu hərflərin üstündə yerləşdirə bilmədilər. Beləliklə, onlar onu əvvəlcə "/\y.2y+1" kimi çap etdilər. Növbəti redaktə epizodunda makinaçılar "/ \" işarəsini vizual olaraq oxşar simvolla əvəz etdilər.
Lambda hesablamasına giriş
Sistem müəyyən formal sintaksis tərəfindən seçilən terminlər dilindən və onlarla manipulyasiya etməyə imkan verən transformasiya qaydaları toplusundan ibarətdir. Sonuncu nöqtə bərabərlik nəzəriyyəsi və ya əməliyyat tərifi kimi qəbul edilə bilər.
Lambda hesablamasındakı bütün funksiyalar anonimdir, yəni onların adları yoxdur. Onlar yalnız bir giriş dəyişənini götürür və çox dəyişənli süjetləri həyata keçirmək üçün köriləmə istifadə olunur.
Lambda şərtləri
Hesab sintaksisi bəzi ifadələri etibarlı, digərlərini isə etibarsız kimi müəyyən edir. Necə ki, müxtəlif simvol sətirləri etibarlı C proqramlarıdır, bəziləri isə yox. Lambda hesabının faktiki ifadəsi "lambda termini" adlanır.
Aşağıdakı üç qayda ola biləcək induktiv tərif verirbütün sintaktik cəhətdən etibarlı anlayışların qurulmasına müraciət edin:
X dəyişəninin özü etibarlı lambda terminidir:
- T LT-dirsə və x qeyri-sabitdirsə, (lambda xt) abstraksiya adlanır.
- əgər T və s anlayışlardırsa, (TS) tətbiq adlanır.
Başqa heç nə lambda termini deyil. Beləliklə, konsepsiya yalnız və yalnız bu üç qaydanın təkrar tətbiqi ilə əldə edilə bildikdə etibarlıdır. Bununla belə, bəzi mötərizələr digər meyarlara görə buraxıla bilər.
Tərif
Lambda ifadələri bunlardan ibarətdir:
- dəyişənlər v 1, v 2, …, v n, …
- abstraksiya 'λ' və nöqtə 'simvolları.'
- mötərizə ().
Λ çoxluğu induktiv olaraq təyin edilə bilər:
- Əgər x dəyişəndirsə, o zaman x ∈ Λ;
- x sabit deyil və M ∈ Λ, onda (λx. M) ∈ Λ;
- M, N ∈ Λ, sonra (MN) ∈ Λ.
Təyinat
Lambda ifadələrinin qeydini səliqəsiz saxlamaq üçün adətən aşağıdakı konvensiyalar istifadə olunur:
- Xarici mötərizələr buraxıldı: (MN əvəzinə MN).
- Tətbiqlərin assosiativ qalacağı güman edilir: ((MN) P yerinə MNP yazmaq olar).
- Astraksiya gövdəsi daha da sağa doğru uzanır: λx. MN λx deməkdir. (MN), yox (λx. M) N.
- Astraksiyaların ardıcıllığı azaldılıb: λx.λy.λz. N λxyz. N ola bilər.
Sərbəst və bağlı dəyişənlər
Operator λ onun qeyri-sabitini abstraksiya gövdəsinin hər yerində birləşdirir. Əhatə dairəsinə daxil olan dəyişənlərə bağlı deyilir. λ x ifadəsində. M, λ x hissəsi çox vaxt bağlayıcı kimi istinad edilir. Sanki M-ə X x əlavə etməklə dəyişənlərin qrup halına gəlməsinə işarə edir. Bütün digər qeyri-sabit olanlar sərbəst adlanır.
Məsələn, λ y ifadəsində. x x y, y - bağlı qeyri-daimi və x - pulsuz. Həm də qeyd etmək lazımdır ki, dəyişən "ən yaxın" abstraksiyasına görə qruplaşdırılır. Aşağıdakı misalda lambda hesablama həlli ikinci terminlə əlaqəli x-in tək baş verməsi ilə təmsil olunur:
λ x. y (λ x. z x)
Sərbəst dəyişənlər M çoxluğu FV (M) kimi işarələnir və terminlərin strukturu üzərində rekursiya ilə aşağıdakı kimi müəyyən edilir:
- FV (x)={x}, burada x dəyişəndir.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Sərbəst dəyişənləri ehtiva etməyən düstur qapalı adlanır. Qapalı lambda ifadələri kombinatorlar kimi də tanınır və kombinator məntiqindəki terminlərə ekvivalentdir.
Abreviatura
Lambda ifadələrinin mənası onların necə qısaldılması ilə müəyyən edilir.
Üç növ kəsmə var:
- α-transform: bağlı dəyişənlərin dəyişdirilməsi (alfa).
- β-reduksiya: onların arqumentlərinə funksiyaların tətbiqi (beta).
- η-transform: genişlənmə anlayışını əhatə edir.
Bu da buradadırSöhbət nəticədə yaranan ekvivalentlərdən gedir: iki ifadə eyni komponentə β-çevrilə bilirsə, β-ekvivalentdir və α / η-ekvivalentlik oxşar şəkildə müəyyən edilir.
Azaldıla bilən dövriyyə üçün qısaldılmış redex termini qaydalardan biri ilə azaldıla bilən alt mövzulara aiddir. Butaforlar üçün Lambda hesabı, nümunələr:
(λ x. M) N, M-də N-nin x ilə əvəz edilməsi ifadəsində beta redeksidir. Redexin azaldığı komponent onun reduksiyası adlanır. Azalma (λ x. M) N M [x:=N]-dir.
Əgər x M-də sərbəst deyilsə, λ x. M x həmçinin tənzimləyici M. ilə em-REDEX
α-çevrilmə
Alfa adlarının dəyişdirilməsi sizə bağlı dəyişənlərin adlarını dəyişməyə imkan verir. Məsələn, x. x λ y verə bilər. y. Yalnız alfa çevrilməsində fərqlənən terminlərə α-ekvivalent deyilir. Çox vaxt lambda hesabından istifadə edərkən α-ekvivalentlər qarşılıqlı hesab olunur.
Alfa çevrilməsi üçün dəqiq qaydalar tamamilə əhəmiyyətsiz deyil. Birincisi, bu abstraksiya ilə yalnız eyni sistemlə əlaqəli dəyişənlərin adı dəyişdirilir. Məsələn, alfa çevrilməsi λ x.λ x. x λ y.λ x-ə səbəb ola bilər. x, lakin bu, λy.λx.y-yə səbəb olmaya bilər. Sonuncu orijinaldan fərqli məna daşıyır. Bu, dəyişən kölgə proqramlaşdırma konsepsiyasına bənzəyir.
İkincisi, qeyri-daimi başqa abstraksiya tərəfindən tutulmaqla nəticələnərsə, alfa çevrilməsi mümkün deyil. Məsələn, λ x.λ y-də x-i y ilə əvəz etsəniz. x, onda əldə edə bilərsinizλy.λy. u, bu heç də eyni deyil.
Statik əhatə dairəsi olan proqramlaşdırma dillərində ad həllini sadələşdirmək üçün alfa çevrilməsi istifadə edilə bilər. Eyni zamanda, dəyişən anlayışının ehtiva edən sahədə təyinatı maskalamamasına diqqət yetirin.
De Bruyne indeks notasiyasında istənilən iki alfa-ekvivalent termin sintaktik olaraq eynidir.
Əvəzetmə
E [V:=R] tərəfindən yazılmış dəyişikliklər E ifadəsində V dəyişəninin bütün sərbəst hallarının R dövriyyəsi ilə əvəz edilməsi prosesidir. λ baxımından əvəzetmə rekursiyanın lambdası ilə müəyyən edilir. konsepsiya strukturu üzrə hesablama aşağıdakı kimidir (qeyd: x və y - yalnız dəyişənlər, M və N - istənilən λ ifadəsi).
x [x:=N] ≡ N
y [x:=N] ≡ y əgər x ≠ y
(M 1 M 2) [x:=N] ≡ (M 1 [x:=N]) (M 2 [x:=N])
(λ x. M) [x:=N] ≡ λ x. M
(λ y. M) [x:=N] y λ y. (M [x:=N]) əgər x ≠ y olarsa, bu şərtlə ki, y ∉ FV (N).
Lambda abstraksiyasına əvəz etmək üçün bəzən ifadəni α-çevirmək lazımdır. Məsələn, (λ x. Y) [y:=x] (λ x. X) ilə nəticələndiyi doğru deyil, çünki əvəz edilmiş x sərbəst olmalı idi, lakin sonunda bağlandı. Bu halda düzgün əvəzləmə (λ z. X) α-ekvivalentinə qədərdir. Qeyd edək ki, əvəzetmə lambdaya qədər unikal şəkildə müəyyən edilir.
β-azalma
Beta azaldılması funksiyanın tətbiqi ideyasını əks etdirir. Beta-reduktiv terminlərlə müəyyən edilirəvəzetmə: ((X V. E) E ') E [V:=E']-dir.
Məsələn, bəzi kodlaşdırma 2, 7, × fərz etsək, aşağıdakı β-reduksiya var: ((λ n. N × 2) 7) → 7 × 2.
Beta reduksiyasına Karri-Hovard izomorfizmi vasitəsilə təbii deduksiya altında yerli azalma anlayışı kimi baxmaq olar.
η-transform
Bu çevrilmə genişlənmə ideyasını ifadə edir, bu kontekstdə iki funksiya bütün arqumentlər üçün eyni nəticəni verdikdə bərabərdir. Bu çevrilmə λ x arasında dəyişir. (F x) və f f-də x sərbəst görünmədikdə.
Bu hərəkət Karri-Hovard izomorfizmi vasitəsilə təbii deduksiyada yerli tamlıq konsepsiyası ilə eyni hesab edilə bilər.
Normal formalar və birləşmə
Tip edilməmiş lambda hesabı üçün β-reduksiya qaydası ümumiyyətlə nə güclü, nə də zəif normallaşdırıcıdır.
Bununla belə, göstərilə bilər ki, β-reduksiya α-çevrilmədən əvvəl işləyərkən birləşir (yəni, birindən digərinə α-çevrilməsi mümkün olarsa, iki normal forma bərabər hesab edilə bilər).
Ona görə də həm güclü normallaşdıran terminlər, həm də zəif düzəliş edən terminlər vahid normal formaya malikdir. İlk şərtlər üçün istənilən azalma strategiyasının tipik konfiqurasiya ilə nəticələnəcəyinə zəmanət verilir. Halbuki zəif normallaşan şərtlər üçün bəzi az altma strategiyaları bunu tapa bilməz.
Əlavə proqramlaşdırma üsulları
Lambda hesabı üçün çoxlu yaradılış deyimləri var. Onların bir çoxu əvvəlcə sistemlərin proqramlaşdırma dilinin semantikasının əsası kimi istifadə edilməsi, onların aşağı səviyyəli konstruksiya kimi effektiv tətbiqi kontekstində işlənib hazırlanmışdır. Bəzi üslublar fraqment kimi lambda hesabını (və ya çox oxşar bir şey) ehtiva etdiyinə görə, bu üsullar praktik yaradıcılıqda da istifadə olunur, lakin sonra qaranlıq və ya xarici kimi qəbul edilə bilər.
Adlı sabitlər
Lambda hesablamasında kitabxana əvvəllər müəyyən edilmiş funksiyalar toplusu formasını alır, burada terminlər sadəcə konkret sabitlərdir. Saf hesablamada adlandırılmış dəyişməzlər anlayışı yoxdur, çünki bütün atom lambda şərtləri dəyişəndir. Lakin onlar dəyişkənliyi sabitin adı kimi götürməklə, bu uçucunu bədəndə bağlamaq üçün lambda abstraksiyasından istifadə etməklə və həmin abstraksiyanı nəzərdə tutulan tərifə tətbiq etməklə də təqlid edilə bilər. Beləliklə, əgər M-ni N-də təmsil etmək üçün f istifadə etsəniz,deyə bilərsiniz.
(λ f. N) M.
Müəlliflər tez-tez şeylərin daha intuitiv şəkildə yazılmasına icazə vermək kimi sintaktik konsepsiya təqdim edirlər.
f=M - N
Belə tərifləri zəncirləməklə, proqramın əsas hissəsini təşkil edən təriflərdən istifadə edərək, bir lambda üzvünün izlədiyi sıfır və ya daha çox funksiya tərifləri kimi lambda hesablama "proqramı" yazmaq olar.
Bunun diqqətəlayiq məhdudiyyəti f adının M-də müəyyən edilməməsidir,M lambda abstraksiyasının məcburi əhatə dairəsindən kənarda olduğundan f. Bu o deməkdir ki, rekursiv funksiya atributundan let ilə M kimi istifadə edilə bilməz. Bu üslubda rekursiv funksiya təriflərini yazmağa imkan verən daha təkmil letrec sintaksisi əlavə olaraq bunun əvəzinə sabit nöqtəli kombinatorlardan istifadə edir.
Çap edilmiş analoqlar
Bu tip anonim funksiya abstraksiyasını təmsil etmək üçün simvoldan istifadə edən tipli formalizmdir. Bu kontekstdə tiplər adətən lambda terminlərinə təyin olunan sintaktik xarakterli obyektlərdir. Dəqiq təbiət sözügedən hesablamadan asılıdır. Müəyyən nöqteyi-nəzərdən yazılan Lİ tipsiz Lİ-nin təkmilləşdirmələri hesab edilə bilər. Lakin digər tərəfdən, onlar da daha fundamental nəzəriyyə hesab oluna bilər və tipsiz lambda hesabı yalnız bir növü olan xüsusi haldır.
Typed LI proqramlaşdırma dillərinin əsasını və ML və Haskell kimi funksional dillərin əsasını təşkil edir. Və daha dolayısı ilə imperativ yaradılış üslubları. Tiplənmiş lambda hesabları proqramlaşdırma dilləri üçün tip sistemlərinin inkişafında mühüm rol oynayır. Burada yazım qabiliyyəti adətən proqramın istənilən xassələrini tutur, məsələn, yaddaşa girişin pozulmasına səbəb olmayacaq.
Yazılan lambda hesabları Curry-Howard izomorfizmi vasitəsilə riyazi məntiq və sübut nəzəriyyəsi ilə sıx bağlıdır və kateqoriya siniflərinin daxili dili kimi düşünülə bilər, məsələn,sadəcə Kartezyen qapaqların tərzidir.
