Լամբդա հաշվարկը մաթեմատիկական տրամաբանության ֆորմալ համակարգ է՝ աբստրակցիայի վրա հիմնված հաշվարկներն արտահայտելու և ֆունկցիաները կիրառելու համար՝ օգտագործելով կապող և փոփոխական փոխարինում: Սա ունիվերսալ մոդել է, որը կարող է կիրառվել ցանկացած Turing մեքենայի նախագծման համար: Լամբդա հաշվարկն առաջին անգամ ներդրվել է հայտնի մաթեմատիկոս Չերչի կողմից 1930-ականներին:
Համակարգը բաղկացած է լամբդա անդամներ կառուցելուց և դրանց վրա կրճատման գործողություններ կատարելուց:
Բացատրություններ և կիրառություններ
Հունարեն լամբդա (λ) տառը օգտագործվում է լամբդա արտահայտություններում և լամբդա տերմիններում՝ ֆունկցիայի մեջ փոփոխականի կապակցումը նշելու համար:
Լամբդայի հաշվարկը կարող է լինել անտիպ կամ տպագրված: Առաջին տարբերակում գործառույթները կարող են օգտագործվել միայն այն դեպքում, եթե դրանք ի վիճակի են ստանալ այս տեսակի տվյալներ: Տպված լամբդա հաշվարկներն ավելի թույլ են, կարող են ավելի փոքր արժեք արտահայտել: Բայց, մյուս կողմից, նրանք թույլ են տալիս ապացուցել ավելի շատ բաներ:
Այդքան տարբեր տեսակների գոյության պատճառներից մեկն այն է, որ գիտնականների ցանկությունն է ավելին անել՝ չհրաժարվելով լամբդա հաշվարկի ուժեղ թեորեմներն ապացուցելու հնարավորությունից:
Համակարգն ունի կիրառություն մաթեմատիկայի, փիլիսոփայության, լեզվաբանության և համակարգչային գիտության տարբեր ոլորտներում: Նախ, լամբդա հաշվարկը հաշվարկ է, որը կարևոր դեր է խաղացել ծրագրավորման լեզուների տեսության զարգացման գործում։ Հենց ֆունկցիոնալ ստեղծման ոճերն են իրականացնում համակարգերը: Դրանք նաև հետազոտության թեժ թեմա են այս կատեգորիաների տեսության մեջ:
Դիմերի համար
Լամբդայի հաշվարկը ներդրվել է մաթեմատիկոս Ալոնզո Չերչի կողմից 1930-ականներին՝ որպես գիտության հիմունքների իր հետազոտության մի մաս: Պարզվեց, որ սկզբնական համակարգը տրամաբանորեն անհամապատասխան է 1935 թվականին, երբ Սթիվեն Քլինը և Ջ. Բ. Ռոսսերը մշակեցին Քլին-Ռոսեր պարադոքսը:
Ավելի ուշ՝ 1936 թվականին, Չերչը առանձնացրեց և հրապարակեց միայն այն մասը, որը վերաբերում է հաշվարկներին, այն, ինչ այժմ կոչվում է անտիպ լամբդա հաշվարկ: 1940 թվականին նա նաև ներկայացրեց ավելի թույլ, բայց տրամաբանորեն հետևողական տեսություն, որը հայտնի է որպես պարզ տիպի համակարգ։ Իր աշխատության մեջ նա բացատրում է ամբողջ տեսությունը պարզ բառերով, ուստի կարելի է ասել, որ Չերչը հրապարակել է լամբդա հաշվարկը կեղծիքների համար։
Մինչև 1960-ականները, երբ նրա կապը ծրագրավորման լեզուների հետ պարզ դարձավ, λ-ն ընդամենը ֆորմալիզմ էր: Բնական լեզվի իմաստաբանության մեջ Ռիչարդ Մոնթագուի և այլ լեզվաբանների կիրառությունների շնորհիվ հաշվարկը հպարտորեն տեղ է գրավել ինչպես լեզվաբանության, այնպես էլ համակարգչային գիտության մեջ:
Սիմվոլի ծագումը
Լամբդան չի նշանակում բառ կամ հապավում, այն գալիս է Ռասելի Հիմնական մաթեմատիկայի հղումից, որին հաջորդում են երկու տպագրական փոփոխություններ: Նշման օրինակ. f (y)=2y + 1 ֆունկցիայի համար 2ŷ + 1 է: Եվ այստեղ մենք օգտագործում ենք մակագրություն («գլխարկ») y-ի վրա՝ մուտքային փոփոխականը պիտակավորելու համար:
Եկեղեցին ի սկզբանե մտադիր էր օգտագործել նմանատիպ խորհրդանիշներ, սակայն գրամեքենաները չեն կարողացել «գլխարկ» նշանը դնել տառերի վերևում: Այսպիսով, փոխարենը նրանք տպեցին այն սկզբնապես որպես «/\y.2y+1»: Խմբագրման հաջորդ դրվագում մեքենագրողները «/ \»-ը փոխարինեցին տեսողականորեն նման գրանշանով։
Ներածություն լամբդայի հաշվարկին
Համակարգը բաղկացած է տերմինների լեզվից, որոնք ընտրվում են որոշակի ֆորմալ շարահյուսությամբ, և փոխակերպման կանոնների մի շարք, որոնք թույլ են տալիս դրանք շահարկել: Վերջին կետը կարելի է համարել որպես հավասարման տեսություն կամ որպես գործառնական սահմանում։
Լամբդա հաշվարկի բոլոր ֆունկցիաները անանուն են, այսինքն՝ անուններ չունեն: Նրանք վերցնում են միայն մեկ մուտքային փոփոխական, և currying-ն օգտագործվում է բազմաթիվ փոփոխականներով սյուժեներ իրականացնելու համար:
Լամբդայի պայմաններ
Հաշվի շարահյուսությունը որոշ արտահայտություններ սահմանում է որպես վավեր, իսկ մյուսները՝ անվավեր: Ճիշտ այնպես, ինչպես նիշերի տարբեր տողերը վավեր C ծրագրեր են, իսկ որոշները՝ ոչ: Լամբդա հաշվարկի իրական արտահայտությունը կոչվում է «լամբդա տերմին»:
Հետևյալ երեք կանոնները տալիս են ինդուկտիվ սահմանում, որը կարող է լինելկիրառել բոլոր շարահյուսական վավերական հասկացությունների կառուցման համար՝
X փոփոխականն ինքնին վավեր լամբդա տերմին է.
- եթե T-ը LT է, իսկ x-ը՝ ոչ հաստատուն, ապա (lambda xt) կոչվում է աբստրակցիա։
- եթե T-ը, ինչպես նաև s-ը հասկացություններ են, ապա (TS) կոչվում է հավելված:
Ուրիշ ոչինչ լամբդա տերմին չէ: Այսպիսով, հայեցակարգը վավեր է, եթե և միայն այն դեպքում, եթե այն կարելի է ձեռք բերել այս երեք կանոնների կրկնակի կիրառմամբ: Այնուամենայնիվ, որոշ փակագծեր կարող են բաց թողնել այլ չափանիշների համաձայն:
Սահմանում
Լամբդա արտահայտությունները բաղկացած են՝
- փոփոխականներ v 1, v 2, …, v n, …
- աբստրակցիայի «λ» և «կետ» խորհրդանիշները։'
- փակագծեր ().
Լ բազմությունը կարող է սահմանվել ինդուկտիվ կերպով՝
- Եթե x-ը փոփոխական է, ապա x ∈ Λ;
- x-ը հաստատուն չէ և M ∈ Λ, ապա (λx. M) ∈ Λ;
- M, N ∈ Λ, ապա (MN) ∈ Լ.
Նշանակում
Լամբդա արտահայտությունների նշումն անխռով պահելու համար սովորաբար օգտագործվում են հետևյալ պայմանականությունները.
- Արտաքին փակագծերը բաց են թողնվել. MN փոխարեն (MN):
- Ենթադրվում է, որ հայտերը մնում են ասոցիատիվ. կարելի է գրել MNP ((MN) P-ի փոխարեն):
- Աբստրակցիայի մարմինը ձգվում է ավելի աջ. λx. MN նշանակում է λx: (MN), ոչ (λx. M) N.
- Աբստրակցիաների հաջորդականությունը կրճատվում է. λx.λy.λz. N կարող է լինել λxyz. N.
Ազատ և սահմանափակ փոփոխականներ
Լ օպերատորը միացնում է իր ոչ հաստատունը, որտեղ էլ որ այն գտնվում է աբստրակցիայի մարմնում: Փոփոխականները, որոնք մտնում են շրջանակի մեջ, կոչվում են կապված: λ x արտահայտության մեջ. M, λ x մասը հաճախ կոչվում է կապող: Կարծես ակնարկելով, որ փոփոխականները դառնում են խումբ՝ X x-ի ավելացումով M-ին: Բոլոր մյուս անկայունները կոչվում են ազատ:
Օրինակ, λ y արտահայտության մեջ. x x y, y - կապված ոչ մշտական, իսկ x - անվճար: Եվ հարկ է նաև նշել, որ փոփոխականը խմբավորված է իր «մոտակա» վերացականությամբ: Հետևյալ օրինակում լամբդա հաշվարկի լուծումը ներկայացված է x-ի մեկ երևույթով, որը կապված է երկրորդ անդամի հետ.
λ x. y (λ x. z x)
Ազատ փոփոխականների բազմությունը M նշվում է որպես FV (M) և սահմանվում է ռեկուրսիայով տերմինների կառուցվածքի վրա հետևյալ կերպ.
- FV (x)={x}, որտեղ x-ը փոփոխական է:
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Բանաձևը, որը չի պարունակում ազատ փոփոխականներ, կոչվում է փակ: Փակ լամբդա արտահայտությունները հայտնի են նաև որպես կոմբինատորներ և համարժեք են կոմբինատոր տրամաբանության տերմիններին:
Հապավում
Լամբդա արտահայտությունների նշանակությունը որոշվում է նրանով, թե ինչպես կարող են դրանք կրճատվել:
Կա երեք տեսակի կրճատումներ.
- α-տրանսֆորմ. փոփոխվող սահմանափակ փոփոխականները (ալֆա).
- β-կրճատում. գործառույթների կիրառում իրենց արգումենտներին (բետա):
- η-տրանսֆորմ. ընդգրկում է ընդարձակման հասկացությունը:
Ահա և այնմենք խոսում ենք ստացված համարժեքների մասին. երկու արտահայտությունները β-համարժեք են, եթե դրանք կարող են β-փոխակերպվել նույն բաղադրիչի, և α/η-համարժեքությունը սահմանվում է նույն կերպ:
Ռեդեքս տերմինը, որը կրճատված է կրճատվող շրջանառություն, վերաբերում է ենթաթեմաներին, որոնք կարող են կրճատվել կանոններից մեկով: Լամբդայի հաշվարկ կեղծիքների համար, օրինակներ՝
(λ x. M) N-ը բետա-redex է M-ում N-ով x-ով փոխարինելու արտահայտության մեջ: Բաղադրիչը, որին կրճատվում է ռեդեքսը, կոչվում է դրա կրճատում: Կրճատումը (λ x. M) N-ը M է [x:=N]:
Եթե x-ը M-ում ազատ չէ, λ x: M x նաև em-REDEX կարգավորիչով M.
α-փոխակերպում
Ալֆա վերանվանումները թույլ են տալիս փոխել կապված փոփոխականների անունները: Օրինակ, x. x-ը կարող է տալ λ y: y. Այն տերմինները, որոնք տարբերվում են միայն ալֆա փոխակերպմամբ, ասում են, որ α-համարժեք են: Հաճախ, երբ օգտագործվում է լամբդա հաշվարկը, α-համարժեքները համարվում են փոխադարձ:
Ալֆա փոխակերպման ճշգրիտ կանոնները բոլորովին չնչին չեն: Նախ, այս աբստրակցիայով վերանվանվում են միայն այն փոփոխականները, որոնք կապված են նույն համակարգի հետ։ Օրինակ, ալֆա փոխակերպումը λ x.λ x. x-ը կարող է հանգեցնել λ y.λ x. x, բայց դա կարող է չհանգեցնել λy.λx.y-ին: Վերջինս ունի տարբեր նշանակություն, քան բնօրինակը: Սա նման է փոփոխական ստվերային ծրագրավորման հայեցակարգին:
Երկրորդ, ալֆա փոխակերպումը հնարավոր չէ, եթե այն կհանգեցնի ոչ մշտական այլ աբստրակցիային: Օրինակ, եթե x-ը փոխարինեք y-ով λ x.λ y-ում: x, ապա կարող եք ստանալλy.λy. u, որն ամենևին էլ նույնը չէ։
Ստատիկ տիրույթով ծրագրավորման լեզուներում ալֆա փոխակերպումը կարող է օգտագործվել անվանման լուծումը պարզեցնելու համար: Միևնույն ժամանակ, հոգ տանելով, որ փոփոխականի հայեցակարգը չքողարկի նշումը պարունակող տարածքում:
Դե Բրույնեի ինդեքսի նշումներում ցանկացած երկու ալֆա-համարժեք տերմիններ շարահյուսորեն նույնական են:
Փոխարինում
E [V:=R]-ով գրված փոփոխությունները E արտահայտության մեջ V փոփոխականի բոլոր ազատ երևույթները փոխարինելու գործընթացն են R շրջանառությամբ: λ-ով փոխարինումը սահմանվում է ռեկուրսիայի լամբդայով: Հայեցակարգի կառուցվածքի հաշվարկը հետևյալ կերպ (նշում. x և y - միայն փոփոխականներ, և M և N - ցանկացած λ-արտահայտություն):
x [x:=N] ≡ N
y [x:=N] ≡ y, եթե 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]), եթե x ≠ y, պայմանով, որ y ∉ FV (N).
Լամբդա աբստրակցիայի փոխարինման համար երբեմն անհրաժեշտ է α-փոխակերպել արտահայտությունը: Օրինակ, ճիշտ չէ, որ (λ x. Y) [y:=x] հանգեցնում է (λ x. X), որովհետև փոխարինված x-ը պետք է ազատ լիներ, բայց ի վերջո կապված լիներ: Ճիշտ փոխարինումն այս դեպքում (λ z. X) է մինչև α-համարժեքը։ Նկատի ունեցեք, որ փոխարինումը եզակիորեն սահմանված է մինչև լամբդա:
β-կրճատում
Բետա կրճատումն արտացոլում է գործառույթ կիրառելու գաղափարը: Բետա-նվազեցնողը սահմանվում է տերմիններովփոխարինում. ((X V. E) E ') E [V:=E'] է:
Օրինակ, ենթադրելով որոշ կոդավորում 2, 7, ×, կա հետևյալ β-կրճատումը. ((λ n. N × 2) 7) → 7 × 2.
Բետա կրճատումը կարելի է համարել նույնը, ինչ տեղային կրճատելիության հայեցակարգը բնական դեդուկցիայի միջոցով Քարի-Հովարդի իզոմորֆիզմի միջոցով:
η-փոխակերպում
Այս փոխարկումն արտահայտում է ընդարձակման գաղափարը, որն այս համատեքստում այն է, որ երկու ֆունկցիաները հավասար են, երբ բոլոր արգումենտների համար տալիս են նույն արդյունքը: Այս փոխակերպումը փոխանակվում է λ x-ի միջև: (F x) և f, երբ x-ն ազատ չի թվում f-ում։
Այս գործողությունը կարելի է համարել նույնը, ինչ տեղային ամբողջականության հայեցակարգը բնական դեդուկցիայում Քարի-Հովարդի իզոմորֆիզմի միջոցով:
Նորմալ ձևեր և միաձուլում
Անտիպ լամբդա հաշվարկի համար β-կրճատման կանոնը սովորաբար ոչ ուժեղ է, ոչ էլ թույլ նորմալացնող:
Այնուամենայնիվ, կարելի է ցույց տալ, որ β-կրճատումը միաձուլվում է α-փոխակերպումից առաջ գործելու ժամանակ (այսինքն, երկու նորմալ ձևերը կարող են հավասար համարվել, եթե հնարավոր է α-վերափոխումը մեկից մյուսը):
Հետևաբար, և՛ խիստ նորմալացնող, և՛ թույլ ճշգրտվող տերմինները ունեն մեկ նորմալ ձև: Առաջին տերմինների համար ցանկացած կրճատման ռազմավարություն երաշխավորված է տիպիկ կոնֆիգուրացիայի արդյունքում: Մինչդեռ թույլ նորմալացնող պայմանների դեպքում որոշ նվազեցման ռազմավարություններ կարող են դա չգտնել:
ծրագրավորման լրացուցիչ մեթոդներ
Լամբդա հաշվարկի համար ստեղծման շատ արտահայտություններ կան: Դրանցից շատերն ի սկզբանե մշակվել են համակարգերը որպես ծրագրավորման լեզվի իմաստաբանության հիմք օգտագործելու համատեքստում՝ դրանք արդյունավետորեն կիրառելով որպես ցածր մակարդակի կառուցվածք: Քանի որ որոշ ոճեր ներառում են լամբդա հաշվարկ (կամ շատ նման մի բան) որպես հատված, այս տեխնիկան նաև օգտագործվում է գործնական ստեղծման մեջ, բայց այնուհետև կարող է ընկալվել որպես անհասկանալի կամ օտար:
Անվանված հաստատուններ
Լամբդա հաշվարկում գրադարանը ստանում է նախկինում սահմանված ֆունկցիաների մի շարք, որտեղ տերմինները պարզապես կոնկրետ հաստատուններ են: Մաքուր հաշվարկը չունի անվանված անփոփոխների հասկացություն, քանի որ ատոմային լամբդա բոլոր տերմինները փոփոխականներ են: Բայց դրանք կարող են նաև ընդօրինակվել՝ ընդունելով փոփոխականը որպես հաստատունի անուն, օգտագործելով լամբդա աբստրակցիան՝ կապելու այդ ցնդող նյութը մարմնում և կիրառելով այդ աբստրակցիան նախատեսված սահմանմանը: Այսպիսով, եթե դուք օգտագործում եք f-ը՝ M-ը N-ում ներկայացնելու համար, կարող եք ասել
(λ f. N) M.
Հեղինակները հաճախ ներկայացնում են շարահյուսական հասկացություն, ինչպիսին է թույլ տալ, որպեսզի իրերը գրվեն ավելի ինտուիտիվ ձևով:
f=M-ից N
Շղթայելով նման սահմանումները՝ կարելի է գրել լամբդա հաշվարկի «ծրագիր» որպես զրոյական կամ ավելի ֆունկցիայի սահմանումներ, որին հաջորդում են մեկ լամբդա անդամ՝ օգտագործելով այն սահմանումները, որոնք կազմում են ծրագրի մեծ մասը:
Սրա ուշագրավ սահմանափակումն այն է, որ f անունը սահմանված չէ M-ում,քանի որ M-ը դուրս է լամբդա աբստրակցիայի պարտադիր շրջանակից f. Սա նշանակում է, որ ռեկուրսիվ ֆունկցիայի հատկանիշը չի կարող օգտագործվել որպես M let-ով: Ավելի առաջադեմ letrec շարահյուսությունը, որը թույլ է տալիս գրել ռեկուրսիվ ֆունկցիայի սահմանումներ այս ոճով, փոխարենը լրացուցիչ օգտագործում է ֆիքսված կետի կոմբինատորներ:
Տպագիր անալոգներ
Այս տեսակը տպագրված ֆորմալիզմ է, որն օգտագործում է խորհրդանիշ՝ անանուն ֆունկցիայի աբստրակցիան ներկայացնելու համար: Այս համատեքստում տիպերը սովորաբար շարահյուսական բնույթի օբյեկտներ են, որոնք վերագրվում են լամբդա տերմիններին։ Ճշգրիտ բնույթը կախված է խնդրո առարկա հաշվարկից: Որոշակի տեսանկյունից տպագրված LI-ն կարելի է համարել որպես անտիպ LI-ի ճշգրտումներ։ Բայց մյուս կողմից, դրանք կարող են նաև համարվել ավելի հիմնարար տեսություն, և անտիպ լամբդա հաշվարկը հատուկ դեպք է միայն մեկ տիպով:
Typed LI-ն ծրագրավորման լեզուների հիմքն է և ֆունկցիոնալ լեզուների հիմքը, ինչպիսիք են ML-ը և Haskell-ը: Եվ, ավելի անուղղակիորեն, ստեղծագործության հրամայական ոճերը: Տպված լամբդա հաշվարկները կարևոր դեր են խաղում ծրագրավորման լեզուների տիպային համակարգերի մշակման գործում: Այստեղ տպագրելիությունը սովորաբար գրավում է ծրագրի ցանկալի հատկությունները, օրինակ՝ այն չի առաջացնի հիշողության հասանելիության խախտում:
Տիպված լամբդա հաշվարկները սերտորեն կապված են մաթեմատիկական տրամաբանության և ապացույցների տեսության հետ Քարի-Հովարդի իզոմորֆիզմի միջոցով և կարող են ընկալվել որպես կատեգորիաների դասերի ներքին լեզու, օրինակ, որըպարզապես դեկարտյան փակումների ոճն է։
