แคลคูลัสแลมบ์ดา

แคลคูลัสแลมบ์ดา (หรือ λ-calculus) เป็นระบบรูปนัยในคณิตตรรกศาสตร์ที่ใช้ในการคำนวณ พื้นฐานของระบบประกอบไปด้วยการสร้างฟังก์ชันและการเรียกใช้ฟังก์ชันโดยใช้การโยงของตัวแปรและการแทนที่ตัวแปร นักคณิตศาสตร์อลอนโซ เชิร์ชได้คิดค้นแคลคูลัสแลมบ์ดาขึ้นมาในช่วงปี 1930 เพื่อสำรวจหารากฐานของคณิตศาสตร์ แคลคูลัสแลมบ์ดาเป็นแบบจำลองสากลในการคำนวณเทียบเท่ากับเครื่องจักรทัวริง (ความเท่าเทียมกันของาองระบบทั้งสองรู้จักได้รับการพิสูจน์ในแนวคิดหลักของเชิร์ช–ทัวริงในปี 1937) คำว่า "แลมบ์ดา" ซึ่งเป็นอักขระกรีก (λ) ปรากฏในพจน์แลมบ์ดา (หรืออาจจะเรียกว่านิพจน์แลมบ์ดา) ซึ่งใช้ในการแสดงถึงการโยงตัวแปรในฟังก์ชัน

แคลคูลัสแลมบ์ดามีสองรูปแบบ: แบบมีชนิดข้อมูล และ ไม่มีชนิดข้อมูล ในแคลคูลัสแลมบ์ดาที่มีชนิดข้อมูล ฟังก์ชันสามารถเรียกใช้ได้เมื่อชนิดของฟังก์ชันสอดคล้องกับชนิดของข้อมูลนำเข้าของฟังก์ชันเท่านั้น

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

แคลคูลัสแลมบ์ดาในประวัติศาสตร์ของคณิตศาสตร์

นักคณิตศาสตร์อลอนโซ เชิร์ช ได้คิดค้นแคลคูลัสแลมบ์ดาขึ้นมาในช่วงปี 1930 เพื่อสำรวจหารากฐานของคณิตศาสตร์ ในปี 1935 Stephen Kleene และ J. B. Rosser ได้ค้นพบ Kleene–Rosser paradox ซึ่งแสดงให้เห็นว่าระบบเดิมของแคลคูลัสแลมบ์ดามี

ต่อมาในปี 1936 เชิร์ชแยกเฉพาะส่วนที่เกี่ยวข้องกับการคำนวณในระบบเดิมออกมา และจัดพิมพ์เฉพาะส่วนดังกล่าว ซึ่งในปัจจุบันเรียกกันว่าแคลคูลัสแลมบ์ดาแบบไม่มีชนิดข้อมูล ในปี 1940 เชิร์ชยังได้สร้างแคลคูลัสแลมบ์ดาแบบมีชนิดข้อมูลอย่างง่าย ซึ่งระบบที่ไม่ทรงพลังในเชิงการคำนวณเท่าแบบไม่มีชนิดข้อมูล แต่ระบบนี้สอดคล้องกันในเชิงตรรกศาสตร์

ก่อนช่วงปี 1960 แคลคูลัสแลมบ์ดาเป็นเพียงแค่เท่านั้น แต่ในช่วงปี 1960 ความสัมพันธ์ระหว่างแคลคูลัสแลมบ์ดาและภาษาโปรแกรมก็เป็นที่ชัดเจน แคลคูลัสแลมบ์ดายังเริ่มมีความสำคัญในภาษาศาสตร์ (ดูที่ Heim and Kratzer 1998) จากการประยุกต์ระบบในอรรถศาสตร์ของภาษาธรรมชาติโดย  และนักภาษาศาสตร์อื่น ๆ ในช่วงเวลาเดียวกันแคลคูลัสแลมบ์ดายังเริ่มมีความสำคัญในวิทยาการคอมพิวเตอร์

คำอธิบายอย่างไม่เป็นทางการ

แรงจูงใจ

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

${\displaystyle \operatorname {square\_sum} (x,y)=x\times x+y\times y}$

สามารถเขียนใหม่ในรูปแบบนิรนามว่า

${\displaystyle (x,y)\mapsto x\times x+y\times y}$

