แคลคูลัสแลมบ์ดาเป็นระบบที่เป็นทางการในตรรกะทางคณิตศาสตร์สำหรับการแสดงการคำนวณตามนามธรรมและการใช้ฟังก์ชันโดยใช้การผูกและการแทนที่ตัวแปร นี่คือรุ่นสากลที่สามารถนำไปใช้กับการออกแบบของเครื่องจักรทัวริงใดๆ แคลคูลัสแลมบ์ดาถูกนำมาใช้ครั้งแรกโดยคริสตจักร ซึ่งเป็นนักคณิตศาสตร์ที่มีชื่อเสียงในช่วงทศวรรษที่ 1930
ระบบประกอบด้วยการสร้างสมาชิกแลมบ์ดาและดำเนินการลดจำนวนสมาชิก
คำอธิบายและการใช้งาน
อักษรกรีก lambda (λ) ใช้ในนิพจน์แลมบ์ดาและพจน์แลมบ์ดาเพื่อแสดงถึงการเชื่อมโยงของตัวแปรในฟังก์ชัน
แคลคูลัสแลมบ์ดาไม่พิมพ์หรือพิมพ์ ในตัวแปรแรก ฟังก์ชันสามารถใช้ได้เฉพาะเมื่อฟังก์ชันเหล่านี้สามารถรับข้อมูลประเภทนี้ได้ แคลคูลัสแลมบ์ดาที่พิมพ์จะอ่อนกว่า สามารถแสดงค่าที่น้อยกว่าได้ แต่ในทางกลับกัน มันยอมให้คุณพิสูจน์อะไรหลายๆ อย่าง
เหตุผลหนึ่งที่มีหลายประเภทที่แตกต่างกันคือความปรารถนาของนักวิทยาศาสตร์ที่จะทำมากขึ้นโดยไม่สูญเสียโอกาสที่จะพิสูจน์ทฤษฎีบทแคลคูลัสแลมบ์ดาที่แข็งแกร่ง
ระบบมีการใช้งานในด้านต่างๆ มากมาย เช่น คณิตศาสตร์ ปรัชญา ภาษาศาสตร์ และวิทยาการคอมพิวเตอร์ ประการแรก แคลคูลัสแลมบ์ดาเป็นแคลคูลัสที่มีบทบาทสำคัญในการพัฒนาทฤษฎีภาษาโปรแกรม เป็นรูปแบบของการสร้างฟังก์ชันที่ระบบนำไปใช้ พวกเขายังเป็นหัวข้อวิจัยยอดนิยมในทฤษฎีของหมวดหมู่เหล่านี้
สำหรับหุ่น
แคลคูลัสแลมบ์ดาได้รับการแนะนำโดยนักคณิตศาสตร์ Alonzo Church ในช่วงทศวรรษที่ 1930 โดยเป็นส่วนหนึ่งของการวิจัยของเขาเกี่ยวกับรากฐานของวิทยาศาสตร์ ระบบเดิมแสดงให้เห็นว่าไม่สอดคล้องกันในเชิงตรรกะในปี 1935 เมื่อ Stephen Kleen และ J. B. Rosser พัฒนาความขัดแย้งของ Kleene-Rosser
ต่อมาในปี 1936 คริสตจักรได้แยกแยะและตีพิมพ์เฉพาะส่วนที่เกี่ยวข้องกับการคำนวณ ซึ่งปัจจุบันเรียกว่าแคลคูลัสแลมบ์ดาที่ไม่ได้พิมพ์ ในปีพ.ศ. 2483 เขายังแนะนำทฤษฎีที่อ่อนแอกว่าแต่มีความสอดคล้องทางตรรกะที่เรียกว่าระบบประเภทเฉพาะ ในงานของเขา เขาอธิบายทฤษฎีทั้งหมดด้วยคำง่ายๆ ดังนั้นจึงอาจกล่าวได้ว่า Church ได้ตีพิมพ์แคลคูลัสแลมบ์ดาสำหรับหุ่น
จนถึงปี 1960 เมื่อความสัมพันธ์กับภาษาโปรแกรมชัดเจน λ เป็นเพียงรูปแบบที่เป็นทางการเท่านั้น ต้องขอบคุณการใช้งานของ Richard Montagu และนักภาษาศาสตร์คนอื่นๆ ในความหมายของภาษาธรรมชาติ แคลคูลัสจึงมีความภาคภูมิใจทั้งในด้านภาษาศาสตร์และวิทยาการคอมพิวเตอร์
ที่มาของสัญลักษณ์
Lambda ไม่ได้ยืนสำหรับคำหรือตัวย่อ แต่มาจากการอ้างอิงใน Principal Mathematics ของ Russell ตามด้วยการเปลี่ยนแปลงการพิมพ์สองครั้ง ตัวอย่างสัญกรณ์: สำหรับฟังก์ชัน f ที่มี f (y)=2y + 1 คือ 2ŷ + 1 และที่นี่เราใช้คาเร็ต (“hat”) ทับ y เพื่อติดป้ายกำกับตัวแปรอินพุต
เดิมทีโบสถ์ตั้งใจจะใช้สัญลักษณ์ที่คล้ายกัน แต่ตัวเรียงพิมพ์ไม่สามารถวางสัญลักษณ์ "หมวก" ไว้เหนือตัวอักษรได้ ดังนั้นแทนที่จะพิมพ์เป็น "/\y.2y+1" ในตอนต่อไปของการแก้ไข คนพิมพ์ดีดแทนที่ "/ \" ด้วยอักขระที่มองเห็นได้คล้ายกัน
แนะนำแคลคูลัสแลมบ์ดา
ระบบประกอบด้วยภาษาของคำ ซึ่งถูกเลือกโดยไวยากรณ์ที่เป็นทางการ และชุดของกฎการแปลงที่อนุญาตให้จัดการได้ จุดสุดท้ายถือได้ว่าเป็นทฤษฎีสมการหรือเป็นคำจำกัดความในการปฏิบัติงาน
ฟังก์ชันทั้งหมดในแคลคูลัสแลมบ์ดาไม่ระบุชื่อ หมายความว่าไม่มีชื่อ พวกเขาใช้ตัวแปรอินพุตเพียงตัวเดียว และการใช้ currying เพื่อใช้แปลงที่มีหลายตัวแปร
เงื่อนไขแลมบ์ดา
ไวยากรณ์แคลคูลัสกำหนดนิพจน์บางนิพจน์ว่าถูกต้องและอื่น ๆ ไม่ถูกต้อง เช่นเดียวกับสตริงอักขระที่แตกต่างกันเป็นโปรแกรม C ที่ถูกต้องและบางโปรแกรมไม่ใช่ นิพจน์ที่แท้จริงของแคลคูลัสแลมบ์ดาเรียกว่า "เทอมแลมบ์ดา"
กฎสามข้อต่อไปนี้ให้คำจำกัดความอุปนัยที่สามารถเป็นได้นำไปใช้กับการสร้างแนวคิดที่ถูกต้องตามวากยสัมพันธ์ทั้งหมด:
ตัวแปร x เป็นพจน์แลมบ์ดาที่ถูกต้อง:
- ถ้า T คือ LT และ x ไม่คงที่ ดังนั้น (แลมบ์ดา 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.
ตัวแปรอิสระและผูกมัด
ตัวดำเนินการ λ เชื่อมต่อแบบไม่คงที่ไม่ว่ามันจะอยู่ที่ใดในร่างของนามธรรม ตัวแปรที่อยู่ในขอบเขตเรียกว่า bound ในนิพจน์ λ 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).
สูตรที่ไม่มีตัวแปรอิสระเรียกว่าปิด นิพจน์แลมบ์ดาปิดเรียกอีกอย่างว่าคอมบิเนเตอร์และเทียบเท่ากับเงื่อนไขในลอจิกแบบรวม
ตัวย่อ
ความหมายของนิพจน์แลมบ์ดาถูกกำหนดโดยวิธีย่อ
การตัดมีสามประเภท:
- α-transform: การเปลี่ยนตัวแปรที่ถูกผูกไว้ (alpha).
- β-reduction: การใช้ฟังก์ชันกับอาร์กิวเมนต์ (เบต้า)
- η-transform: ครอบคลุมแนวคิดของการขยาย
นี่ก็เช่นกันเรากำลังพูดถึงผลลัพธ์ที่เทียบเท่ากัน: นิพจน์สองนิพจน์เทียบเท่า β หากสามารถแปลงเป็นองค์ประกอบเดียวกันได้ β และ α / η-equivalence ถูกกำหนดในทำนองเดียวกัน
คำว่า redex ย่อมาจาก reducible turnover หมายถึงหัวข้อย่อยที่สามารถลดได้ตามกฎข้อใดข้อหนึ่ง แคลคูลัสแลมบ์ดาสำหรับหุ่นจำลอง ตัวอย่าง:
(λ x. M) N คือ beta redex ในนิพจน์สำหรับการแทนที่ N ด้วย x ใน M องค์ประกอบที่ redex ลดลงเรียกว่า reduct การลดลง (λ x. M) N คือ M [x:=N].
ถ้า x ไม่ว่างใน M, λ x M x ยัง em-REDEX พร้อมตัวควบคุม M.
α-การแปลง
Alpha เปลี่ยนชื่อทำให้คุณสามารถเปลี่ยนชื่อของตัวแปรที่ถูกผูกไว้ได้ ตัวอย่างเช่น x x สามารถให้ λ y ย. คำศัพท์ที่แตกต่างกันในการแปลงอัลฟาเท่านั้นเรียกว่าเทียบเท่า α บ่อยครั้งเมื่อใช้แคลคูลัสแลมบ์ดา ค่าเทียบเท่า α จะถือเป็นส่วนกลับกัน
กฎที่แน่นอนสำหรับการแปลงอัลฟ่าไม่ใช่เรื่องเล็กน้อย ประการแรก ด้วยสิ่งที่เป็นนามธรรมนี้ เฉพาะตัวแปรที่เกี่ยวข้องกับระบบเดียวกันเท่านั้นที่จะถูกเปลี่ยนชื่อ ตัวอย่างเช่น การแปลงอัลฟา λ x.λ x x สามารถนำไปสู่ λ y.λ x x แต่อาจไม่นำไปสู่ λy.λx.y ความหมายหลังมีความหมายที่ต่างไปจากเดิม ซึ่งคล้ายกับแนวคิดของการเขียนโปรแกรมแชโดว์ตัวแปร
ประการที่สอง การแปลงอัลฟาเป็นไปไม่ได้หากจะส่งผลให้ถูกนามธรรมอื่นๆ ที่ไม่ถาวรจับ ตัวอย่างเช่น หากคุณแทนที่ x ด้วย y ใน λ x.λ y x จากนั้นคุณจะได้รับล.ล. u ซึ่งไม่เหมือนกันเลย
ในภาษาโปรแกรมที่มีขอบเขตคงที่ สามารถใช้การแปลงอัลฟ่าเพื่อทำให้การจำแนกชื่อง่ายขึ้น ในขณะเดียวกัน การดูแลไม่ให้แนวคิดของตัวแปรปิดบังการกำหนดในพื้นที่บรรจุ
ในสัญกรณ์ดัชนี De Bruyne คำสองคำที่เทียบเท่าอัลฟ่าจะเหมือนกันทางวากยสัมพันธ์
เปลี่ยน
การเปลี่ยนแปลงที่เขียนโดย E [V:=R] เป็นกระบวนการแทนที่การเกิดขึ้นของตัวแปร V อิสระทั้งหมดในนิพจน์ E ด้วยการหมุนเวียน 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) สูงถึง α-equivalence โปรดทราบว่าการแทนที่ถูกกำหนดไว้เฉพาะสำหรับแลมบ์ดา
ลดเบต้า
การลดเบต้าสะท้อนแนวคิดในการใช้ฟังก์ชัน Beta-reductive ถูกกำหนดไว้ในเงื่อนไขทดแทน: ((X V. E) E ') คือ E [V:=E'].
ตัวอย่างเช่น สมมติว่าการเข้ารหัส 2, 7, × มีการลดค่า β ดังต่อไปนี้: ((λ n. N × 2) 7) → 7 × 2
การลดเบต้าสามารถเห็นได้เช่นเดียวกับแนวคิดของการลดปริมาณการใช้ในพื้นที่ภายใต้การหักตามธรรมชาติผ่านไอโซมอร์ฟิซึมของแกง-โฮเวิร์ด
η-transform
การแปลงนี้เป็นการแสดงออกถึงแนวคิดเรื่องการขยายขอบเขต ซึ่งในบริบทนี้คือฟังก์ชันสองหน้าที่เท่ากันเมื่อให้ผลลัพธ์ที่เหมือนกันสำหรับอาร์กิวเมนต์ทั้งหมด การแปลงนี้ทำการแลกเปลี่ยนระหว่าง λ x (F x) และ f เมื่อใดก็ตามที่ x ดูเหมือนไม่ว่างใน f.
การกระทำนี้ถือได้ว่าเหมือนกับแนวคิดของความสมบูรณ์ของท้องถิ่นในการหักตามธรรมชาติผ่าน isomorphism ของ Curry-Howard
รูปแบบปกติและฟิวชั่น
สำหรับแคลคูลัสแลมบ์ดาที่ไม่ได้พิมพ์ กฎการลด β โดยทั่วไปจะไม่ทำให้ค่าปกติแข็งแกร่งหรืออ่อนลง
อย่างไรก็ตาม จะเห็นได้ว่าการลด β ผสานกันเมื่อทำงานก่อนการแปลง α (กล่าวคือ รูปแบบปกติสองรูปแบบสามารถถือได้ว่าเท่ากันหากการแปลง α จากอันหนึ่งเป็นอีกอันหนึ่งเป็นไปได้)
ดังนั้น ทั้งเงื่อนไขการทำให้เป็นมาตรฐานอย่างเข้มงวดและข้อกำหนดที่ปรับเล็กน้อยจึงมีรูปแบบปกติเพียงรูปแบบเดียว สำหรับเงื่อนไขแรก กลยุทธ์การลดใดๆ รับประกันว่าจะส่งผลให้เกิดการกำหนดค่าทั่วไป ในขณะที่สภาวะปกติเล็กน้อย กลยุทธ์การลดบางอย่างอาจไม่พบ
วิธีการตั้งโปรแกรมเพิ่มเติม
แคลคูลัสแลมบ์ดามีสำนวนการสร้างสรรค์มากมาย เดิมจำนวนมากได้รับการพัฒนาในบริบทของการใช้ระบบเป็นพื้นฐานสำหรับความหมายของภาษาโปรแกรม โดยนำไปใช้เป็นโครงสร้างระดับต่ำได้อย่างมีประสิทธิภาพ เนื่องจากบางรูปแบบมีแคลคูลัสแลมบ์ดา (หรือบางอย่างที่คล้ายกันมาก) เป็นตัวอย่าง เทคนิคเหล่านี้จึงพบการใช้งานจริงในการสร้างสรรค์ แต่อาจถูกมองว่าคลุมเครือหรือแปลกปลอม
ชื่อคงที่
ในแคลคูลัสแลมบ์ดา ไลบรารี่จะอยู่ในรูปแบบของชุดของฟังก์ชันที่กำหนดไว้ก่อนหน้านี้ โดยที่เงื่อนไขเป็นเพียงค่าคงที่ที่เป็นรูปธรรม แคลคูลัสบริสุทธิ์ไม่มีแนวคิดเรื่องความไม่เปลี่ยนรูปแบบที่มีชื่อเนื่องจากเงื่อนไขแลมบ์ดาอะตอมทั้งหมดเป็นตัวแปร แต่พวกมันยังสามารถเลียนแบบได้ด้วยการนำ mutable เป็นชื่อของค่าคงที่ โดยใช้ lambda abstraction เพื่อผูกกับสารระเหยนั้นในร่างกาย และใช้สิ่งที่เป็นนามธรรมนั้นกับคำจำกัดความที่ตั้งใจไว้ ดังนั้น ถ้าคุณใช้ f แทน M ใน N คุณสามารถพูดว่า
(λ f. N) M.
ผู้เขียนมักจะแนะนำแนวคิดเชิงวากยสัมพันธ์ เช่น ปล่อยให้เขียนสิ่งต่าง ๆ ในลักษณะที่เป็นธรรมชาติมากขึ้น
f=M ถึง N
โดยเชื่อมโยงคำจำกัดความดังกล่าว เราสามารถเขียน "โปรแกรม" แคลคูลัสแลมบ์ดาเป็นศูนย์หรือคำจำกัดความของฟังก์ชันมากกว่านั้นตามด้วยสมาชิกแลมบ์ดาตัวเดียว โดยใช้คำจำกัดความเหล่านั้นที่ประกอบขึ้นเป็นกลุ่มของโปรแกรม
ข้อจำกัดที่น่าสังเกตของ let นี้คือชื่อ f ไม่ได้กำหนดไว้ใน M,เนื่องจาก M อยู่นอกขอบเขตการจับของสิ่งที่เป็นนามธรรมของแลมบ์ดา f ซึ่งหมายความว่าแอตทริบิวต์ฟังก์ชันแบบเรียกซ้ำไม่สามารถใช้เป็น M ด้วยให้ ไวยากรณ์ letrec ขั้นสูง ซึ่งช่วยให้คุณเขียนคำจำกัดความของฟังก์ชันแบบเรียกซ้ำในรูปแบบนี้ ยังใช้ตัวรวมจุดคงที่แทน
พิมพ์แอนะล็อก
ประเภทนี้เป็นรูปแบบการพิมพ์ที่ใช้สัญลักษณ์แทนฟังก์ชันนามธรรมที่ไม่ระบุชื่อ ในบริบทนี้ ประเภทมักจะเป็นอ็อบเจ็กต์ที่มีลักษณะวากยสัมพันธ์ที่กำหนดให้กับเงื่อนไขแลมบ์ดา ลักษณะที่แน่นอนขึ้นอยู่กับแคลคูลัสที่เป็นปัญหา จากมุมมองหนึ่ง การพิมพ์ LI ถือได้ว่าเป็นการปรับแต่ง LI ที่ไม่ได้พิมพ์ แต่ในทางกลับกัน พวกมันสามารถถือเป็นทฤษฎีพื้นฐานที่มากกว่า และแคลคูลัสแลมบ์ดาที่ไม่ได้พิมพ์นั้นเป็นกรณีพิเศษที่มีเพียงประเภทเดียวเท่านั้น
พิมพ์ LI เป็นพื้นฐานของภาษาโปรแกรมและเป็นแกนหลักของภาษาที่ใช้งานได้ เช่น ML และ Haskell และโดยอ้อมมากขึ้น รูปแบบการสร้างสรรค์ที่จำเป็น แคลคูลัสแลมบ์ดาที่พิมพ์มีบทบาทสำคัญในการพัฒนาระบบการพิมพ์สำหรับภาษาโปรแกรม ในที่นี้ ความสามารถในการพิมพ์มักจะจับคุณสมบัติที่ต้องการของโปรแกรม เช่น จะไม่ทำให้เกิดการละเมิดการเข้าถึงหน่วยความจำ
แคลคูลัสแลมบ์ดาที่พิมพ์มีความเกี่ยวข้องอย่างใกล้ชิดกับตรรกะทางคณิตศาสตร์และทฤษฎีการพิสูจน์ผ่านไอโซมอร์ฟิซึมของเคอร์รี–โฮเวิร์ด และสามารถคิดได้ว่าเป็นภาษาภายในของคลาสหมวดหมู่ เป็นต้นมันคือสไตล์ของคาร์ทีเซียนปิด
