แลมบ์ดาแคลคูลัสและแบบจำลองเชิงฟังก์ชัน

แลมบ์ดาแคลคูลัสเป็นระบบรูปนัยที่เรียบง่าย ซึ่งทุกสิ่งคือฟังก์ชันและการคำนวณดำเนินไปโดยการแทนที่ โดยเป็นทั้งแบบจำลองเริ่มต้นของการคำนวณที่มีประสิทธิภาพและแกนหลักทางทฤษฎีของการเขียนโปรแกรมเชิงฟังก์ชัน

Definition

แลมบ์ดาแคลคูลัสเป็นภาษาเชิงรูปนัยที่สร้างขึ้นจากตัวแปร การสร้างฟังก์ชันนามธรรม และการประยุกต์ใช้ โดยมีการคำนวณดำเนินการโดยการลดรูปเบต้า ซึ่งเป็นกฎที่ใช้ฟังก์ชันกับอาร์กิวเมนต์โดยการแทนที่ เป็นแบบจำลองสากลที่มีพลังเทียบเท่ากับเครื่องจักรทัวริง

Scope

หัวข้อนี้ครอบคลุมไวยากรณ์ของพจน์แลมบ์ดา กฎการลดรูปที่เป็นตัวขับเคลื่อนการคำนวณ คุณสมบัติการบรรจบกันของเชิร์ช-รอสเซอร์ การเข้ารหัสข้อมูลและการเรียกซ้ำผ่านตัวรวมจุดตรึง ความสมบูรณ์แบบทัวริงของแคลคูลัส และรูปแบบที่มีชนิดข้อมูลที่เชื่อมโยงการคำนวณเข้ากับตรรกะ

Core questions

• การคำนวณสามารถแสดงออกได้อย่างไรโดยใช้เพียงฟังก์ชันและการแทนที่เท่านั้น?
• เหตุใดลำดับของการลดรูปจึงไม่เปลี่ยนแปลงผลลัพธ์สุดท้าย?
• ตัวเลข ข้อมูล และการเรียกซ้ำถูกนำเสนอด้วยฟังก์ชันล้วนๆ ได้อย่างไร?
• แลมบ์ดาแคลคูลัสแบบมีชนิดข้อมูลเชื่อมโยงการคำนวณเข้ากับการพิสูจน์เชิงตรรกะได้อย่างไร?

Key theories

ทฤษฎีบทเชิร์ช-รอสเซอร์

หากพจน์แลมบ์ดาสามารถลดรูปได้หลายวิธี ผลลัพธ์สามารถนำกลับมารวมกันได้เสมอ ดังนั้นทุกพจน์จึงมีรูปแบบปกติได้มากที่สุดหนึ่งรูปแบบ และแคลคูลัสจึงบรรจบกันและมีความหมายที่ดีในฐานะแบบจำลองของการคำนวณ

ความสมบูรณ์แบบทัวริงและจุดตรึง

ตัวรวมจุดตรึงแสดงการเรียกซ้ำแบบใดก็ได้ ทำให้แลมบ์ดาแคลคูลัสแบบไม่มีชนิดข้อมูลสามารถคำนวณฟังก์ชันที่สามารถคำนวณได้ด้วยเครื่องจักรทัวริงทุกฟังก์ชัน และดังนั้นจึงเป็นแบบจำลองการคำนวณที่สมบูรณ์

การติดต่อแบบเคอร์รี-ฮาวเวิร์ด

แลมบ์ดาแคลคูลัสแบบมีชนิดข้อมูลสอดคล้องกับระบบตรรกะ โดยมีชนิดข้อมูลเป็นประพจน์และโปรแกรมเป็นข้อพิสูจน์ ซึ่งเชื่อมโยงการคำนวณโดยตรงกับตรรกะเชิงสร้างสรรค์และเป็นรากฐานของโปรแกรมช่วยพิสูจน์

Clinical relevance

แลมบ์ดาแคลคูลัสเป็นรากฐานของภาษาโปรแกรมเชิงฟังก์ชัน เช่น Lisp, Haskell และ ML ของระบบชนิดข้อมูลที่ตรวจจับข้อผิดพลาดในภาษาโปรแกรมสมัยใหม่ และของโปรแกรมช่วยพิสูจน์ที่การติดต่อแบบเคอร์รี-ฮาวเวิร์ดช่วยให้โปรแกรมและข้อพิสูจน์ทางคณิตศาสตร์สามารถตรวจสอบได้ด้วยกลไกเดียวกัน

History

เชิร์ชได้นำเสนอแลมบ์ดาแคลคูลัสในช่วงทศวรรษ 1930 เพื่อเป็นรากฐานสำหรับตรรกะและการคำนวณ และร่วมกับรอสเซอร์ได้พิสูจน์การบรรจบกันของมัน แม้ว่าระบบตรรกะดั้งเดิมจะไม่สอดคล้องกัน แต่แกนหลักของการคำนวณก็เจริญรุ่งเรือง และตั้งแต่ทศวรรษ 1960 เป็นต้นมา มันได้กำหนดรูปแบบการเขียนโปรแกรมเชิงฟังก์ชัน และผ่านการติดต่อแบบเคอร์รี-ฮาวเวิร์ด ความเชื่อมโยงระหว่างข้อพิสูจน์และโปรแกรม

Key figures

• Alonzo Church
• Haskell Curry
• J. Barkley Rosser
• William Alvin Howard

Seminal works

• church1936
• barendregt1984

Frequently asked questions

ระบบที่มีเพียงฟังก์ชันสามารถคำนวณด้วยตัวเลขได้อย่างไร?

ตัวเลขถูกเข้ารหัสเป็นฟังก์ชัน ตัวอย่างเช่น ตัวเลขเชิร์ชที่แสดงจำนวนครั้งที่การดำเนินการที่กำหนดถูกนำไปใช้ เลขคณิต บูลีน คู่ และโครงสร้างข้อมูลทั้งหมดมีการเข้ารหัสเชิงฟังก์ชัน ดังนั้นแคลคูลัสจึงไม่จำเป็นต้องมีชนิดข้อมูลในตัว แต่สามารถแสดงการคำนวณใดๆ ได้

ความเชื่อมโยงระหว่างแลมบ์ดาแคลคูลัสกับการเขียนโปรแกรมคืออะไร?

ภาษาเชิงฟังก์ชันโดยพื้นฐานแล้วคือแลมบ์ดาแคลคูลัสที่ขยายออกไป: แกนหลักของมันคือฟังก์ชัน การประยุกต์ใช้ และการแทนที่ แคลคูลัสยังให้ทฤษฎีชนิดข้อมูลที่ภาษาโปรแกรมสมัยใหม่ใช้เพื่อความปลอดภัย และผ่านการติดต่อแบบเคอร์รี-ฮาวเวิร์ด มันเชื่อมโยงโปรแกรมที่มีชนิดข้อมูลที่ถูกต้องเข้ากับข้อพิสูจน์เชิงตรรกะ