fbpx
วิกิพีเดีย

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

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

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

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

เนื้อหา

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

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

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

แรงจูงใจ

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

s q u a r e _ s u m ( x , y ) = x × x + y × y {\displaystyle \operatorname {square\_sum} (x,y)=x\times x+y\times y}

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

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

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

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

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

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

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

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

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

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

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

( ( x , y ) x × x + y × y ) ( 5 , 2 ) {\textstyle ((x,y)\mapsto x\times x+y\times y)(5,2)}
= 5 × 5 + 2 × 2 {\textstyle =5\times 5+2\times 2}
= 29 {\textstyle =29} ,

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

( ( x ( y x × x + y × y ) ) ( 5 ) ) ( 2 ) {\textstyle ((x\mapsto (y\mapsto x\times x+y\times y))(5))(2)}
= ( y 5 × 5 + y × y ) ( 2 ) {\textstyle =(y\mapsto 5\times 5+y\times y)(2)}
= 5 × 5 + 2 × 2 {\textstyle =5\times 5+2\times 2}
= 29 {\textstyle =29}

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

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

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

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

พจน์แลมบ์ดา

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

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

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

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

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

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

แคลคูลัสแลมบ์ดาไม่มีแนวคิดของการประกาศตัวแปร ในพจน์เช่น λ x . x + y {\displaystyle \lambda x.x+y} (หรือ f ( x ) = x + y {\displaystyle f(x)=x+y} ) แคลคูลัสแลมบ์ดานับ y {\displaystyle y} ว่าเป็นตัวแปรที่ยังไม่ได้รับการนิยาม การสร้างแลมบ์ดา λ x . x + y {\displaystyle \lambda x.x+y} ถูกต้องในเชิงวากยสัมพันธ์ และแสดงถึงฟังก์ชันที่บวกข้อมูลนำเข้ากับตัวแปร 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 .
  • Henk Barendregt, . 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. 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 . A classic paper highlighting the importance of lambda calculus as a basis for programming languages.
  • Larson, Jim, . A gentle introduction for programmers.
  • Schalk, A. and Simmons, H. (2005) . Notes for a course in the Mathematical Logic MSc at Manchester University.
  • de Queiroz, Ruy J.G.B. (2008) [ลิงก์เสีย]. 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 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 โดยได้รับการอนุญาตแล้ว

  • Hazewinkel, Michiel, บ.ก. (2001), , Encyclopedia of Mathematics, Springer, ISBN 978-1-55608-010-4
  • Achim Jung, -(PDF)
  • Dana Scott, -(PDF)
  • David C. Keenan,
  • Raúl Rojas, -(PDF)
  • Peter Selinger, -(PDF)
  • L. Allison,
  • Georg P. Loczewski,
  • Bret Victor,
  • on
  • on PlanetMathPlanetMath.org.
  • a simple yet powerful pure calculus interpreter
  • Mike Thyer, 2007-07-13 ที่ เวย์แบ็กแมชชีน, a graphical Java applet demonstrating alternative reduction strategies.
  • , by Jim Larson
  • using C++ Templates
  • Marius Buliga,
  • 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, , Internet Encyclopedia of Philosophy
  1. Turing, A. M. (December 1937). "Computability and λ-Definability". The Journal of Symbolic Logic. 2 (4): 153–163. doi:. JSTOR .
  2. Coquand, Thierry, , The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed.
  3. , Books.google.co.uk, 1988-01-01, ISBN 9789067653879, สืบค้นเมื่อ2013-09-15
  4. , Books.google.co.uk, 2008-07-02, ISBN 9781402059575, สืบค้นเมื่อ2013-09-15
  5. Mitchell, John C. (2003), , 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. Alama, Jesse , The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed.
  11. Frink Jr., Orrin (1944). (PDF). Bull. Amer. Math. Soc. 50 (3): 169–172. doi:.