(ความหมายคือ "คู่อันดับ x และ y ไปยัง ${\textstyle x\times x+y\times y}$") อีกตัวอย่างคือ

${\displaystyle \operatorname {id} (x)=x}$

สามารถเขียนใหม่ในรูปแบบนิรนามว่า ${\textstyle x\mapsto x}$, นั่นคือ ข้อมูลนำเข้าของฟังก์ชันถูกส่งไปยังตัวเอง

ประการที่สอง แคลคูลัสแลมบ์ดาอนุญาตให้ฟังก์ชันรับข้อมูลนำเข้าเพียงแค่ตัวเดียวเท่านั้น ฟังก์ชันที่รับข้อมูลนำเข้ามากกว่าหนึ่ง เช่น ${\textstyle \operatorname {square\_sum} }$ ที่รับข้อมูลสองตัว สามารถเขียนใหม่เป็นฟังก์ชันที่รับข้อมูลตัวแรก และคืนค่าฟังก์ชันอีกอันที่รับข้อมูลตัวที่สอง ตัวอย่างเช่น

${\displaystyle (x,y)\mapsto x\times x+y\times y}$

สามารถเขียนใหม่เป็น

${\displaystyle x\mapsto (y\mapsto x\times x+y\times y)}$

วิธีนี้ซึ่งรู้จักกันในชื่อการเคอร์รี เป็นการเปลี่ยนฟังก์ชันที่รับหลายอาร์กิวเมนต์มาเป็นฟังก์ชันที่รับอาร์กิวเมนต์เดียวซ้อนกันหลาย ๆ ฟังก์ชัน

การเรียกใช้ฟังก์ชันของ ${\textstyle \operatorname {square\_sum} }$ ดั้งเดิม ด้วยข้อมูล (5, 2) ทำให้เกิดการประมวลผลดังต่อไปนี้

${\textstyle ((x,y)\mapsto x\times x+y\times y)(5,2)}$

${\textstyle =5\times 5+2\times 2}$

${\textstyle =29}$,

แต่การประมวลผลของฟังก์ชันที่เขียนใหม่ (มีการเคอร์รี) มีขั้นตอนเพิ่มขึ้นหนึ่งขั้นตอน

${\textstyle ((x\mapsto (y\mapsto x\times x+y\times y))(5))(2)}$

${\textstyle =(y\mapsto 5\times 5+y\times y)(2)}$

${\textstyle =5\times 5+2\times 2}$

${\textstyle =29}$

แต่ทั้งสองวิธีให้ผลลัพธ์เหมือนกัน

แคลคูลัสแลมบ์ดา

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

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

พจน์แลมบ์ดา

วากยสัมพันธ์ของพจน์แลมบ์ดานิยามบางนิพจน์ให้เป็น นิพนจ์แคลคูลัสแลมบ์ดาที่ถูกต้องหรือไม่ถูกต้อง นิพนจ์แคลคูลัสแลมบ์ดาที่ถูกต้องเรียกว่า "พจน์แลมบ์ดา"

กฎ 3 ประการด้านล่างเป็นนิยามเชิงอุปนัยซึ่งใช้ในการสร้างพจน์แลมบ์ดาทั้งหมดที่ถูกต้อง

• ตัวแปร ${\displaystyle x}$ เป็นพจน์แลมบ์ดา
• ถ้า ${\displaystyle t}$ เป็นพจน์แลมบ์ดา และ ${\displaystyle x}$ เป็นตัวแปร แล้วจะได้ว่า ${\displaystyle (\lambda x.t)}$ เป็นพจน์แลมบ์ดา (เรียกพจน์ดังกล่าวว่า การสร้างแลมบ์ดา หรือ lambda abstraction);
• ถ้า ${\displaystyle t}$ และ ${\displaystyle s}$ เป็นพจน์แลมบ์ดา แล้วจะได้ว่า ${\displaystyle (ts)}$ เป็นพจน์แลมบ์ดา (เรียกพจน์ดังกล่าวว่า การเรียกใช้ หรือ application).

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

