Lambda hisobi - bu matematik mantiqda abstraktsiyaga asoslangan hisoblarni ifodalash va bog'lash va o'zgaruvchan almashtirish yordamida funktsiyalarni qo'llash uchun rasmiy tizim. Bu har qanday Tyuring mashinasining dizayni uchun qo'llanilishi mumkin bo'lgan universal model. Lambda hisobi birinchi marta 1930-yillarda mashhur matematik Chercx tomonidan kiritilgan.
Tizim lambda a'zolarini qurish va ular ustida qisqartirish amallarini bajarishdan iborat.
Tushuntirishlar va ilovalar
Yunoncha lambda (l) harfi lambda iboralarida va lambda atamalarida funksiyadagi oʻzgaruvchining bogʻlanishini bildirish uchun ishlatiladi.
Lambda hisobi yozilishi yoki yozilishi mumkin. Birinchi variantda funksiyalar faqat shu turdagi ma'lumotlarni qabul qilish imkoniyatiga ega bo'lsa foydalanish mumkin. Yozilgan lambda hisoblari zaifroq, kichikroq qiymatni ifodalashi mumkin. Biroq, boshqa tomondan, ular sizga ko'proq narsani isbotlash imkonini beradi.
Bunchalik xilma-xil boʻlishining sabablaridan biri olimlarning kuchli lambda hisobi teoremalarini isbotlash imkoniyatidan voz kechmasdan koʻproq ishlashga intilishidir.
Tizimda matematika, falsafa, tilshunoslik va informatikaning turli sohalarida ilovalar mavjud. Avvalo, lambda hisobi dasturlash tillari nazariyasining rivojlanishida muhim rol o‘ynagan hisobdir. Bu tizimlar amalga oshiradigan funktsional yaratish uslublari. Ular, shuningdek, ushbu toifalar nazariyasi bo‘yicha eng dolzarb tadqiqot mavzusidir.
Axmoqlar uchun
Lambda hisobi 1930-yillarda matematik Alonzo Cherkov tomonidan fan asoslariga oid tadqiqotlari doirasida kiritilgan. Asl tizim 1935 yilda Stiven Klin va J. B. Rosser Klin-Rosser paradoksini ishlab chiqqanida mantiqiy jihatdan nomuvofiq ekanligi ko'rsatilgan.
Keyinchalik, 1936 yilda Cherch faqat hisob-kitoblarga taalluqli bo'lgan qismini ajratib ko'rsatdi va nashr etdi, bu endi tiplanmagan lambda hisobi deb ataladi. 1940-yilda u zaifroq, ammo mantiqiy jihatdan izchil nazariyani taqdim etdi, bu asosiy tizim deb nomlanadi. O'z ishida u butun nazariyani sodda so'zlar bilan tushuntiradi, shuning uchun aytish mumkinki, Cherkov manikyurlar uchun lambda hisobini nashr etgan.
1960-yillargacha, uning dasturlash tillari bilan aloqasi aniq boʻlganida, l shunchaki rasmiyatchilik edi. Richard Montagu va boshqa tilshunoslarning tabiiy til semantikasida qoʻllanishlari tufayli hisob tilshunoslikda ham, informatikada ham faxrli oʻrinlarni egalladi.
Belgining kelib chiqishi
Lambda soʻz yoki qisqartmani anglatmaydi, u Rassellning Principal Mathematics kitobidagi havoladan soʻng ikkita tipografik oʻzgarishlardan kelib chiqqan. Belgilanish misoli: f (y)=2y + 1 bo‘lgan f funksiya uchun 2ŷ + 1 bo‘ladi. Bu yerda esa kiritilgan o‘zgaruvchini belgilash uchun y ustiga karet (“shlyapa”) qo‘llaniladi.
Cherkov dastlab shunga oʻxshash belgilardan foydalanishni moʻljallagan, biroq matn terish ustalari “shlyapa” belgisini harflar ustiga qoʻya olmagan. Buning o'rniga ular dastlab "/\y.2y+1" sifatida chop etishdi. Tahrirlashning keyingi qismida teruvchilar “/ \” belgisini vizual jihatdan oʻxshash belgi bilan almashtirdilar.
Lambda hisobiga kirish
Tizim ma'lum bir rasmiy sintaksis tomonidan tanlangan atamalar tilidan va ularni manipulyatsiya qilish imkonini beruvchi transformatsiya qoidalari to'plamidan iborat. Oxirgi nuqta tenglama nazariyasi yoki operatsion ta'rif sifatida ko'rib chiqilishi mumkin.
Lambda hisobidagi barcha funksiyalar anonim, ya'ni ularning nomlari yo'q. Ular faqat bitta kiritish oʻzgaruvchisini oladi va bir nechta oʻzgaruvchiga ega boʻlgan chizmalarni amalga oshirish uchun kurriing ishlatiladi.
Lambda shartlari
Hisob sintaksisi ba'zi ifodalarni to'g'ri, boshqalari esa noto'g'ri deb belgilaydi. Xuddi turli xil belgilar qatorlari C dasturlari bo'lgani kabi, ba'zilari esa haqiqiy emas. Lambda hisobining haqiqiy ifodasi "lambda atamasi" deb ataladi.
Quyidagi uchta qoida boʻlishi mumkin boʻlgan induktiv taʼrifni beradibarcha sintaktik asosli tushunchalar qurilishiga taalluqli:
X oʻzgaruvchisining oʻzi yaroqli lambda atamasi:
- agar T LT va x doimiy boʻlmasa, (lambda xt) abstraksiya deb ataladi.
- agar T ham, s ham tushuncha boʻlsa, (TS) ilova deyiladi.
Boshqa hech narsa lambda atamasi emas. Shunday qilib, kontseptsiya faqat ushbu uchta qoidani takroran qo'llash orqali olinishi mumkin bo'lgan taqdirdagina haqiqiy hisoblanadi. Biroq, ba'zi qavslar boshqa mezonlarga ko'ra o'tkazib yuborilishi mumkin.
Tanrif
Lambda iboralari quyidagilardan iborat:
- oʻzgaruvchilar v 1, v 2, …, v n, …
- abstraksiya belgilari 'l' va nuqta '.'
- qavslar ().
I toʻplami induktiv tarzda aniqlanishi mumkin:
- Agar x oʻzgaruvchi boʻlsa, x ∈ L;
- x doimiy emas va M ∈ L, keyin (lx. M) ∈ L;
- M, N ∈ L, keyin (MN) ∈ L.
Tayinlash
Lambda iboralarining notasini tartibsiz saqlash uchun odatda quyidagi konventsiyalardan foydalaniladi:
- Tashqi qavslar kiritilmagan: (MN) oʻrniga MN.
- Ilovalar assotsiativ boʻlib qoladi deb taxmin qilinadi: ((MN) P oʻrniga MNP yozish mumkin).
- Abstraksiya tanasi o'ngga cho'ziladi: lx. MN lx degan ma'noni anglatadi. (MN), emas (lx. M) N.
- Abstraktsiyalar ketma-ketligi qisqartirildi: lx.ly.lz. N lxyz. N bo'lishi mumkin.
Erkin va bogʻlangan oʻzgaruvchilar
Operator l o’zining doimiy bo’lmaganini abstraktsiya tanasining qayerida bo’lmasin bog’laydi. Qo'llash doirasiga kiradigan o'zgaruvchilar bog'langan deb ataladi. l x ifodasida. M, l x qismi ko'pincha bog'lovchi deb ataladi. Go'yo o'zgaruvchilar M ga X x qo'shilishi bilan guruhga aylanganiga ishora qilgandek. Boshqa barcha beqarorlar bepul deb nomlanadi.
Masalan, l y ifodasida. x x y, y - bog'langan doimiy bo'lmagan va x - erkin. Va shuni ham ta'kidlash joizki, o'zgaruvchi "eng yaqin" abstraktsiya bo'yicha guruhlangan. Quyidagi misolda lambda hisobi yechimi ikkinchi had bilan bog'liq bo'lgan x ning bir martalik ko'rinishi bilan ifodalanadi:
l x. y (l x. z x)
Erkin oʻzgaruvchilar toʻplami M FV (M) sifatida belgilanadi va atamalar tuzilishi boʻyicha quyidagi rekursiya bilan aniqlanadi:
- FV (x)={x}, bu erda x - o'zgaruvchi.
- FV (lx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Erkin oʻzgaruvchilar boʻlmagan formula yopiq deyiladi. Yopiq lambda ifodalari kombinator sifatida ham tanilgan va kombinator mantiqidagi atamalarga ekvivalentdir.
Qisqartma
Lambda iboralarining ma'nosi ularni qanday qisqartirish mumkinligi bilan belgilanadi.
Uch xil kesish mavjud:
- a-transform: bogʻlangan oʻzgaruvchilarni oʻzgartirish (alfa).
- b-kamaytirish: ularning argumentlariga funksiyalarni qoʻllash (beta).
- ķ-transform: kengaytma tushunchasini qamrab oladi.
Mana bu hambiz natijaviy ekvivalentlar haqida ketyapmiz: ikkita ifoda b-ekvivalent bo'lib, agar ular bir xil komponentga aylantirilishi mumkin bo'lsa va a / ē-ekvivalentlik xuddi shunday aniqlanadi.
Qayqariladigan aylanmaning qisqartmasi redex atamasi qoidalardan biri bilan qisqartirilishi mumkin bo'lgan kichik mavzularga ishora qiladi. Qo'g'irchoqlar uchun lambda hisobi, misollar:
(l x. M) N - M da N ni x bilan almashtirish ifodasidagi beta-qaytarilish. Redex kamaytiruvchi komponent uning qisqarishi deb ataladi. Qisqartirish (l x. M) N - M [x:=N].
Agar x Mda erkin bo'lmasa, l x. M x shuningdek, regulyator M. bilan em-REDEX
a-transformatsiya
Alfa nomini oʻzgartirish sizga bogʻlangan oʻzgaruvchilar nomlarini oʻzgartirish imkonini beradi. Masalan, x. x l y ni berishi mumkin. y. Faqat alfa transformatsiyasida farq qiladigan atamalar a-ekvivalent deyiladi. Ko'pincha, lambda hisobini ishlatganda, a-ekvivalentlar o'zaro hisoblanadi.
Alfa konvertatsiyasining aniq qoidalari mutlaqo ahamiyatsiz emas. Birinchidan, bu abstraktsiya bilan faqat bir xil tizim bilan bog'langan o'zgaruvchilar nomi o'zgartiriladi. Masalan, alfa konvertatsiyasi l x.l x. x l y.l x ga olib kelishi mumkin. x, lekin bu ly.lx.y ga olib kelmasligi mumkin, ikkinchisi asl ma'nodan farq qiladi. Bu oʻzgaruvchan soyali dasturlash tushunchasiga oʻxshaydi.
Ikkinchidan, agar doimiy bo'lmagan boshqa abstraksiya tomonidan qo'lga kiritilishiga olib keladigan bo'lsa, alfa transformatsiyasi mumkin emas. Masalan, l x.l y da x ni y bilan almashtirsangiz. x, keyin olishingiz mumkinly.ly. u, bu umuman bir xil emas.
Statik qamrovli dasturlash tillarida nomni aniqlashni soddalashtirish uchun alfa konversiyasidan foydalanish mumkin. Shu bilan birga, oʻzgaruvchi kontseptsiyasi oʻz ichiga olgan hududdagi belgilashni yashirmasligiga eʼtibor bering.
De Bryuyne indeks belgisida har qanday ikkita alfa-ekvivalent atamalar sintaktik jihatdan bir xil.
Almashtirish
E [V:=R] tomonidan yozilgan oʻzgarishlar E ifodasidagi V oʻzgaruvchining barcha erkin hodisalarini R aylanmasiga almashtirish jarayonidir. l boʻyicha almashtirish rekursiya lambdasi bilan aniqlanadi. kontseptsiya tuzilmasi bo'yicha hisob quyidagicha (eslatma: x va y - faqat o'zgaruvchilar, M va N - har qanday l-ifoda).
x [x:=N] ≡ N
y [x:=N] ≡ y agar x ≠ y
(M 1 M 2) [x:=N] ≡ (M 1 [x:=N]) (M 2 [x:=N])
(l x. M) [x:=N] ≡ l x. M
(l y. M) [x:=N] y l y. (M [x:=N]) agar x ≠ y bo'lsa, y ∉ FV (N) sharti bilan.
Lambda abstraktsiyasiga almashtirish uchun ba'zan ifodani a-o'zgartirish kerak bo'ladi. Masalan, (l x. Y) [y:=x] (l x. X) ga olib kelishi to'g'ri emas, chunki almashtirilgan x erkin bo'lishi kerak edi, lekin bog'langan bo'lishi kerak edi. Bu holda to'g'ri almashtirish (l z. X) a-ekvivalentga qadar. Esda tutingki, almashtirish lambdagacha yagona tarzda aniqlanadi.
b-kamaytirish
Beta-versiyasini qisqartirish funksiyani qoʻllash gʻoyasini aks ettiradi. Beta-reduktiv atamalar bilan belgilanadialmashtirish: ((X V. E) E ') E [V:=E'].
Masalan, ba'zi kodlash 2, 7, × deb faraz qilsak, quyidagi b-kamaytirish mavjud: ((l n. N × 2) 7) → 7 × 2.
Beta-versiyani kamaytirishni Karri-Xovard izomorfizmi orqali tabiiy chegirma ostida mahalliy qaytarilish tushunchasi bilan bir xil koʻrish mumkin.
ķ-transform
Ushbu konvertatsiya kengaytma gʻoyasini ifodalaydi, bu kontekstda ikkita funksiya barcha argumentlar uchun bir xil natija berganda teng boʻladi. Bu konvertatsiya l x o'rtasida almashinadi. (F x) va f f. da x bepul koʻrinmasa
Bu harakatni Karri-Xovard izomorfizmi orqali tabiiy deduksiyadagi mahalliy toʻliqlik tushunchasi bilan bir xil deb hisoblash mumkin.
Oddiy shakllar va sintez
Tirilmagan lambda hisobi uchun b-kamaytirish qoidasi odatda kuchli ham, kuchsiz ham normalizatsiya emas.
Shunga qaramay, a-transformatsiyadan oldin ishlaganda b-qaytarilish birlashishini ko'rsatish mumkin (ya'ni, agar biridan ikkinchisiga a-transformatsiya qilish mumkin bo'lsa, ikkita oddiy shakl teng deb hisoblanishi mumkin).
Shuning uchun kuchli normallashtiruvchi atamalar ham, kuchsiz moslashtiruvchi atamalar ham bitta normal shaklga ega. Birinchi shartlar uchun har qanday qisqartirish strategiyasi odatiy konfiguratsiyaga olib kelishi kafolatlanadi. Kuchsiz normallashadigan sharoitlarda esa, ba'zi kamaytirish strategiyalari buni topa olmasligi mumkin.
Qoʻshimcha dasturlash usullari
Lambda hisobi uchun yaratilish idiomalari juda koʻp. Ularning ko'pchiligi dastlab tizimlardan dasturlash tili semantikasining asosi sifatida foydalanish, ularni past darajadagi konstruksiya sifatida samarali qo'llash kontekstida ishlab chiqilgan. Ba'zi uslublar parcha sifatida lambda hisobini (yoki juda o'xshash narsani) o'z ichiga olganligi sababli, bu usullar amaliy yaratishda ham qo'llaniladi, lekin keyinchalik noaniq yoki begona sifatida qabul qilinishi mumkin.
Nomli konstantalar
Lambda hisob-kitobida kutubxona oldindan belgilangan funktsiyalar to'plami shaklida bo'ladi, bu erda atamalar faqat aniq konstantalardir. Sof hisobda nomlangan o'zgarmaslar tushunchasi yo'q, chunki barcha atomik lambda atamalari o'zgaruvchilardir. Ammo ularni doimiyning nomi sifatida o'zgaruvchanni olish, tanadagi o'zgaruvchanlikni bog'lash uchun lambda abstraktsiyasidan foydalanish va ushbu mavhumlikni mo'ljallangan ta'rifga qo'llash orqali ham taqlid qilish mumkin. Shunday qilib, agar siz N dagi M ni ifodalash uchun f dan foydalansangiz,deyishingiz mumkin.
(l f. N) M.
Mualliflar koʻpincha narsalarni intuitivroq tarzda yozishga ruxsat berish kabi sintaktik tushunchani kiritadilar.
f=M dan N
Bunday ta'riflarni zanjirlash orqali dasturning asosiy qismini tashkil etuvchi ta'riflardan foydalanib, lambda hisobi "dasturini" nol yoki undan ortiq funksiya ta'riflari va undan keyin bitta lambda a'zosi sifatida yozish mumkin.
Buning muhim cheklovi shundaki, f nomi M harfida aniqlanmagan.chunki M lambda abstraktsiyasining majburiy doirasidan tashqarida f. Bu shuni anglatadiki, rekursiv funktsiya atributidan let bilan M sifatida foydalanilmaydi. Ushbu uslubda rekursiv funksiya taʼriflarini yozish imkonini beruvchi yanada rivojlangan letrec sintaksisi qoʻshimcha ravishda oʻrniga qattiq nuqtali kombinatorlardan foydalanadi.
Bosma analoglar
Bu tip anonim funksiya abstraktsiyasini ifodalash uchun belgidan foydalanadigan yoziladigan formalizmdir. Shu nuqtai nazardan, tiplar odatda lambda atamalariga tayinlangan sintaktik xususiyatga ega ob'ektlardir. To'liq tabiat ko'rib chiqilayotgan hisob-kitoblarga bog'liq. Muayyan nuqtai nazardan, terilgan LI ni tiplanmagan LI ning takomillashtirilgani deb hisoblash mumkin. Biroq, boshqa tomondan, ularni yanada fundamental nazariya deb hisoblash mumkin va tiplanmagan lambda hisobi faqat bitta turdagi maxsus holatdir.
Typed LI dasturlash tillarining asosi va ML va Haskell kabi funktsional tillarning asosidir. Va bilvosita, yaratilishning imperativ uslublari. Tiplangan lambda hisoblari dasturlash tillari uchun tip tizimlarini ishlab chiqishda muhim rol o'ynaydi. Bu yerda matn terish qobiliyati odatda dasturning kerakli xususiyatlarini qamrab oladi, masalan, xotiraga kirish buzilishiga olib kelmaydi.
Tiplangan lambda hisoblari Karri-Govard izomorfizmi orqali matematik mantiq va isbot nazariyasi bilan chambarchas bog'liq va toifa sinflarining ichki tili sifatida qaralishi mumkin, masalan,oddiygina dekart yopilish uslubi.