แคลคูลัสแลมบ์ดา
แคลค, สแลมบ, ดา, ระบบร, ปน, ยหน, งในคณ, ตตรรกศาสตร, ภาษาอ, เฝ, าด, แก, ไข, หร, calculus, เป, นระบบร, ปน, ยในคณ, ตตรรกศาสตร, ใช, ในการคำนวณ, นฐานของระบบประกอบไปด, วยการสร, างฟ, งก, นและการเร, ยกใช, งก, นโดยใช, การโยงของต, วแปรและการแทนท, วแปร, กคณ, ตศาสตร, อลอน. aekhlkhulsaelmbda rabbrupnyhnunginkhnittrrksastr phasaxun efadu aekikh aekhlkhulsaelmbda hrux l calculus epnrabbrupnyinkhnittrrksastrthiichinkarkhanwn phunthankhxngrabbprakxbipdwykarsrangfngkchnaelakareriykichfngkchnodyichkaroyngkhxngtwaepraelakaraethnthitwaepr nkkhnitsastrxlxnos echirchidkhidkhnaekhlkhulsaelmbdakhunmainchwngpi 1930 ephuxsarwcharakthankhxngkhnitsastr aekhlkhulsaelmbdaepnaebbcalxngsaklinkarkhanwnethiybethakbekhruxngckrthwring khwamethaethiymknkhxngaxngrabbthngsxngruckidrbkarphisucninaenwkhidhlkkhxngechirch thwringinpi 1937 1 khawa aelmbda sungepnxkkhrakrik l praktinphcnaelmbda hruxxaccaeriykwaniphcnaelmbda sungichinkaraesdngthungkaroyngtwaeprinfngkchn aekhlkhulsaelmbdamisxngrupaebb aebbmichnidkhxmul aela immichnidkhxmul inaekhlkhulsaelmbdathimichnidkhxmul fngkchnsamartheriykichidemuxchnidkhxngfngkchnsxdkhlxngkbchnidkhxngkhxmulnaekhakhxngfngkchnethann mikarnaaekhlkhulsaelmbdaipprayuktichinhlakhlaydaninkhnitsastr prchya 2 phasasastr 3 4 aelawithyakarkhxmphiwetxr 5 aekhlkhulsaelmbdayngmibthbathsakhyinkarphthnakhxngthvsdikhxngphasakhxmphiwetxr phasaopraekrmaebbfngchnepnphlmacakaekhlkhulsaelmbda enuxha 1 aekhlkhulsaelmbdainprawtisastrkhxngkhnitsastr 2 khaxthibayxyangimepnthangkar 2 1 aerngcungic 2 2 aekhlkhulsaelmbda 2 2 1 phcnaelmbda 3 duephim 4 xanephimetim 5 aehlngkhxmulxun 6 xangxingaekhlkhulsaelmbdainprawtisastrkhxngkhnitsastr aekikhnkkhnitsastrxlxnos echirch idkhidkhnaekhlkhulsaelmbdakhunmainchwngpi 1930 ephuxsarwcharakthankhxngkhnitsastr 6 7 inpi 1935 Stephen Kleene aela J B Rosser idkhnphb Kleene Rosser paradox sungaesdngihehnwarabbedimkhxngaekhlkhulsaelmbdamikhwamkhdaeyngkninechingtrrksastr txmainpi 1936 echirchaeykechphaaswnthiekiywkhxngkbkarkhanwninrabbedimxxkma aelacdphimphechphaaswndngklaw sunginpccubneriykknwaaekhlkhulsaelmbdaaebbimmichnidkhxmul 8 inpi 1940 echirchyngidsrangaekhlkhulsaelmbdaaebbmichnidkhxmulxyangngay sungrabbthiimthrngphlnginechingkarkhanwnethaaebbimmichnidkhxmul aetrabbnisxdkhlxngkninechingtrrksastr 9 kxnchwngpi 1960 aekhlkhulsaelmbdaepnephiyngaekhrupnyniyminthangkhnitsastrethann aetinchwngpi 1960 khwamsmphnthrahwangaekhlkhulsaelmbdaaelaphasaopraekrmkepnthichdecn aekhlkhulsaelmbdayngerimmikhwamsakhyinphasasastr duthi Heim and Kratzer 1998 cakkarprayuktrabbinxrrthsastrkhxngphasathrrmchatiody Montague aelankphasasastrxun inchwngewlaediywknaekhlkhulsaelmbdayngerimmikhwamsakhyinwithyakarkhxmphiwetxr 10 khaxthibayxyangimepnthangkar aekikhaerngcungic aekikh fngkchnthikhanwnidepnaenwkhidphunthaninwithyakarkhxmphiwetxraelakhnitsastr aekhlkhulsaelmbdaepnxrrthsastrthieriybngaysahrbkarkhanwn sngphlihsamarthsuksakhunsmbtikhxngkarkhanwnidxyangepnrupny xrrthsastrthieriybngaykhxngaekhlkhulsaelmbdamacakkhunlksna 2 prakar prakaraerk aekhlkhulsaelmbdaimmikarkahndchuxihkbfngkchn klawkhux mxngfngkchntang xyangirchux fngkchnnirnam twxyangechn fngkchn s q u a r e s u m x y x x y y displaystyle operatorname square sum x y x times x y times y samarthekhiynihminrupaebbnirnamwa x y x x y y displaystyle x y mapsto x times x y times y khwamhmaykhux khuxndb x aela y thuksngipyng x x y y textstyle x times x y times y xiktwxyangkhux id x x displaystyle operatorname id x x samarthekhiynihminrupaebbnirnamwa x x textstyle x mapsto x nnkhux khxmulnaekhakhxngfngkchnthuksngipyngtwexng prakarthisxng aekhlkhulsaelmbdaxnuyatihfngkchnrbkhxmulnaekhaephiyngaekhtwediywethann fngkchnthirbkhxmulnaekhamakkwahnung echn s q u a r e s u m textstyle operatorname square sum thirbkhxmulsxngtw samarthekhiynihmepnfngkchnthirbkhxmultwaerk aelakhunkhafngkchnxikxnthirbkhxmultwthisxng twxyangechn x y x x y y displaystyle x y mapsto x times x y times y samarthekhiynihmepn x y x x y y displaystyle x mapsto y mapsto x times x y times y withinisungruckkninchuxkarekhxrri epnkarepliynfngkchnthirbhlayxarkiwemntmaepnfngkchnthirbxarkiwemntediywsxnknhlay fngkchn kareriykichfngkchnkhxng s q u a r e s u m textstyle operatorname square sum dngedim dwykhxmul 5 2 thaihekidkarpramwlphldngtxipni x y x x y y 5 2 textstyle x y mapsto x times x y times y 5 2 5 5 2 2 textstyle 5 times 5 2 times 2 29 textstyle 29 aetkarpramwlphlkhxngfngkchnthiekhiynihm mikarekhxrri mikhntxnephimkhunhnungkhntxn x y x x y y 5 2 textstyle x mapsto y mapsto x times x y times y 5 2 y 5 5 y y 2 textstyle y mapsto 5 times 5 y times y 2 5 5 2 2 textstyle 5 times 5 2 times 2 29 textstyle 29 aetthngsxngwithiihphllphthehmuxnkn aekhlkhulsaelmbda aekikh aekhlkhulsaelmbdaprakxbipdwy phcnaelmbda sungniyamodywakysmphnthrupny aelakdtang inkarepliynrupsungthaihsamarthcdkaraelapramwlphlphcnaelmbdaid karepliynrupehlanisamarthmxngepnthvsdiechingsmkarhruxkarniyamechingdaeninkar fngkchnthnghmdinaekhlkhulsaelmbdaepnfngkchnnirnamtamthiidxthibayiwaelwkhangtn nxkcakni fngkchnyngrbkhxmulnaekhaephiyngaekhtwediywethann odyichkarekhxrriephuxaeplngfngkchnthirbkhxmulnaekhahlaytwepnfngkchnthirbkhxmulnaekhaephiyngtwediyw phcnaelmbda aekikh wakysmphnthkhxngphcnaelmbdaniyambangniphcnihepn niphncaekhlkhulsaelmbdathithuktxnghruximthuktxng niphncaekhlkhulsaelmbdathithuktxngeriykwa phcnaelmbda kd 3 prakardanlangepnniyamechingxupnysungichinkarsrangphcnaelmbdathnghmdthithuktxng twaepr x displaystyle x epnphcnaelmbda tha t displaystyle t epnphcnaelmbda aela x displaystyle x epntwaepr aelwcaidwa l x t displaystyle lambda x t epnphcnaelmbda eriykphcndngklawwa karsrangaelmbda hrux lambda abstraction tha t displaystyle t aela s displaystyle s epnphcnaelmbda aelwcaidwa t s displaystyle ts epnphcnaelmbda eriykphcndngklawwa kareriykichhrux application kdkhangtnepnkdthnghmdthiichxthibayphcnaelmbda immiktxun xikthiichinkarxthibayphcnaelmbda dngnn phcnhnung caepnphcnaelmbdathithuktxngktxemuxphcnnnsamarthsrangidcakkarichkdthng 3 saipmacnidphcndngklaw xyangirktam wngelbxaccasamarthlaiwidinbangkrni echn wngelbchnnxksudmkcamikarlaiw duephimetimthiswnsylksndanlang karsrangaelmbda l x t displaystyle lambda x t epnkarniyamfngkchnnirnamthisamarthrbkhxmulnaekha x displaystyle x aelaaethnthikhxmuldngklawin niphcn t displaystyle t dngnn nicungepnkarniyamfngkchnnirnamthirbkhxmulnaekha x displaystyle x aelakhunkha t displaystyle t twxyangechn l x x 2 2 displaystyle lambda x x 2 2 epnkarsrangaelmbdakhxngfngkchn f x x 2 2 displaystyle f x x 2 2 odymiphcn x 2 2 displaystyle x 2 2 epn t displaystyle t niyamkhxngkarsrangaelmbdaniephiyngaekh srang twfngkchn aetimideriykichfngkchn karsrangaelmbdaoyngtwaepr x displaystyle x inphcn t displaystyle t kareriykich t s displaystyle ts epnkareriykichfngkchn t displaystyle t dwykhxmulnaekha s displaystyle s nnkhuxepnkareriykichfngkchn t displaystyle t dwy s displaystyle s ephuxihkha t s displaystyle t s aekhlkhulsaelmbdaimmiaenwkhidkhxngkarprakastwaepr inphcnechn l x x y displaystyle lambda x x y hrux f x x y displaystyle f x x y aekhlkhulsaelmbdanb y displaystyle y waepntwaeprthiyngimidrbkarniyam karsrangaelmbda l x x y displaystyle lambda x x y thuktxnginechingwakysmphnth aelaaesdngthungfngkchnthibwkkhxmulnaekhakbtwaepr y displaystyle y sungyngimrukhaduephim aekikhxanephimetim aekikhAbelson Harold amp 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 Archived 2011 10 10 thi ewyaebkaemchchin 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 11 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 A gentle introduction for programmers Schalk A and Simmons H 2005 An introduction to l 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 lingkesiy 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 hnngsuxxaneriynsahrbnkeriynpriyyaexk Morten Heine Sorensen Pawel 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 enuxhabangswnkhxngbthkhwamnixingmacakenuxhacak FOLDOC odyidrbkarxnuyataelwaehlngkhxmulxun aekikhHazewinkel Michiel b k 2001 Lambda calculus Encyclopedia of Mathematics Springer ISBN 978 1 55608 010 4 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 Raul Rojas A Tutorial Introduction to the Lambda Calculus PDF Peter Selinger Lecture Notes on the Lambda Calculus PDF L Allison Some executable l calculus examples Georg P Loczewski The Lambda Calculus and A Bret Victor Alligator Eggs A Puzzle Game Based on Lambda Calculus Lambda Calculus on Safalra s Website Lambda Calculus on PlanetMathPlanetMath org LCI Lambda Interpreter a simple yet powerful pure calculus interpreter Lambda Calculus links on Lambda the Ultimate Mike Thyer Lambda Animator Archived 2007 07 13 thi ewyaebkaemchchin 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 Philosophyxangxing aekikh Turing A M December 1937 Computability and l Definability The Journal of Symbolic Logic 2 4 153 163 doi 10 2307 2268280 JSTOR 2268280 Coquand Thierry Type Theory The Stanford Encyclopedia of Philosophy Summer 2013 Edition Edward N Zalta ed Categorial Investigations Logical and Linguistic Aspects of the Lambek Calculus Michael Moortgat Google Books Books google co uk 1988 01 01 ISBN 9789067653879 subkhnemux 2013 09 15 Computing Meaning Google Books Books google co uk 2008 07 02 ISBN 9781402059575 subkhnemux 2013 09 15 Mitchell John C 2003 Concepts in Programming Languages Cambridge University Press p 57 ISBN 9780521780988 A Church A set of postulates for the foundation of logic Annals of Mathematics Series 2 33 346 366 1932 For a full history see Cardone and Hindley s History of Lambda calculus and Combinatory Logic 2006 A Church An unsolvable problem of elementary number theory American Journal of Mathematics Volume 58 No 2 Church A A Formulation of the Simple Theory of Types Journal of Symbolic Logic 5 1940 doi 10 2307 2266170 Alama Jesse The Lambda Calculus The Stanford Encyclopedia of Philosophy Summer 2013 Edition Edward N Zalta ed 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 ekhathungcak https th wikipedia org w index php title aekhlkhulsaelmbda amp oldid 9552813, wikipedia, วิกิ หนังสือ, หนังสือ, ห้องสมุด,

บทความ

, อ่าน, ดาวน์โหลด, ฟรี, ดาวน์โหลดฟรี, mp3, วิดีโอ, mp4, 3gp, jpg, jpeg, gif, png, รูปภาพ, เพลง, เพลง, หนัง, หนังสือ, เกม, เกม