การสร้างแลมบ์ดา ${\displaystyle \lambda x.t}$ เป็นการนิยามฟังก์ชันนิรนามที่สามารถรับข้อมูลนำเข้า ${\displaystyle x}$ และแทนที่ข้อมูลดังกล่าวใน นิพจน์ ${\displaystyle t}$ ดังนั้น นี่จึงเป็นการนิยามฟังก์ชันนิรนามที่รับข้อมูลนำเข้า ${\displaystyle x}$ และคืนค่า ${\displaystyle t}$ ตัวอย่างเช่น ${\displaystyle \lambda x.x^{2}+2}$ เป็นการสร้างแลมบ์ดาของฟังก์ชัน ${\displaystyle f(x)=x^{2}+2}$ โดยมีพจน์ ${\displaystyle x^{2}+2}$ เป็น ${\displaystyle t}$  นิยามของการสร้างแลมบ์ดานี้เพียงแค่ "สร้าง" ตัวฟังก์ชัน แต่ไม่ได้เรียกใช้ฟังก์ชัน การสร้างแลมบ์ดาโยงตัวแปร ${\displaystyle x}$ ในพจน์ ${\displaystyle t}$

การเรียกใช้ ${\displaystyle ts}$ เป็นการเรียกใช้ฟังก์ชัน ${\displaystyle t}$ ด้วยข้อมูลนำเข้า ${\displaystyle s}$ นั่นคือเป็นการเรียกใช้ฟังก์ชัน ${\displaystyle t}$ ด้วย ${\displaystyle s}$ เพื่อให้ค่า ${\displaystyle t(s)}$

แคลคูลัสแลมบ์ดาไม่มีแนวคิดของการประกาศตัวแปร ในพจน์เช่น ${\displaystyle \lambda x.x+y}$ (หรือ ${\displaystyle f(x)=x+y}$) แคลคูลัสแลมบ์ดานับ ${\displaystyle y}$ ว่าเป็นตัวแปรที่ยังไม่ได้รับการนิยาม การสร้างแลมบ์ดา ${\displaystyle \lambda x.x+y}$ ถูกต้องในเชิงวากยสัมพันธ์ และแสดงถึงฟังก์ชันที่บวกข้อมูลนำเข้ากับตัวแปร ${\displaystyle y}$ ซึ่งยังไม่รู้ค่า

ดูเพิ่ม

อ่านเพิ่มเติม

• Abelson, Harold & Gerald Jay Sussman. Structure and Interpretation of Computer Programs. The MIT Press. ISBN 0-262-51087-1.
• Hendrik Pieter Barendregt Introduction to Lambda Calculus.
• Henk Barendregt, The Impact of the Lambda Calculus in Logic and Computer Science 2016-02-15 ที่ เวย์แบ็กแมชชีน. The Bulletin of Symbolic Logic, Volume 3, Number 2, June 1997.
• Barendregt, Hendrik Pieter, The Type Free Lambda Calculus pp1091–1132 of Handbook of Mathematical Logic, North-Holland (1977) ISBN 0-7204-2285-X
• Cardone and Hindley, 2006. History of Lambda-calculus and Combinatory Logic 2011-10-10 ที่ เวย์แบ็กแมชชีน^{[dead link]}. In Gabbay and Woods (eds.), Handbook of the History of Logic, vol. 5. Elsevier.
• Church, Alonzo, An unsolvable problem of elementary number theory, American Journal of Mathematics, 58 (1936), pp. 345–363. This paper contains the proof that the equivalence of lambda expressions is in general not decidable.
• Alonzo Church, The Calculi of Lambda-Conversion (ISBN 978-0-691-08394-0)
• Kleene, Stephen, A theory of positive integers in formal logic, American Journal of Mathematics, 57 (1935), pp. 153–173 and 219–244. Contains the lambda calculus definitions of several familiar functions.
• Landin, Peter, A Correspondence Between ALGOL 60 and Church's Lambda-Notation, Communications of the ACM, vol. 8, no. 2 (1965), pages 89–101. Available from the ACM site. A classic paper highlighting the importance of lambda calculus as a basis for programming languages.
• Larson, Jim, An Introduction to Lambda Calculus and Scheme 2001-12-06 ที่ เวย์แบ็กแมชชีน. A gentle introduction for programmers.
• Schalk, A. and Simmons, H. (2005) An introduction to λ-calculi and arithmetic with a decent selection of exercises. Notes for a course in the Mathematical Logic MSc at Manchester University.
• de Queiroz, Ruy J.G.B. (2008) On Reduction Rules, Meaning-as-Use and Proof-Theoretic Semantics^[]. Studia Logica, 90(2):211-247. A paper giving a formal underpinning to the idea of 'meaning-is-use' which, even if based on proofs, it is different from proof-theoretic semantics as in the Dummett–Prawitz tradition since it takes reduction as the rules giving meaning.

