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

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

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

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

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

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

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

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

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

แรงจูงใจ

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

$\mathrm{s}\mathrm{q}\mathrm{u}\mathrm{a}\mathrm{r}\mathrm{e}\mathrm{\_}\mathrm{s}\mathrm{u}\mathrm{m}(x,y)=x\times x+y\times y$

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

$(x,y)\mapsto x\times x+y\times y$

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

$\mathrm{id}(x)=x$

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

ประการที่สอง แคลคูลัสแลมบ์ดาอนุญาตให้ฟังก์ชันรับข้อมูลนำเข้าเพียงแค่ตัวเดียวเท่านั้น ฟังก์ชันที่รับข้อมูลนำเข้ามากกว่าหนึ่ง เช่น $\mathrm{s}\mathrm{q}\mathrm{u}\mathrm{a}\mathrm{r}\mathrm{e}\mathrm{\_}\mathrm{s}\mathrm{u}\mathrm{m}$ ที่รับข้อมูลสองตัว สามารถเขียนใหม่เป็นฟังก์ชันที่รับข้อมูลตัวแรก และคืนค่าฟังก์ชันอีกอันที่รับข้อมูลตัวที่สอง ตัวอย่างเช่น

$(x,y)\mapsto x\times x+y\times y$

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

$x\mapsto (y\mapsto x\times x+y\times y)$

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

การเรียกใช้ฟังก์ชันของ $\mathrm{s}\mathrm{q}\mathrm{u}\mathrm{a}\mathrm{r}\mathrm{e}\mathrm{\_}\mathrm{s}\mathrm{u}\mathrm{m}$ ดั้งเดิม ด้วยข้อมูล (5, 2) ทำให้เกิดการประมวลผลดังต่อไปนี้

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

$=5\times 5+2\times 2$

$=29$,

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

$((x\mapsto (y\mapsto x\times x+y\times y))(5))(2)$

$=(y\mapsto 5\times 5+y\times y)(2)$

$=5\times 5+2\times 2$

$=29$

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

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

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

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

พจน์แลมบ์ดา

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

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

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

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

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

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

แคลคูลัสแลมบ์ดาไม่มีแนวคิดของการประกาศตัวแปร ในพจน์เช่น $\lambda x.x+y$ (หรือ $f(x)=x+y$) แคลคูลัสแลมบ์ดานับ $y$ ว่าเป็นตัวแปรที่ยังไม่ได้รับการนิยาม การสร้างแลมบ์ดา $\lambda x.x+y$ ถูกต้องในเชิงวากยสัมพันธ์ และแสดงถึงฟังก์ชันที่บวกข้อมูลนำเข้ากับตัวแปร $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 แม่แบบ:Webarchive. 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 แม่แบบ:Webarchive. 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 แม่แบบ:Webarchive. 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.
• แม่แบบ:Citation covers lambda calculi from a practical type system perspective; some topics like dependent types are only mentioned, but subtyping is an important topic.

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

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

• แม่แบบ:SpringerEOM
• 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 แม่แบบ:Webarchive
• Georg P. Loczewski, The Lambda Calculus and A++
• Bret Victor, Alligator Eggs: A Puzzle Game Based on Lambda Calculus
• Lambda Calculus แม่แบบ:Webarchive on Safalra’s Website แม่แบบ:Webarchive
• แม่แบบ:Planetmath referencePlanetMath.org.
• LCI Lambda Interpreter a simple yet powerful pure calculus interpreter
• Lambda Calculus links on Lambda-the-Ultimate
• Mike Thyer, Lambda Animator แม่แบบ:Webarchive, a graphical Java applet demonstrating alternative reduction strategies.
• An Introduction to Lambda Calculus and Scheme แม่แบบ:Webarchive, by Jim Larson
• Implementing the Lambda calculus using C++ Templates
• Marius Buliga, Graphic lambda calculus
• Lambda Calculus as a Workflow Model แม่แบบ:Webarchive 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