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

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

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

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

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

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

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

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

### แรงจูงใจ
ฟังก์ชันที่คำนวณได้เป็นแนวคิดพื้นฐานในวิทยาการคอมพิวเตอร์และคณิตศาสตร์ แคลคูลัสแลมบ์ดาเป็นอรรถศาสตร์ที่เรียบง่ายสำหรับการคำนวณ ส่งผลให้สามารถศึกษาคุณสมบัติของการคำนวนได้อย่างเป็นรูปนัย อรรถศาสตร์ที่เรียบง่ายของแคลคูลัสแลมบ์ดามาจากคุณลักษณะ 2 ประการ ประการแรก แคลคูลัสแลมบ์ดาไม่มีการกำหนดชื่อให้กับฟังก์ชัน กล่าวคือ มองฟังก์ชันต่าง ๆ อย่างไร้ชื่อ (ฟังก์ชันนิรนาม) ตัวอย่างเช่น ฟังก์ชัน
: \operatorname{square\_sum}(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") อีกตัวอย่างคือ
: \operatorname{id}(x) = x
สามารถเขียนใหม่ในรูปแบบนิรนามว่า x \mapsto x, นั่นคือ ข้อมูลนำเข้าของฟังก์ชันถูกส่งไปยังตัวเอง

ประการที่สอง แคลคูลัสแลมบ์ดาอนุญาตให้ฟังก์ชันรับข้อมูลนำเข้าเพียงแค่ตัวเดียวเท่านั้น ฟังก์ชันที่รับข้อมูลนำเข้ามากกว่าหนึ่ง เช่น \operatorname{square\_sum} ที่รับข้อมูลสองตัว สามารถเขียนใหม่เป็นฟังก์ชันที่รับข้อมูลตัวแรก และคืนค่า *ฟังก์ชันอีกอัน* ที่รับข้อมูลตัวที่สอง ตัวอย่างเช่น
: (x, y) \mapsto x \times x + y \times y
สามารถเขียนใหม่เป็น
: x \mapsto (y \mapsto x \times x + y \times y)
วิธีนี้ซึ่งรู้จักกันในชื่อการเคอร์รี เป็นการเปลี่ยนฟังก์ชันที่รับหลายอาร์กิวเมนต์มาเป็นฟังก์ชันที่รับอาร์กิวเมนต์เดียวซ้อนกันหลาย ๆ ฟังก์ชัน

การเรียกใช้ฟังก์ชันของ \operatorname{square\_sum} ดั้งเดิม ด้วยข้อมูล (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 . 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 &#x5B;*<span title=" since July 2012">dead link</span>*&#x5D;. 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.&nbsp;345&#x2013;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.&nbsp;153&#x2013;173 and 219&#x2013;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'' . A gentle introduction for programmers.
* Schalk, A. and Simmons, H. (2005) *[http://www.cs.man.ac.uk/~hsimmons/BOOKS/lcalculus.pdf 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.
*  covers lambda calculi from a practical type system perspective; some topics like dependent types are only mentioned, but subtyping is an important topic.
*เนื้อหาบางส่วนของบทความนี้อิงมาจากเนื้อหาจาก FOLDOC โดยได้รับการอนุญาตแล้ว*

## แหล่งข้อมูลอื่น
* 
* Achim Jung, *[http://www.cs.bham.ac.uk/~axj/pub/papers/lambda-calculus.pdf A Short Introduction to the Lambda Calculus]*-(PDF) 
* Dana Scott, *[http://turing100.acm.org/lambda_calculus_timeline.pdf A timeline of lambda calculus]*-(PDF)
* David C. Keenan, *[http://dkeenan.com/Lambda/ To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction]*
* Raúl Rojas, *[http://www.inf.fu-berlin.de/inst/ag-ki/rojas_home/documents/tutorials/lambda.pdf A Tutorial Introduction to the Lambda Calculus]*-(PDF)
* Peter Selinger, *[http://www.mscs.dal.ca/~selinger/papers/#lambdanotes Lecture Notes on the Lambda Calculus]*-(PDF)
* L. Allison, *[http://www.allisons.org/ll/FP/Lambda/Examples/ Some executable λ-calculus examples] *
* Georg P. Loczewski, ''The Lambda Calculus and A++''
* Bret Victor, *[http://worrydream.com/AlligatorEggs/ Alligator Eggs: A Puzzle Game Based on Lambda Calculus]*
* *[http://www.safalra.com/science/lambda-calculus/ Lambda Calculus] * on Safalra’s Website 
* *PlanetMath.org<span contenteditable="false">. </span>*
* LCI Lambda Interpreter a simple yet powerful pure calculus interpreter
* Lambda Calculus links on Lambda-the-Ultimate
* Mike Thyer, Lambda Animator , a graphical Java applet demonstrating alternative reduction strategies.
* An Introduction to Lambda Calculus and Scheme , by Jim Larson
* Implementing the Lambda calculus using C++ Templates
* Marius Buliga, ''Graphic lambda calculus''
* ''Lambda Calculus as a Workflow Model''  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*

## อ้างอิง

หมวดหมู่:สิ่งประดิษฐ์ของสหรัฐ
หมวดหมู่:ทฤษฎีการคำนวณได้
หมวดหมู่:วิทยาการคอมพิวเตอร์เชิงทฤษฎี