ლამბდა კალკულუსი არის ფორმალური სისტემა მათემატიკური ლოგიკაში აბსტრაქციაზე დაფუძნებული გამოთვლების გამოხატვისა და ფუნქციების გამოყენებისათვის სავალდებულო და ცვლადი ჩანაცვლების გამოყენებით. ეს არის უნივერსალური მოდელი, რომელიც შეიძლება გამოყენებულ იქნას ნებისმიერი Turing მანქანის დიზაინზე. ლამბდას გამოთვლა პირველად ჩერჩმა, ცნობილმა მათემატიკოსმა, 1930-იან წლებში შემოიტანა.
სისტემა შედგება ლამბდა წევრების აგებისა და მათზე შემცირების ოპერაციებისგან.
ახსნა და აპლიკაციები
ბერძნული ასო ლამბდა (λ) გამოიყენება ლამბდა გამონათქვამებში და ლამბდა ტერმინებში ცვლადის დაკავშირების აღსანიშნავად ფუნქციაში.
ლამბდას გამოთვლა შეიძლება იყოს არატიპირებული ან აკრეფილი. პირველ ვარიანტში ფუნქციების გამოყენება შესაძლებელია მხოლოდ იმ შემთხვევაში, თუ მათ შეუძლიათ ამ ტიპის მონაცემების მიღება. აკრეფილი ლამბდა კალკულები უფრო სუსტია, შეუძლია გამოხატოს უფრო მცირე მნიშვნელობა. მაგრამ, მეორე მხრივ, ისინი საშუალებას გაძლევთ დაამტკიცოთ მეტი რამ.
ერთი მიზეზი, რის გამოც ამდენი განსხვავებული ტიპი არსებობს, არის მეცნიერთა სურვილი, გააკეთონ მეტი ლამბდა გამოთვლის ძლიერი თეორემების დამტკიცების შესაძლებლობაზე უარის თქმის გარეშე.
სისტემას აქვს აპლიკაციები მათემატიკის, ფილოსოფიის, ლინგვისტიკისა და კომპიუტერული მეცნიერების მრავალ სხვადასხვა სფეროში. უპირველეს ყოვლისა, ლამბდა კალკულუსი არის კალკულუსი, რომელმაც მნიშვნელოვანი როლი ითამაშა პროგრამირების ენების თეორიის განვითარებაში. ეს არის ფუნქციური შექმნის სტილი, რომელსაც სისტემები ახორციელებენ. ისინი ასევე არის ამ კატეგორიების თეორიის კვლევის მთავარი თემა.
მუნჯებისთვის
ლამბდას გამოთვლა შემოიღო მათემატიკოსმა ალონცო ჩერჩმა 1930-იან წლებში, როგორც მეცნიერების საფუძვლების კვლევის ნაწილი. თავდაპირველი სისტემა ლოგიკურად არათანმიმდევრული იყო 1935 წელს, როდესაც სტივენ კლეინმა და ჯ.ბ. როსერმა განავითარეს კლეინ-როსერის პარადოქსი.
მოგვიანებით, 1936 წელს, ჩურჩხელამ გამოყო და გამოაქვეყნა მხოლოდ ის ნაწილი, რომელიც დაკავშირებულია გამოთვლებთან, რასაც ახლა უტიფრო ლამბდა კალკულუსს უწოდებენ. 1940 წელს მან ასევე შემოიტანა უფრო სუსტი, მაგრამ ლოგიკურად თანმიმდევრული თეორია, რომელიც ცნობილია როგორც ძირითადი ტიპის სისტემა. თავის ნაშრომში იგი ხსნის მთელ თეორიას მარტივი სიტყვებით, ასე რომ, შეიძლება ითქვას, რომ ჩუმებმა გამოაქვეყნა კალკულუს ლამბდა.
1960-იან წლებამდე, როდესაც მისი კავშირი პროგრამირების ენებთან ნათელი გახდა, λ მხოლოდ ფორმალიზმი იყო. რიჩარდ მონტაგუს და სხვა ლინგვისტთა გამოყენებების წყალობით ბუნებრივი ენის სემანტიკაში, გაანგარიშებამ დაიკავა ადგილი როგორც ლინგვისტიკაში, ასევე კომპიუტერულ მეცნიერებაში.
სიმბოლოს წარმოშობა
ლამბდა არ ნიშნავს სიტყვას ან აკრონიმს, ის მოდის რასელის ძირითადი მათემატიკის მითითებიდან, რასაც მოჰყვება ორი ტიპოგრაფიული ცვლილება. აღნიშვნის მაგალითი: f ფუნქციისთვის f (y)=2y + 1 არის 2ŷ + 1. და აქ ვიყენებთ კარტს („ქუდი“) y-ზე შეყვანის ცვლადის ლეიბლისთვის.
ეკლესია თავდაპირველად განზრახული ჰქონდა მსგავსი სიმბოლოების გამოყენებას, მაგრამ ტიპაჟებმა ვერ შეძლეს "ქუდის" სიმბოლო ასოების ზემოთ. ამის ნაცვლად, მათ დაბეჭდეს იგი თავდაპირველად, როგორც "/\y.2y+1". რედაქტირების შემდეგ ეპიზოდში, ტიპაპისტებმა შეცვალეს "/ \" ვიზუალურად მსგავსი სიმბოლოთი.
შესავალი ლამბდა გამოთვლებში
სისტემა შედგება ტერმინების ენისგან, რომლებიც არჩეულია გარკვეული ფორმალური სინტაქსით, და ტრანსფორმაციის წესების ნაკრებისგან, რომელიც მათ მანიპულირების საშუალებას იძლევა. ბოლო პუნქტი შეიძლება ჩაითვალოს როგორც განტოლების თეორია ან როგორც ოპერატიული განსაზღვრება.
ლამბდა გამოთვლების ყველა ფუნქცია ანონიმურია, რაც ნიშნავს, რომ მათ სახელები არ აქვთ. ისინი იღებენ მხოლოდ ერთ შეყვანის ცვლადს და currying გამოიყენება ნაკვეთების განსახორციელებლად მრავალი ცვლადით.
ლამბდას პირობები
გაანგარიშების სინტაქსი განსაზღვრავს ზოგიერთ გამონათქვამს, როგორც მართებულს, ზოგი კი - არასწორს. ისევე, როგორც სიმბოლოების სხვადასხვა სტრიქონები არის სწორი C პროგრამები და ზოგიერთი არა. ლამბდა კალკულუსის რეალურ გამოხატულებას ეწოდება "ლამბდა ტერმინი".
შემდეგი სამი წესი იძლევა ინდუქციურ განმარტებას, რომელიც შეიძლება იყოსვრცელდება ყველა სინტაქსურად მართებული ცნების კონსტრუქციაზე:
X ცვლადი თავისთავად არის სწორი ლამბდა ტერმინი:
- თუ T არის LT და x არის არამუდმივი, მაშინ (ლამბდა xt) ეწოდება აბსტრაქცია.
- თუ T ისევე როგორც s არის ცნებები, მაშინ (TS) ეწოდება აპლიკაცია.
სხვა არაფერი არ არის ლამბდა ტერმინი. ამრიგად, კონცეფცია მოქმედებს, თუ და მხოლოდ მაშინ, თუ მისი მიღება შესაძლებელია ამ სამი წესის განმეორებით გამოყენებით. თუმცა, ზოგიერთი ფრჩხილები შეიძლება გამოტოვდეს სხვა კრიტერიუმების მიხედვით.
განმარტება
ლამბდა გამონათქვამები შედგება:
- ცვლადები v 1, v 2, …, v n, …
- აბსტრაქციის სიმბოლოები 'λ' და წერტილი '.'
- ფრჩხილები ().
L ნაკრები შეიძლება განისაზღვროს ინდუქციურად:
- თუ 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 არის ბეტა რედექსი გამოსახულებაში N x-ით ჩანაცვლების გამოსახულებაში M-ში. კომპონენტს, რომელსაც რედექსი მცირდება, ეწოდება მისი რედუქცია. შემცირება (λ x. M) N არის M [x:=N].
თუ x არ არის თავისუფალი M-ში, λ x. M x ასევე em-REDEX რეგულატორით M.
ა-ტრანსფორმაცია
ალფა გადარქმევა საშუალებას გაძლევთ შეცვალოთ შეკრული ცვლადების სახელები. მაგალითად, x. x-ს შეუძლია მისცეს λ y. წ. ტერმინები, რომლებიც განსხვავდებიან მხოლოდ ალფა ტრანსფორმაციით, ითვლება α-ეკვივალენტად. ხშირად, ლამბდა კალკულუსის გამოყენებისას, α-ეკვივალენტები განიხილება ორმხრივად.
ალფა კონვერტაციის ზუსტი წესები არ არის სრულიად ტრივიალური. პირველ რიგში, ამ აბსტრაქციის საშუალებით, მხოლოდ იმ ცვლადებს, რომლებიც დაკავშირებულია იმავე სისტემასთან, ერქმევა სახელი. მაგალითად, ალფა გარდაქმნა λ x.λ x. x შეიძლება გამოიწვიოს λ y.λ x. x, მაგრამ ამან შეიძლება არ გამოიწვიოს λy.λx.y ამ უკანასკნელს ორიგინალთან შედარებით განსხვავებული მნიშვნელობა აქვს. ეს ცვლადი დაჩრდილვის პროგრამირების კონცეფციის ანალოგია.
მეორე, ალფა ტრანსფორმაცია შეუძლებელია, თუ ეს გამოიწვევს სხვა არამუდმივ აბსტრაქციას. მაგალითად, თუ x შეცვლით y-ით λ x.λ y. x, მაშინ შეგიძლიათ მიიღოთλy.λy. u, რაც სულაც არ არის იგივე.
პროგრამირების ენებში სტატიკური მასშტაბით, ალფა კონვერტაცია შეიძლება გამოყენებულ იქნას სახელის რეზოლუციის გასამარტივებლად. ამავდროულად, იზრუნეთ იმაზე, რომ ცვლადის კონცეფცია არ ფარავდეს აღნიშვნას შემცველ ზონაში.
დე ბრუინის ინდექსის აღნიშვნაში, ნებისმიერი ორი ალფა-ეკვივალენტური ტერმინი სინტაქსურად იდენტურია.
ჩანაცვლება
E-ს მიერ დაწერილი ცვლილებები [V:=R] არის V ცვლადის ყველა თავისუფალი მოვლენის ჩანაცვლების პროცესი E გამოსახულებაში R ბრუნვით 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-ს N-ში M-ის წარმოსაჩენად, შეგიძლიათ თქვათ
(λ f. N) M.
ავტორები ხშირად შემოგვთავაზებენ სინტაქსურ კონცეფციას, როგორიცაა ნება, რათა საგნები უფრო ინტუიციურად დაიწეროს.
f=M-დან N-მდე
ასეთი განმარტებების მიჯაჭვით, შეიძლება დაწეროთ ლამბდა გამოთვლების "პროგრამა", როგორც ნული ან მეტი ფუნქციის განსაზღვრება, რასაც მოჰყვება ერთი ლამბდა წევრი, იმ განმარტებების გამოყენებით, რომლებიც ქმნიან პროგრამის ძირითად ნაწილს.
ამის შესამჩნევი შეზღუდვა არის ის, რომ სახელი f არ არის განსაზღვრული M-ში,ვინაიდან M სცილდება ლამბდა აბსტრაქციის სავალდებულო სფეროს f. ეს ნიშნავს, რომ რეკურსიული ფუნქციის ატრიბუტი არ შეიძლება გამოყენებულ იქნას როგორც M let-ით. უფრო მოწინავე letrec სინტაქსი, რომელიც საშუალებას გაძლევთ დაწეროთ რეკურსიული ფუნქციების განმარტებები ამ სტილში, დამატებით იყენებს ფიქსირებული წერტილის კომბინატორებს.
ნაბეჭდი ანალოგები
ეს ტიპი არის აკრეფილი ფორმალიზმი, რომელიც იყენებს სიმბოლოს ანონიმური ფუნქციის აბსტრაქციის წარმოსაჩენად. ამ კონტექსტში, ტიპები, როგორც წესი, სინტაქსური ხასიათის ობიექტებია, რომლებიც ენიჭება ლამბდა ტერმინებს. ზუსტი ბუნება დამოკიდებულია განსახილველ კალკულუსზე. გარკვეული თვალსაზრისით, აკრეფილი LI შეიძლება ჩაითვალოს არატიპური LI-ის დახვეწად. მაგრამ მეორე მხრივ, ისინი ასევე შეიძლება ჩაითვალოს უფრო ფუნდამენტურ თეორიად და დაუტიპებელი ლამბდა გამოთვლა განსაკუთრებული შემთხვევაა მხოლოდ ერთი ტიპისთვის.
Typed LI არის პროგრამირების ენების საფუძველი და ფუნქციური ენების ხერხემალი, როგორიცაა ML და Haskell. და, უფრო ირიბად, შექმნის იმპერატიული სტილები. აკრეფილი ლამბდა კალკულები მნიშვნელოვან როლს თამაშობს პროგრამირების ენებისთვის ტიპის სისტემების შემუშავებაში. აქ ტიპაჟი ჩვეულებრივ ასახავს პროგრამის სასურველ თვისებებს, მაგალითად, ეს არ გამოიწვევს მეხსიერების წვდომის დარღვევას.
ტიპირებული ლამბდა გამოთვლები მჭიდროდ არის დაკავშირებული მათემატიკურ ლოგიკასთან და მტკიცებულებათა თეორიასთან Curry-Howard იზომორფიზმის მეშვეობით და შეიძლება ჩაითვალოს, როგორც კატეგორიის კლასების შიდა ენა, მაგალითად, რომელიცუბრალოდ დეკარტისეული დახურვის სტილია.