หนังสืออ่านเรียนสำหรับนักเรียนปริญญาเอก

• Morten Heine Sørensen, Paweł Urzyczyn, Lectures on the Curry-Howard isomorphism, Elsevier, 2006, ISBN 0-444-52077-5 is a recent monograph that covers the main topics of lambda calculus from the type-free variety, to most typed lambda calculi, including more recent developments like pure type systems and the lambda cube. It does not cover subtyping extensions.
• Pierce, Benjamin (2002), Types and Programming Languages, MIT Press, ISBN  covers lambda calculi from a practical type system perspective; some topics like dependent types are only mentioned, but subtyping is an important topic.

เนื้อหาบางส่วนของบทความนี้อิงมาจากเนื้อหาจาก FOLDOC โดยได้รับการอนุญาตแล้ว

แหล่งข้อมูลอื่น

• Hazewinkel, Michiel, บ.ก. (2001), "Lambda-calculus", , , ISBN 
• Achim Jung, A Short Introduction to the Lambda Calculus-(PDF)
• Dana Scott, A timeline of lambda calculus-(PDF)
• David C. Keenan, To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction
• Raúl Rojas, A Tutorial Introduction to the Lambda Calculus-(PDF)
• Peter Selinger, Lecture Notes on the Lambda Calculus-(PDF)
• L. Allison, Some executable λ-calculus examples 2021-04-20 ที่ เวย์แบ็กแมชชีน
• Georg P. Loczewski, The Lambda Calculus and A++
• Bret Victor, Alligator Eggs: A Puzzle Game Based on Lambda Calculus
• Lambda Calculus 2012-10-14 ที่ เวย์แบ็กแมชชีน on Safalra’s Website 2021-05-02 ที่ เวย์แบ็กแมชชีน
• Lambda Calculus on PlanetMath.org.
• LCI Lambda Interpreter a simple yet powerful pure calculus interpreter
• Lambda Calculus links on Lambda-the-Ultimate
• Mike Thyer, Lambda Animator 2007-07-13 ที่ เวย์แบ็กแมชชีน, a graphical Java applet demonstrating alternative reduction strategies.
• An Introduction to Lambda Calculus and Scheme 2001-12-06 ที่ เวย์แบ็กแมชชีน, by Jim Larson
• Implementing the Lambda calculus using C++ Templates
• Marius Buliga, Graphic lambda calculus
• Lambda Calculus as a Workflow Model 2016-07-29 ที่ เวย์แบ็กแมชชีน by Peter Kelly, Paul Coddington, and Andrew Wendelborn; mentions graph reduction as a common means of evaluating lambda expressions and discusses the applicability of lambda calculus for distributed computing (due to the Church–Rosser property, which enables parallel graph reduction for lambda expressions).
• Shane Steinert-Threlkeld, "Lambda Calculi", Internet Encyclopedia of Philosophy

อ้างอิง

1. Turing, A. M. (December 1937). "Computability and λ-Definability". The Journal of Symbolic Logic. 2 (4): 153–163. doi:10.2307/2268280. JSTOR 2268280.
2. Coquand, Thierry, "Type Theory", The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed.
3. Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus - Michael Moortgat - Google Books, Books.google.co.uk, 1988-01-01, ISBN , สืบค้นเมื่อ 2013-09-15
4. Computing Meaning - Google Books, Books.google.co.uk, 2008-07-02, ISBN , สืบค้นเมื่อ 2013-09-15
5. Mitchell, John C. (2003), Concepts in Programming Languages, Cambridge University Press, p. 57, ISBN .
6. A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366 (1932).
7. For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).
8. A. Church, "An unsolvable problem of elementary number theory", American Journal of Mathematics, Volume 58, No. 2.
9. Church, A. "A Formulation of the Simple Theory of Types". Journal of Symbolic Logic. 5: 1940. doi:10.2307/2266170.
10. Alama, Jesse "The Lambda Calculus", The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed.
11. (1944). "Review: The Calculi of Lambda-Conversion by Alonzo Church" (PDF). Bull. Amer. Math. Soc. 50 (3): 169–172. doi:10.1090/s0002-9904-1944-08090-7.