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

ระบบรูปนัยหนึ่งในคณิตตรรกศาสตร์

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

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

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

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

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

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

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

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

แรงจูงใจ แก้

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

 

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

 

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

 

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

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

 

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

 

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

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

 
 
 ,

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

 
 
 
 

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

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

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

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

พจน์แลมบ์ดา แก้

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

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

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

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

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

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

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

ดูเพิ่ม แก้

อ่านเพิ่มเติม แก้

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

  • 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 0-262-16209-1 covers lambda calculi from a practical type system perspective; some topics like dependent types are only mentioned, but subtyping is an important topic.

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

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

อ้างอิง แก้

  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 9789067653879, สืบค้นเมื่อ 2013-09-15
  4. Computing Meaning - Google Books, Books.google.co.uk, 2008-07-02, ISBN 9781402059575, สืบค้นเมื่อ 2013-09-15
  5. Mitchell, John C. (2003), Concepts in Programming Languages, Cambridge University Press, p. 57, ISBN 9780521780988.
  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. Frink Jr., Orrin (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.