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

แคลคูลัสแลมบ์ดาประกอบด้วยภาษาของเทอมแลมบ์ดาซึ่งถูกกำหนดโดยไวยากรณ์เชิงรูปธรรม และชุดของกฎการแปลงสำหรับการจัดการเทอมเหล่านั้น ในBNFไวยากรณ์คือโดยที่ตัวแปรx , y , zครอบคลุมเซตของชื่อที่ไม่มีที่สิ้นสุด เทอมM , N , t , s , e , fครอบคลุมเทอมแลมบ์ดาทั้งหมด ซึ่งสอดคล้องกับนิยามอุปนัย ต่อไปนี้ : ${\displaystyle e::=x\mid \lambda xe\mid e\,e,}$

• ตัวแปรxเป็นเทอมแลมบ์ดาที่ถูกต้อง
• นามธรรมคือเทอมแลมบ์ดาโดยที่t คือเทอมแลมบ์ดา ซึ่งเรียกว่า ส่วนเนื้อหาของนามธรรมและx คือ ตัวแปรพารามิเตอร์ของนามธรรม${\displaystyle (\lambda xt)}$
• แอปพลิเคชันคือเทอมแลมบ์ดาโดยที่tและsเป็นเทอมแลมบ์ดา${\displaystyle (t\,s)}$

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

ภายในเทอมแลมบ์ดา การปรากฏของตัวแปรใดๆ ที่ไม่ใช่พารามิเตอร์ของ λ ที่ล้อมรอบอยู่ เรียกว่าตัวแปรอิสระการปรากฏแบบอิสระของตัวแปรอิสระในเทอม ใดๆ จะถูกผูกไว้ใน เทอม นั้น การปรากฏแบบอิสระของตัวแปรอื่นๆ ภายในเทอมนั้นจะยังคงเป็นอิสระในเทอมนั้น ${\displaystyle x}$${\displaystyle M}$${\displaystyle \lambda xM}$${\displaystyle M}$${\displaystyle \lambda xM}$

ตัวอย่างเช่น ในเทอมทั้งและปรากฏเป็นอิสระ ในเป็นอิสระ แต่ในส่วนเนื้อหา (เช่น หลังจุด) ไม่เป็นอิสระ และกล่าวได้ว่าถูกผูกไว้ (กับพารามิเตอร์) ในขณะที่เป็นอิสระใน แต่ถูกผูกไว้ในมีสองครั้งที่ ปรากฏใน– ครั้งหนึ่งถูกผูกไว้ และอีกครั้งเป็นอิสระ ${\displaystyle x\,y}$${\displaystyle x}$${\displaystyle y}$${\displaystyle (\lambda xx\,y)}$${\displaystyle y}$${\displaystyle x}$${\displaystyle y}$${\displaystyle (\lambda xx\,y)}$${\displaystyle (\แลมบ์ดา y.\แลมบ์ดา xx\,y)}$${\displaystyle x}$${\displaystyle (\lambda y.(\lambda xx\,y)\,x)}$

FV(M)คือเซตของตัวแปรอิสระของMกล่าวคือ ตัวแปรที่ปรากฏเป็นอิสระในMอย่างน้อยหนึ่งครั้ง สามารถนิยามแบบอุปนัยได้ดังนี้:

• ${\displaystyle \operatorname {FV} (x)=\{x\}}$
• ${\displaystyle \operatorname {FV} (M_{1}M_{2})=\operatorname {FV} (M_{1})\cup \operatorname {FV} (M_{2})}$
• ${\displaystyle \operatorname {FV} (\lambda xM)=\operatorname {FV} (M)\backslash \{x\}}$

สัญลักษณ์นี้หมายถึงการแทนที่แบบหลีกเลี่ยงการจับตัวแปร : แทนที่N ด้วย xที่ปรากฏอย่างอิสระในM ทุกครั้ง ในขณะที่หลีกเลี่ยงการจับตัวแปร^{[ a ]} ​​การดำเนินการนี้ถูกกำหนดแบบอุปนัยดังต่อไปนี้: ${\displaystyle M[x:=N]}$

• ${\displaystyle x[x:=N]=N}$; ถ้า.${\displaystyle y[x:=N]=y}$${\displaystyle y\neq x}$
• ${\displaystyle (M_{1}M_{2})[x:=N]=(M_{1}[x:=N])(M_{2}[x:=N])}$.
• ${\displaystyle (\lambda yM)[x:=N]}$มีสามกรณี:
  • ถ้ากลายเป็น( ถูกผูกไว้; ไม่มีการเปลี่ยนแปลง)${\displaystyle y=x}$${\displaystyle \lambda xM}$${\displaystyle x}$
  • ถ้ากลายเป็น.${\displaystyle y\notin FV(N)}$${\displaystyle \lambda y.(M[x:=N])}$
  • ถ้าให้เปลี่ยนชื่อ α เป็นชื่อใหม่ ก่อน เพื่อหลีกเลี่ยงการชนกันของชื่อจากนั้นดำเนินการต่อตามข้างต้น ชื่อจะกลายเป็นชื่อใหม่${\displaystyle y\in FV(N)}$${\displaystyle \lambda yM}$${\displaystyle \lambda y'.M[y:=y']}$${\displaystyle y'}$${\displaystyle \lambda y'.M[y:=y'][x:=N]}$${\displaystyle y'\notin \operatorname {FV} (M)\cup \operatorname {FV} (N)}$

มีแนวคิดเรื่อง "ความเท่าเทียมกัน" และ "การลดทอน" หลายประการที่ทำให้สามารถลดเทอมแลมบ์ดาเป็นเทอมแลมบ์ดาที่เทียบเท่ากันได้^{[ 3 ]}

• การแปลงอัลฟา (α-conversion)แสดงให้เห็นถึงสัญชาตญาณที่ว่า การเลือกตัวแปรผูกพันเฉพาะเจาะจงในนามธรรมนั้น (โดยปกติ) ไม่สำคัญ ถ้าแล้วเทอมและถือว่า สมมูลกันแบบอัลฟา (alpha-equivalent ) เขียนแทนด้วยความสัมพันธ์สมมูล คือความสัมพันธ์สอดคล้องที่เล็กที่สุดบนเทอมแลมบ์ดาที่สร้างขึ้นโดยกฎนี้ ตัวอย่างเช่นและเป็นเทอมแลมบ์ดาที่สมมูลกันแบบอัลฟา${\displaystyle y\notin FV(M)}$${\displaystyle \lambda xM}$${\displaystyle \lambda yM[x:=y]}$${\displaystyle \lambda xM\equiv _{\alpha }\lambda yM[x:=y]}$${\displaystyle \lambda xx}$${\displaystyle \lambda yy}$
• กฎการลดรูป βระบุว่า β-redex ซึ่งเป็นการประยุกต์ใช้ในรูปแบบ จะลด รูปเป็นเทอม^{[ b ]}ตัวอย่างเช่น สำหรับทุก, . สิ่งนี้แสดงให้เห็นว่าเป็นเอกลักษณ์จริงๆ ในทำนองเดียวกันซึ่งแสดงให้เห็นว่าเป็นฟังก์ชันคงที่${\displaystyle (\lambda xt)s}$${\displaystyle t[x:=s]}$${\displaystyle s}$${\displaystyle (\lambda xx)s\to x[x:=s]=s}$${\displaystyle \lambda xx}$${\displaystyle (\lambda xy)s\to y[x:=s]=y}$${\displaystyle \lambda xy}$
• การแปลง ηแสดงถึงความเป็นส่วนขยายและแปลงระหว่างและเมื่อใดก็ตามที่ไม่ปรากฏเป็นอิสระในมักถูกละเว้นในตำราแคลคูลัสแลมบ์ดาหลายเล่ม${\displaystyle \lambda x.fx}$${\displaystyle f}$${\displaystyle x}$${\displaystyle f}$

คำว่าredexซึ่งย่อมาจากreducible expressionหมายถึงเทอมย่อยที่สามารถลดรูปได้โดยใช้กฎการลดรูปข้อใดข้อหนึ่ง ตัวอย่างเช่น (λ x . M ) Nเป็น β-redex ในการแสดงการแทนที่Nด้วยxในMนิพจน์ที่ redex ลดรูปได้เรียกว่าreduct ของมัน reduct ของ (λ x . M ) NคือM [ x  := N ]

แคลคูลัสแลมบ์ดาเป็นแบบทัวริงสมบูรณ์นั่นคือ เป็นแบบจำลองการคำนวณ สากล ที่สามารถใช้จำลองเครื่องจักรทัวริง ใดๆ ก็ได้^{[ 4 ]}ชื่อของมันมาจากอักษรกรีกแลมบ์ดา (λ) ซึ่งใช้ในนิพจน์แลมบ์ดาและเทอมแลมบ์ดาเพื่อแสดงถึงการ ผูกตัวแปรในฟังก์ชัน

แคลคูลัสแลมบ์ดาอาจเป็นแบบไม่มีประเภทหรือมีประเภทในแคลคูลัสแลมบ์ดาแบบมีประเภท ฟังก์ชันจะสามารถใช้งานได้ก็ต่อเมื่อสามารถรับ "ประเภท" ของข้อมูลอินพุตที่กำหนดได้เท่านั้น แคลคูลัสแลมบ์ดาแบบมีประเภทนั้นอ่อนแอกว่าแคลคูลัสแลมบ์ดาแบบไม่มีประเภท ซึ่งเป็นหัวข้อหลักของบทความนี้ ในแง่ที่ว่าแคลคูลัสแลมบ์ดาแบบมีประเภทสามารถแสดงได้น้อยกว่าแคลคูลัสแบบไม่มีประเภท ในทางกลับกัน สามารถพิสูจน์สิ่งต่างๆ ได้มากขึ้นด้วยแคลคูลัสแลมบ์ดาแบบมีประเภท ตัวอย่างเช่น ในแคลคูลัสแลมบ์ดาแบบมีประเภทอย่างง่ายมีทฤษฎีบทว่ากลยุทธ์การประเมินทุกกลยุทธ์จะสิ้นสุดลงสำหรับเทอมแลมบ์ดาแบบมีประเภทอย่างง่ายทุกเทอม^{[ 5 ]}ในขณะที่การประเมินเทอมแลมบ์ดาแบบไม่มีประเภทไม่จำเป็นต้องสิ้นสุดลง (ดูด้านล่าง ) เหตุผลหนึ่งที่มีแคลคูลัสแลมบ์ดาแบบมีประเภทที่แตกต่างกันมากมายก็คือความปรารถนาที่จะทำสิ่งต่างๆ ได้มากขึ้น (จากสิ่งที่แคลคูลัสแบบไม่มีประเภทสามารถทำได้) โดยไม่ละทิ้งความสามารถในการพิสูจน์ทฤษฎีบทที่แข็งแกร่งเกี่ยวกับแคลคูลัส

แคลคูลัสแลมบ์ดามีการประยุกต์ใช้ในหลายสาขาที่แตกต่างกันในคณิตศาสตร์^{ปรัชญา [6] ภาษาศาสตร์ [7] [8] และวิทยาศาสตร์คอมพิวเตอร์ [9} ] [ ^{10 ] แคลคูลัส}แลมบ์^{ดามีบทบาทสำคัญ}ในการพัฒนา^{ทฤษฎีภาษาโปรแกรมภาษาโปรแกรมเชิง}ฟังก์ชันใช้แคลคูลัสแลมบ์ดา แคลคูลัสแลมบ์ดายังเป็นหัวข้อวิจัยในปัจจุบันใน^{ทฤษฎี}หมวดหมู่^{[ 11 ]}

แคลคูลัสแลมบ์ดาได้รับการแนะนำโดยนักคณิตศาสตร์Alonzo Churchในช่วงทศวรรษ 1930 ซึ่งเป็นส่วนหนึ่งของการตรวจสอบรากฐานของคณิตศาสตร์ [ ^{12 ] [ c ]}ระบบดั้งเดิมได้รับการพิสูจน์แล้วว่า^ไม่สอดคล้องกันทางตรรกะในปี 1935 เมื่อ Stephen Kleene และJB Rosserพัฒนาปรากฏการณ์ Kleene–Rosser paradox ^{[ 13 ] [ 14 ]}

ต่อมาในปี พ.ศ. 2479 เชิร์ชได้แยกและเผยแพร่เฉพาะส่วนที่เกี่ยวข้องกับการคำนวณ ซึ่งปัจจุบันเรียกว่าแคลคูลัสแลมบ์ดาแบบไม่มีประเภท^{[ 15 ]}ในปี พ.ศ. 2483 เขายังได้แนะนำระบบที่อ่อนแอกว่าในเชิงการคำนวณ แต่มีความสอดคล้องกันทางตรรกะ ซึ่งรู้จักกันในชื่อ แคลคูลัสแลมบ์ ดาแบบมีประเภทอย่างง่าย^{[ 16 ]}

จนกระทั่งถึงช่วงทศวรรษ 1960 เมื่อความสัมพันธ์กับภาษาโปรแกรมได้รับการชี้แจง แคลคูลัสแลมบ์ดาจึงเป็นเพียงรูปแบบเท่านั้น ต้องขอบคุณริชาร์ด มอนแทกูและนักภาษาศาสตร์คนอื่นๆ ที่นำไปประยุกต์ใช้ในความหมายของภาษาธรรมชาติ แคลคูลัสแลมบ์ดาจึงเริ่มได้รับการยอมรับในสาขาภาษาศาสตร์^{[ 17 ]}และวิทยาศาสตร์คอมพิวเตอร์^{[ 18 ]}

ยังมีความไม่แน่นอนอยู่บ้างเกี่ยวกับเหตุผลที่เชิร์ชใช้ตัวอักษรกรีกแลมบ์ดา (λ) เป็นสัญลักษณ์แทนการแทนที่ฟังก์ชันในแคลคูลัสแลมบ์ดา ซึ่งอาจเป็นเพราะคำอธิบายที่ขัดแย้งกันของตัวเชิร์ชเอง ตามที่คาร์โดนและฮินด์ลีย์ (2006) กล่าวไว้ว่า:

อย่างไรก็ตาม ทำไม Church ถึงเลือกใช้สัญลักษณ์ "λ"? ใน [จดหมายที่ไม่ได้รับการตีพิมพ์ในปี 1964 ถึง Harald Dickson] เขาได้ระบุไว้อย่างชัดเจนว่า สัญลักษณ์นี้มาจากสัญลักษณ์ " " ที่ Whitehead และ Russellใช้สำหรับนามธรรมของคลาสโดยการปรับเปลี่ยน " " เป็น " เพื่อแยกความแตกต่างระหว่างนามธรรมของฟังก์ชันกับนามธรรมของคลาส จากนั้นจึงเปลี่ยน " " เป็น "λ" เพื่อความสะดวกในการพิมพ์ ${\displaystyle {\hat {x}}}$${\displaystyle {\hat {x}}}$${\displaystyle \land x}$${\displaystyle \land }$

ที่มานี้ได้รับการรายงานไว้ใน [Rosser, 1984, p.338] เช่นกัน ในทางกลับกัน ในช่วงบั้นปลายชีวิต เชิร์ชได้บอกกับผู้สอบถามสองคนว่า การเลือกสัญลักษณ์นี้เป็นเรื่องบังเอิญมากกว่า คือมีความจำเป็นต้องใช้สัญลักษณ์ และสัญลักษณ์ λ ก็บังเอิญถูกเลือกขึ้นมา

Dana Scottได้กล่าวถึงคำถามนี้ในการบรรยายสาธารณะต่างๆ ด้วยเช่นกัน^{[ 19 ]} Scott เล่าว่าครั้งหนึ่งเขาเคยตั้งคำถามเกี่ยวกับที่มาของสัญลักษณ์แลมบ์ดาให้กับ John W. Addison Jr. อดีตนักเรียนและลูกเขยของ Church ซึ่งต่อมาได้เขียนโปสการ์ดถึงพ่อตาของเขา:

เรียน ศาสตราจารย์เชิร์ช,

รัสเซลมีตัวดำเนินการไอโอตา ส่วนฮิลเบิร์ตมีตัวดำเนินการเอปซิลอนทำไมคุณถึงเลือกแลมบ์ดาเป็นตัวดำเนินการของคุณ?

ตามคำกล่าวของสก็อตต์ คำตอบทั้งหมดของเชิร์ชประกอบด้วยการส่งโปสการ์ดคืนพร้อมข้อความกำกับว่า " eeny, meeny, miny, moe "

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

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

สามารถเขียนใหม่ในรูปแบบที่ไม่ระบุชื่อได้ดังนี้

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

(ซึ่งอ่านว่า " คู่ของxและyถูกแมปไปยัง") ^{[ d ]}ในทำนองเดียวกัน ฟังก์ชัน ${\textstyle x^{2}+y^{2}}$

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

สามารถเขียนใหม่ในรูปแบบที่ไม่ระบุชื่อได้ดังนี้

${\displaystyle x\mapsto x}$

โดยที่อินพุตจะถูกแมปไปยังตัวมันเอง^{[ d ]}

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

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

สามารถปรับเปลี่ยนเป็น

${\displaystyle x\mapsto (y\mapsto (x^{2}+y^{2}))}$

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

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

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

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

${\textstyle =29}$,

ในขณะที่การประเมินเวอร์ชันที่ปรุงด้วยเครื่องแกงนั้นต้องผ่านขั้นตอนเพิ่มเติมอีกหนึ่งขั้นตอน

${\textstyle {\Bigl (}{\bigl (}x\mapsto (y\mapsto x^{2}+y^{2}){\bigr )}(5){\Bigr )}(2)}$

${\textstyle =(y\mapsto 5^{2}+y^{2})(2)}$// นิยามของได้ถูกนำมาใช้ร่วมกับในนิพจน์ภายใน ซึ่งคล้ายกับการลดรูปเบต้า (β-reduction)${\displaystyle x}$${\displaystyle 5}$

${\textstyle =5^{2}+2^{2}}$// นิยามของได้ถูกนำมาใช้ร่วมกับอีกครั้ง คล้ายกับการลดเบต้า${\displaystyle y}$${\displaystyle 2}$

${\textstyle =29}$

เพื่อให้ได้ผลลัพธ์เดียวกัน

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

สามารถแสดงได้ว่าการลดแบบ β นั้นมีความต่อเนื่องเมื่อดำเนินการไปจนถึงการแปลงแบบ α (กล่าวคือ เราถือว่ารูปแบบปกติสองรูปแบบเท่ากันหากสามารถแปลงแบบ α รูปแบบหนึ่งไปเป็นอีกรูปแบบหนึ่งได้) หากการประยุกต์ใช้ขั้นตอนการลดซ้ำ ๆสิ้นสุดลงในที่สุด ตามทฤษฎีบทของ Church–Rosserมันจะสร้างรูปแบบปกติแบบ β ที่ไม่ซ้ำ กัน อย่างไรก็ตาม แคลคูลัสแลมบ์ดาที่ไม่มีประเภทเป็นกฎการเขียนใหม่ ภายใต้การลดแบบ β นั้น ไม่ใช่ทั้งการทำให้เป็นปกติอย่างเข้มแข็งหรือการทำให้เป็นปกติอย่างอ่อนแอมีเทอมที่ไม่มีรูปแบบปกติ เช่นΩ

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

แคลคูลัสแลมบ์ดาพื้นฐานสามารถใช้ในการจำลองเลขคณิต บูลี น โครงสร้างข้อมูล และการเรียกซ้ำได้ ดังที่แสดงในหัวข้อย่อยต่อไปนี้i , ii , iiiและiv

ในแคลคูลัสแลมบ์ดา มีหลายวิธีในการกำหนดจำนวนธรรมชาติแต่ที่พบได้บ่อยที่สุดคือจำนวนเชิร์ชซึ่งสามารถกำหนดได้ดังนี้:

0 := λ f .λ x . x

1 := λ f .λ x . f x

2 := λ f .λ x . f ( f x )

3 := λ f .λ x . f ( f ( f x ))

และอื่นๆ หรือการใช้ไวยากรณ์ทางเลือกที่อนุญาตให้มีอาร์กิวเมนต์หลายตัวที่ไม่ใช้ curried ในฟังก์ชัน:

0 := λ fx . x

1 := λ fx . f x

2 := λ fx . f ( f x )

3 := λ fx . f ( f ( f x ))

ตัวเลขเชิร์ช (Church numeral) คือฟังก์ชันลำดับสูง — โดยรับฟังก์ชัน fที่มีอาร์กิวเมนต์เดียวและส่งคืนฟังก์ชันที่มีอาร์กิวเมนต์เดียวอีกฟังก์ชันหนึ่ง ตัวเลขเชิร์ชnคือฟังก์ชันที่รับฟังก์ชันfเป็นอาร์กิวเมนต์และส่งคืนการประกอบฟังก์ชันfลำดับที่n กล่าว คือ ฟังก์ชันfที่ประกอบกับตัวเองnครั้ง ซึ่งเขียนแทนด้วยf ^{( n )}และในความเป็นจริงคือเลข ยกกำลัง nของf (ถือว่าเป็นตัวดำเนินการ) โดยf ⁽⁰⁾ถูกกำหนดให้เป็นฟังก์ชันเอกลักษณ์ การประกอบฟังก์ชันมีคุณสมบัติการสลับที่ดังนั้น การประกอบฟังก์ชันf ซ้ำๆ กันจึงเป็นไปตาม กฎของเลขยกกำลังสอง ข้อ คือf ^{( m )} ∘ f ^{( n )} = f ^{( m+n )}และ( f ^{( n )} ) ^{( m )} = f ^{( m*n )}ซึ่งเป็นเหตุผลว่าทำไมตัวเลขเหล่านี้จึงสามารถใช้ในการคำนวณเลขคณิตได้ (ในแคลคูลัสแลมบ์ดาแบบดั้งเดิมของเชิร์ช พารามิเตอร์อย่างเป็นทางการของนิพจน์แลมบ์ดาจะต้องปรากฏอย่างน้อยหนึ่งครั้งในส่วนของฟังก์ชัน ซึ่งทำให้คำจำกัดความของ0 ข้างต้น เป็นไปไม่ได้)

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

λ n .λ x . n (PAIR x ) NIL

สร้าง ลำดับของการประยุกต์ใช้จำนวน n ครั้งโดยกำหนดเลข Church nและค่า x บางค่า

คู่x (คู่x ...(คู่xไม่มี)...)

โดยการเปลี่ยนแปลงสิ่งที่ถูกทำซ้ำ และอาร์กิวเมนต์ที่ฟังก์ชันที่ถูกทำซ้ำนั้นถูกนำไปใช้ จะสามารถสร้างผลลัพธ์ที่แตกต่างกันได้มากมาย

เราสามารถกำหนดฟังก์ชันตัวสืบทอด ซึ่งรับค่า Church numeral nและส่งคืนค่าตัวสืบทอดn + 1โดยการใช้ฟังก์ชันfที่ได้รับมาอีกหนึ่งครั้ง โดยที่( nfx )หมายถึง " การใช้ ฟังก์ชัน f จำนวน n ครั้งโดยเริ่มจากx "

SUCC := λ n .λ f .λ x . f ( n f x )

เนื่องจาก องค์ประกอบลำดับที่ mของfเมื่อรวมกับ องค์ประกอบลำดับ ที่ nของfจะได้ องค์ประกอบลำดับที่ m + nของfดังนั้นf ^{( m )} ∘ f ^{( n )} = f ^{( m+n )}การบวกจึงสามารถนิยามได้ดังนี้

บวก := แลมบ์ . แลม .แลมบ์ ฉ . แลมx . มฉ ( n f x )

ฟังก์ชัน PLUSสามารถมองได้ว่าเป็นฟังก์ชันที่รับจำนวนธรรมชาติสองจำนวนเป็นอาร์กิวเมนต์และส่งคืนค่าเป็นจำนวนธรรมชาติ สามารถตรวจสอบได้ว่า

บวก 2 3

และ

5

เป็นนิพจน์แลมบ์ดาที่เทียบเท่ากับเบต้า เนื่องจากสามารถเพิ่มmให้กับจำนวนได้โดยการทำซ้ำการดำเนินการตัวถัดไปmครั้ง ดังนั้นคำจำกัดความทางเลือกจึงเป็นดังนี้:

บวก′ := แลม. .แลม . ม. SUCC ^{[ 20 ]}

ในทำนองเดียวกัน ตาม( f ^{( n )} ) ^{( m )} = f ^{( m*n )}การคูณสามารถนิยามได้ดังนี้

MULT := λ m .λ n .λ f . m ( n f ) ^{[ 21 ]}

ดังนั้น การคูณตัวเลขของ Church ก็คือการประกอบกันของตัวเลขเหล่านั้นในฐานะฟังก์ชันนั่นเอง หรืออีกนัยหนึ่ง

หลาย′ := แลม. .แลn . ม. (บวกn ) 0

เนื่องจากการคูณmกับnนั้นเหมือนกับการบวกnซ้ำๆ กันmครั้ง โดยเริ่มจากศูนย์

การยกกำลัง คือการคูณจำนวนกับตัวเองซ้ำๆ ซึ่งแปลได้ว่าเป็นการนำเลข Church มาประกอบกับตัวเองซ้ำๆ ในฐานะฟังก์ชัน และการประกอบซ้ำๆ นี่แหละคือหัวใจสำคัญของเลข Church

POW := λ b .λ n . n b ^{[ 1 ]}

หรืออีกทางเลือกหนึ่งที่นี่เช่นกัน

เชลยศึก′ := แล ข.แลn . n (MULT ข ) 1

เมื่อทำให้ง่ายขึ้น ก็จะได้ดังนี้

เชลยศึก' := แลมบ์ .แลม .เลฟ . ไม่มี​​

แต่นั่นเป็นเพียงเวอร์ชันขยายความของPOWที่เรามีอยู่แล้วข้างต้น

ฟังก์ชันก่อนหน้าซึ่งระบุโดยสมการสองสมการPRED (SUCC n ) = nและPRED 0 = 0นั้นมีความซับซ้อนกว่ามาก สูตรดังกล่าว

เปรด := แลมบ์ดา . แลมบ์ ฉ .แลมบ์n (และ แล ล . แล ล h . h ( g f )) (แล ะu . x ) (แล ลu . u )

สามารถตรวจสอบความถูกต้องได้โดยการแสดงแบบอุปนัยว่า ถ้าTหมายถึง(λ g .λ h . h ( g f ))แล้วT ^{( n )} (λ u . x ) = (λ h . h ( f ^{( n −1)} ( x )))สำหรับn > 0 นิยามอื่น ๆ ของ PREDอีกสองแบบจะแสดงไว้ด้านล่าง แบบหนึ่งใช้เงื่อนไขและอีกแบบใช้คู่ด้วยฟังก์ชันก่อนหน้า การลบจึงทำได้ง่าย การกำหนด

ย่อย := แลมบ์ .แลม . nเปร็ดม . ,

SUB m nจะให้ผลลัพธ์เป็นm − nเมื่อm > nและ0ในกรณีอื่น ๆ

ตามธรรมเนียมแล้ว ค่าบูลีน TRUEและFALSEจะใช้คำจำกัดความสองแบบต่อไปนี้ (เรียกว่า Church Booleans) :

จริง := λ x .λ y . x

เท็จ := λ x .λ y . y

จากนั้น ด้วยเงื่อนไขแลมบ์ดา 2 ข้อนี้ เราสามารถกำหนดตัวดำเนินการตรรกะบางอย่างได้ (นี่เป็นเพียงสูตรที่เป็นไปได้เท่านั้น นิพจน์อื่นๆ ก็อาจถูกต้องเช่นกัน) ^{[ 22 ]}

และ := λ p .λ q . p q p

หรือ := λ p .λ q . p p q

ไม่ใช่ := λ p . pเท็จ จริง

IFTHENELSE := แลมบ์ ดา .แลมบ . ล . ข . พีอัข

ขณะนี้เราสามารถคำนวณฟังก์ชันตรรกะบางอย่างได้แล้ว ตัวอย่างเช่น:

และจริงเท็จ

≡ (แล ลp . แล ล q . p q p ) จริง เท็จ → _βจริง เท็จ จริง

≡ (แลมบ์x .แลม y . x ) เท็จ จริง → _βเท็จ

และเราจะเห็นว่าAND TRUE FALSEเทียบเท่า กับFALSE

เพรดิเคท (Predicate)คือฟังก์ชันที่ส่งคืนค่าบูลีน เพรดิเคทพื้นฐานที่สุดคือISZEROซึ่งจะส่งคืนค่า TRUEถ้าอาร์กิวเมนต์เป็นเลข Church 0แต่ จะส่งคืน ค่า FALSEถ้าอาร์กิวเมนต์เป็นเลข Church อื่นๆ

ISZERO := แลมบ์ . n (แลมบ์x .FALSE) จริง

述语ต่อไปนี้ทดสอบว่าอาร์กิวเมนต์ตัวแรกน้อยกว่าหรือเท่ากับอาร์กิวเมนต์ตัวที่สองหรือไม่:

LEQ := แลมบ์ .แลมn .ISZERO (SUB มn ) ,

และเนื่องจากm = nถ้าLEQ m nและLEQ n mจึงสามารถสร้าง述语สำหรับความเท่าเทียมกันเชิงตัวเลขได้อย่างง่ายดาย

การมีอยู่ของ述語 (predicates) และคำจำกัดความของ TRUEและFALSEข้างต้นทำให้การเขียนนิพจน์ "if-then-else" ในแคลคูลัสแลมบ์ดาทำได้สะดวก ตัวอย่างเช่น ฟังก์ชันก่อนหน้า (predecessor function) สามารถกำหนดได้ดังนี้:

เปร็ด := แลn . n (แลมบ์ดา g .แลม k .ISZERO ( ก. 1) k (บวก ( g k ) 1)) (แลมบ์v .0) 0

ซึ่งสามารถตรวจสอบได้โดยการแสดงให้เห็นแบบอุปนัยว่าn (λ g .λ k .ISZERO ( g 1) k (PLUS ( g k ) 1)) (λ v .0)คือฟังก์ชัน add n − 1 สำหรับn > 0

คู่ (2-tuple) ประกอบด้วยค่าสองค่า และแสดงด้วยนามธรรมที่คาดหวังตัวจัดการที่จะส่งค่าทั้งสองไปให้ ฟังก์ชันFIRSTจะส่งคืนองค์ประกอบแรกของคู่ และฟังก์ชัน SECONDจะส่งคืนองค์ประกอบที่สอง

PAIR := λ x .λ y .λ f . f x y

ครั้งแรก := แลพี . พี (เอชx . แล ย . x )

ที่สอง := แลมพาร์ . พี (เอชx . แล ย . ย )

โครงสร้างข้อมูลแบบ Linked List สามารถเป็นได้เพียงค่าเดียวคือ NIL ซึ่งหมายถึงรายการว่างเปล่า หรือเป็นคู่ขององค์ประกอบหนึ่ง (เรียกว่าหัว ) และองค์ประกอบที่เล็กกว่า ( เรียกว่า หาง ) ฟังก์ชันตรวจสอบNULLจะคืนค่า TRUEสำหรับค่าNILและคืนค่า FALSEสำหรับรายการที่ไม่ว่างเปล่า

NIL := λ f .TRUE

โมฆะ := แลมพี . p (แลมบ์ดา.แล มบ์ y .FALSE)

หรืออีกทางเลือกหนึ่ง ด้วยNIL := FALSEโครงสร้าง( l (λ h .λ t .λ z . ... h ... t ...) _on_nil_)จะทำให้ไม่จำเป็นต้องทดสอบค่า NULL อย่างชัดเจน:

NIL := λ x .λ y . y

โมฆะ := แลลล . l (แลมบ์h .แลต t .แล ม z .FALSE) จริง

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

Φ := λ p .PAIR (SECOND p ) (SUCC (SECOND p ))

Ψ := λ fp .PAIR (SECOND p ) (f (SECOND p ))

ซึ่งทำให้เราสามารถนำเสนอฟังก์ชันรุ่นก่อนหน้าในรูปแบบที่โปร่งใสที่สุดได้:

PRED := λ n .FIRST ( n (Ψ SUCC) (PAIR 0 0))

  = λ nfx .FIRST ( n (Ψ f ) (PAIR xx ))

การแทนที่คำจำกัดความและการทำให้สมการที่ได้นั้นง่ายขึ้น จะนำไปสู่คำจำกัดความที่กระชับยิ่งขึ้น

  = แลงเอฟเอ็กซ์n (แลrab . rb ( fb )) (แลab . a ) xx

  = แลงเอฟเอ็กซ์n (λ rij . j ( rjf )) (γ ij . x ) II

  = แลงเอฟเอ็กซ์n (λ rij . i ( rjj )) (λ ij . x ) ฉันf

  = แลงเอฟเอ็กซ์n (λ ri . i ( rf )) (γ i . x ) I

(โดยที่  I := λ x . x ) ซึ่งเห็นได้ชัดว่านำกลับไปสู่จุดเริ่มต้น

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

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

(λ f . M ) N

ผู้เขียนมักใช้คำย่อทางไวยากรณ์เช่นlet , ^{[ e ]}เพื่อให้สามารถเขียนข้อความข้างต้นในลำดับที่เข้าใจง่ายกว่า

ให้f = N ในM

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

ข้อจำกัดที่สำคัญอย่างหนึ่งของคำสั่ง let นี้ คือ ชื่อfอาจไม่สามารถอ้างอิงได้ในNเนื่องจากNอยู่นอกขอบเขตของการผูกนามธรรมfซึ่งก็คือMนั่นหมายความว่าไม่สามารถเขียนนิยามฟังก์ชันแบบเรียกซ้ำด้วยlet ได้โครงสร้าง letrec [ ^{f ] จะ}ช่วยให้สามารถเขียนนิยามฟังก์ชันแบบเรียกซ้ำได้ โดยที่ขอบเขตของการผูกนามธรรมfครอบคลุม ทั้ง NและM หรือ อาจใช้ การประยุกต์ใช้กับตัวเองแบบเดียวกับที่นำไปสู่​​Y combinator ก็ได้

Recursion is when a function invokes itself. What would a value be which were to represent such a function? It has to refer to itself somehow inside itself, just as the definition refers to itself inside itself. If this value were to contain itself by value, it would have to be of infinite size, which is impossible. Other notations, which support recursion natively, overcome this by referring to the function by name inside its definition. Lambda calculus cannot express this, since in it there simply are no names for terms to begin with, only arguments' names, ie parameters in abstractions. Thus, a lambda expression can receive itself as its argument and refer to (a copy of) itself via the corresponding parameter's name. This will work fine in case it was indeed called with itself as an argument. For example, (λ x . x x ) E = ( EE ) will express recursion when E is an abstraction which is applying its parameter to itself inside its body to express a recursive call. เนื่องจากพารามิเตอร์นี้รับ ค่าเป็น Eดังนั้นการประยุกต์ใช้กับตัวเองจึงเหมือนเดิม( EE )อีกครั้ง

ตัวอย่างที่เป็นรูปธรรมคือ พิจารณาฟังก์ชันแฟกทอเรียลF( n )ซึ่งนิยามแบบเวียนเกิดโดย

F( n ) = 1 ถ้าn = 0; มิฉะนั้นn × F( n − 1 )

ในนิพจน์แลมบ์ดาซึ่งใช้แทนฟังก์ชันนี้พารามิเตอร์ (โดยทั่วไปคือพารามิเตอร์ตัวแรก) จะถูกสมมติว่ารับนิพจน์แลมบ์ดาเองเป็นค่า ดังนั้นการเรียกใช้โดยส่งตัวมันเองเป็นอาร์กิวเมนต์ตัวแรกจะเท่ากับการเรียกซ้ำ ดังนั้นเพื่อให้เกิดการเรียกซ้ำ อาร์กิวเมนต์ที่ตั้งใจให้ชี้ไปยังตัวเอง (เรียกว่าsในที่นี้ ซึ่งคล้ายกับคำว่า "self" หรือ "self-applying") จะต้องถูกส่งไปยังตัวมันเองภายในตัวฟังก์ชัน ณ จุดเรียกซ้ำเสมอ:

E := λ s . λ n .(1, ถ้าn = 0; มิฉะนั้นn × ( s s ( n −1)))

โดยที่ ssn = F n = EE n จะต้องคงอยู่ ดังนั้น s = E และ

F := (λ x . x x ) E = EE

และเรามี

F = EE = λ n .(1 ถ้าn = 0; มิฉะนั้นn × (EE ( n −1)))

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

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

วิธีการเรียกใช้ฟังก์ชันด้วยตนเองนี้ช่วยแก้ปัญหาได้ แต่ต้องเขียนการเรียกซ้ำแต่ละครั้งใหม่ให้เป็นการเรียกใช้ฟังก์ชันด้วยตนเอง เราต้องการวิธีแก้ปัญหาแบบทั่วไป โดยไม่ต้องเขียนใหม่เลย:

G := λ r . λ n .(1, ถ้าn = 0; มิฉะนั้นn × ( r ( n −1)))

โดยที่ r x = F x = G r x จะต้องคงอยู่ ดังนั้น r = G r =: ตรึง G และ

F := FIX G โดยที่ FIX g = ( rโดยที่r = g r ) = g (FIX g )

ดังนั้น FIX G = G (FIX G) = (λ n .(1, ถ้าn = 0; มิฉะนั้นn × ((FIX G) ( n −1))))

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

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

Y  := แลมบ์ดา ก .(แลมx . ก ( x x )) (แลมบ์. ก . ( x x ))

ในแคลคูลัสแลมบ์ดาY g เป็นจุดตรึงของgเนื่องจากมันขยายออกเป็น:

วายจี

~> (λ h .(λ x . h ( x x )) (λ x . h ( x x ))) g

~> (λ x . g ( x x )) (λ x . g ( x x ))

~> g ((λ x . g ( x x )) (λ x . g ( x x )))

<~ g ( Y g )

ทีนี้ เพื่อเรียกฟังก์ชันแฟกทอเรียลแบบเรียกซ้ำสำหรับอาร์กิวเมนต์nเราจะเรียก( Y G) nโดยกำหนดให้n = 4 ตัวอย่างเช่น จะได้ดังนี้:

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

เมื่อY combinatorถูกเขียนโค้ดโดยตรงในภาษาโปรแกรมที่เข้มงวดลำดับการประเมินแบบประยุกต์ใช้ในภาษาดังกล่าวจะทำให้เกิดความพยายามที่จะขยายการประยุกต์ใช้ภายในอย่างเต็มที่ก่อนกำหนด ส่งผลให้เกิดstack overflowหรือในกรณีของการเพิ่มประสิทธิภาพ tail callจะทำให้เกิดการวนลูปไม่สิ้นสุด^{[ 24 ]}ตัวแปรที่ล่าช้าของ Y คือZ combinatorสามารถใช้ในภาษาดังกล่าวได้ โดยมีการประยุกต์ใช้ภายในซ่อนอยู่เบื้องหลังนามธรรมเพิ่มเติมผ่านการขยาย etaเช่นดังนั้นจึงป้องกันการขยายตัวก่อนกำหนด: ^{[ 25 ]}${\displaystyle (xx)}$${\displaystyle (\lambda v.xxv)}$

${\displaystyle Z=\lambda f.(\lambda x.f(\lambda v.xxv))\ (\lambda x.f(\lambda v.xxv))\ .}$

คำศัพท์บางคำมีชื่อที่ยอมรับกันโดยทั่วไป: ^{[ 26 ] [ 27 ] [ 28 ]}

I  := λ x . x

ส  := แลมบ์ดาx . แลมบ์ . เลซ . xz ( yz )​​

K  := λ x .λ y . x

ข  := แลมบ์ดาx .แลมบ์ . เล ซ . x ( y z )

C  := λ x .λ y .λ z . x z y

W  := λ x .λ y . x y y

ωหรือΔหรือU  := λ x . x x

Ω  := ω ω

Iคือฟังก์ชันเอกลักษณ์ SKและ BCKWเป็น ระบบ แคลคูลัสคอมบินาเตอร์ ที่สมบูรณ์ ซึ่งสามารถแสดงเทอมแลมบ์ดาใดๆ ก็ได้ - ดู ส่วนถัดไปΩคือ UUซึ่งเป็นเทอมที่เล็กที่สุดที่ไม่มีรูปแบบปกติ YIก็เป็นเทอมแบบเดียวกันอีกเทอมหนึ่ง Yเป็นค่ามาตรฐานและนิยามไว้ข้างต้นและยังสามารถนิยามได้เป็นY = BU (CBU)ดังนั้น Y g=g( Y g)ค่า TRUEและ FALSEที่นิยามไว้ข้างต้นมักจะย่อเป็น Tและ F

ถ้าNเป็นเทอมแลมบ์ดาที่ไม่มีนามธรรม แต่มีค่าคงที่ที่มีชื่อ ( คอมบินาเตอร์ ) อยู่ภายใน ก็จะมีเทอมแลมบ์ดาT(x, N) ซึ่งเทียบเท่ากับ λx.Nแต่ขาดนามธรรม ( ยกเว้นในส่วนของค่าคงที่ที่มีชื่อ หากถือว่าค่าคงที่เหล่านั้นไม่ใช่อะตอมิก) นอกจากนี้ยังสามารถมองได้ว่าเป็นการทำให้ตัวแปรเป็นนิรนาม เนื่องจากT ( x , N ) จะลบ xออกจากN ทั้งหมด ในขณะที่ยังคงอนุญาตให้แทนที่ค่าอาร์กิวเมนต์ลงในตำแหน่งที่Nมีx อยู่ ฟังก์ชันการแปลงTสามารถกำหนดได้ดังนี้:

T ( x , x ) := I

T ( x , N ) := K Nถ้าxไม่เป็นอิสระในN

T ( x , M N ) := S T ( x , M ) T ( x , N )

ไม่ว่าในกรณีใด เทอมในรูปแบบT ( x , N ) Pจะถูกลดรูปโดยให้ตัวรวมเริ่มต้นI , KหรือSรับอาร์กิวเมนต์Pเช่นเดียวกับการลดรูป β ของ(λ x . N ) PจะทำIจะส่งคืนอาร์กิวเมนต์นั้นK Nจะทิ้งอาร์กิวเมนต์ไป เช่นเดียวกับ(λ x . N )เมื่อxไม่มีอยู่ในNอย่าง อิสระ Sจะส่งอาร์กิวเมนต์ต่อไปยังเทอมย่อยทั้งสองของการประยุกต์ใช้ จากนั้นจึงใช้ผลลัพธ์ของเทอมแรกกับผลลัพธ์ของเทอมที่สอง เช่นเดียวกับ(λ x . MN ) Pที่เหมือนกับ((λ x . M ) P ) ( (λ x . N ) P )

ตัวรวมBและCคล้ายกับSแต่ส่งผ่านอาร์กิวเมนต์ไปยังเทอมย่อยเพียงเทอมเดียวของการประยุกต์ใช้ ( Bไปยังเทอมย่อย "อาร์กิวเมนต์" และCไปยังเทอมย่อย "ฟังก์ชัน") จึงช่วยประหยัดK ในภายหลัง หากไม่มีการปรากฏของxในเทอมย่อยใดเทอมหนึ่ง เมื่อเปรียบเทียบกับBและC ตัวรวม Sนั้นรวมฟังก์ชันการทำงานสองอย่างเข้าด้วยกัน คือ การจัดเรียงอาร์กิวเมนต์ใหม่ และการทำซ้ำอาร์กิวเมนต์เพื่อให้สามารถใช้ในสองที่ ตัว รวม Wทำเพียงอย่างหลังเท่านั้น ทำให้ได้ระบบ B, C, K, Wเป็นทางเลือกแทนแคลคูลัสตัวรวม SKI

แคลคูลัสแลมบ์ดาแบบมีประเภทคือรูปแบบ ที่มีประเภท ซึ่งใช้สัญลักษณ์แลมบ์ดา ( ) เพื่อแสดงถึงนามธรรมของฟังก์ชันนิรนาม ในบริบทนี้ ประเภทมักจะเป็นวัตถุที่มีลักษณะทางไวยากรณ์ซึ่งถูกกำหนดให้กับเทอมแลมบ์ดา ลักษณะที่แท้จริงของประเภทขึ้นอยู่กับแคลคูลัสที่พิจารณา (ดูประเภทของแคลคูลัสแลมบ์ดาแบบมีประเภท ) จากมุมมองหนึ่ง แคลคูลัสแลมบ์ดาแบบมีประเภทสามารถมองได้ว่าเป็นการปรับปรุงแคลคูลัสแลมบ์ดาแบบไม่มีประเภท แต่จากมุมมองอื่น พวกมันยังสามารถถือได้ว่าเป็นทฤษฎีพื้นฐานมากกว่า และแคลคูลัสแลมบ์ดาแบบไม่มีประเภทเป็นกรณีพิเศษที่มีเพียงประเภทเดียว^{[ 29 ]}${\displaystyle \lambda }$

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

แคลคูลัสแลมบ์ดาแบบมีประเภทมีความเกี่ยวข้องอย่างใกล้ชิดกับตรรกะทางคณิตศาสตร์และทฤษฎีการพิสูจน์ผ่านไอโซมอร์ฟิซึมของเคอร์รี-โฮเวิร์ดและสามารถถือได้ว่าเป็นภาษาภายในของคลาสของหมวดหมู่เช่น แคลคูลัสแลมบ์ดาแบบมีประเภทอย่างง่ายเป็นภาษาของหมวดหมู่ปิดแบบคาร์ทีเซียน (CCC) ^{[ 30 ]}

ไม่ว่าเทอมนั้นจะเป็นเทอมปกติหรือไม่ และต้องดำเนินการมากน้อยเพียงใดในการทำให้เป็นเทอมปกติหากเป็นเทอมปกติ ก็ขึ้นอยู่กับกลยุทธ์การลดที่ใช้เป็นอย่างมาก กลยุทธ์การลดแคลคูลัสแลมบ์ดาทั่วไป ได้แก่: ^{[ 31 ] [ 32 ] [ 33 ]}

ลำดับปกติ

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

คำสั่งการสมัคร

รีเดกซ์ภายในสุดซ้ายสุดจะถูกลดรูปก่อน ดังนั้น อาร์กิวเมนต์ของฟังก์ชันจึงถูกลดรูปก่อนที่จะถูกนำไปแทนในฟังก์ชันเสมอ ซึ่งแตกต่างจากการลดรูปตามลำดับปกติ การลดรูปตามลำดับการประยุกต์ใช้ อาจไม่สามารถหาฟอร์มเบต้าปกติของนิพจน์ได้ แม้ว่าจะมีฟอร์มปกติเช่นนั้นอยู่ก็ตาม ตัวอย่างเช่น เทอมจะถูกลดรูปเป็นตัวมันเองโดยการลดรูปตามลำดับการประยุกต์ใช้ ในขณะที่การลดรูปตามลำดับปกติจะลดรูปให้เป็นรูปแบบเบต้าปกติ${\displaystyle (\;\lambda x.y\;\;(\lambda z.(zz)\;\lambda z.(zz))\;)}$${\displaystyle y}$

การลดเบต้าแบบสมบูรณ์

รีเดกซ์ใดๆ ก็สามารถลดทอนได้ตลอดเวลา ซึ่งหมายความว่าโดยพื้นฐานแล้วไม่มีกลยุทธ์การลดทอนใดๆ ที่เฉพาะเจาะจง กล่าวคือ ในแง่ของการลดทอนนั้น "ไม่มีอะไรแน่นอน"

กลยุทธ์การลดแบบอ่อนไม่สามารถลดได้ภายใต้นามธรรมแลมบ์ดา:

เรียกตามค่า

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

เรียกชื่อตามที่กำหนด

เช่นเดียวกับลำดับปกติ แต่ไม่มีการลดรูปใด ๆ เกิดขึ้นภายในนามธรรม ตัวอย่างเช่นλ x .(λ y . y ) xอยู่ในรูปแบบปกติตามกลยุทธ์นี้ แม้ว่าจะมี redex (λ y . y ) x อยู่ด้วย ก็ตาม

กลยุทธ์การแบ่งปันช่วยลดการคำนวณที่ "เหมือนกัน" ในแบบขนาน:

การลดลงที่เหมาะสมที่สุด

ตามลำดับปกติ แต่การคำนวณที่มีป้ายกำกับเดียวกันจะถูกลดทอนพร้อมกัน

เรียกใช้ตามความจำเป็น

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

ไม่มีอัลกอริทึมใดที่รับนิพจน์แลมบ์ดา 2 ตัวเป็นอินพุตและส่งออกTRUEหรือFALSEขึ้นอยู่กับว่านิพจน์หนึ่งลดรูปเป็นอีกนิพจน์หนึ่งหรือไม่^{[ 15 ]} กล่าว ให้แม่นยำยิ่งขึ้น ไม่มีฟังก์ชันที่คำนวณได้ ใด ที่สามารถตัดสินคำถามนี้ได้ นี่เป็นปัญหาแรกในประวัติศาสตร์ที่สามารถพิสูจน์ได้ว่าไม่สามารถตัดสินได้ ตามปกติสำหรับการพิสูจน์ดังกล่าว คำว่า " คำนวณได้"หมายถึงคำนวณได้โดยแบบจำลองการคำนวณ ใดๆ ที่สมบูรณ์แบบทัวริงอันที่จริง ความสามารถในการคำนวณสามารถกำหนดได้ผ่านแคลคูลัสแลมบ์ดา: ฟังก์ชันF : N → Nของจำนวนธรรมชาติเป็นฟังก์ชันที่คำนวณได้ก็ต่อเมื่อมีนิพจน์แลมบ์ดาf อยู่ เช่นนั้นสำหรับทุกคู่ของx , yในN , F ( x )= yก็ต่อเมื่อf x  = _β yโดยที่xและyเป็นตัวเลขของ Churchที่สอดคล้องกับxและyตามลำดับ และ = _βหมายถึงความเท่าเทียมกันกับการลดรูป β ดูวิทยานิพนธ์ Church–Turingสำหรับแนวทางอื่นๆ ในการกำหนดความสามารถในการคำนวณและความเท่าเทียมกัน  

การพิสูจน์ความไม่สามารถคำนวณได้ของเชิร์ชเริ่มต้นด้วยการลดปัญหาลงเหลือเพียงการพิจารณาว่านิพจน์แลมบ์ดาที่กำหนดให้มีรูปแบบปกติ หรือ ไม่ จากนั้นเขาสมมติว่า述语นี้สามารถคำนวณได้ และด้วยเหตุนี้จึงสามารถแสดงออกมาในแคลคูลัสแลมบ์ดาได้ โดยอาศัยงานก่อนหน้านี้ของคลีนและสร้างหมายเลขเกอเดลสำหรับนิพจน์แลมบ์ดา เขาได้สร้างนิพจน์แลมบ์ดาeที่สอดคล้องกับการพิสูจน์ทฤษฎีบทความไม่สมบูรณ์ข้อแรกของเกอเดล อย่างใกล้ชิด หาก นำ eไปใช้กับหมายเลขเกอเดลของตัวเอง จะเกิดข้อขัดแย้งขึ้น

แนวคิดเรื่องความซับซ้อนในการคำนวณสำหรับแคลคูลัสแลมบ์ดาค่อนข้างยุ่งยาก เพราะต้นทุนของการลด β อาจแตกต่างกันไปขึ้นอยู่กับวิธีการใช้งาน^{[ 34 ]} กล่าวคือ ต้องหาตำแหน่งของการเกิดขึ้นทั้งหมดของตัวแปรที่ถูกผูกไว้Vในนิพจน์Eซึ่งหมายถึงต้นทุนด้านเวลา หรือต้องติดตามตำแหน่งของตัวแปรอิสระด้วยวิธีใดวิธีหนึ่ง ซึ่งหมายถึงต้นทุนด้านพื้นที่ การค้นหาตำแหน่งของVในE อย่างง่ายๆ จะ ใช้ เวลา O ( n )ตามความยาวnของEสตริงไดเร็กเตอร์เป็นแนวทางแรกๆ ที่แลกเปลี่ยนต้นทุนด้านเวลานี้กับการใช้พื้นที่แบบกำลังสอง^{[ 35 ]}โดยทั่วไปแล้วสิ่งนี้นำไปสู่การศึกษาระบบที่ใช้การแทนที่แบบชัดเจน

ในปี 2014 ได้มีการแสดงให้เห็นว่าจำนวนขั้นตอนการลด β ที่ใช้โดยการลดลำดับปกติเพื่อลดเทอมนั้นเป็น แบบจำลองต้นทุนเวลา ที่สมเหตุสมผลกล่าวคือ การลดสามารถจำลองบนเครื่องทัวริงได้ในเวลาที่เป็นสัดส่วนพหุนามกับจำนวนขั้นตอน^{[ 36 ]}นี่เป็นปัญหาที่เปิดค้างมานานเนื่องจากการระเบิดของขนาดการมีอยู่ของเทอมแลมบ์ดาซึ่งมีขนาดเพิ่มขึ้นแบบเลขชี้กำลังสำหรับการลด β แต่ละครั้ง ผลลัพธ์นี้แก้ปัญหานี้ได้โดยการทำงานกับการแสดงแทนร่วมกันแบบกระชับ ผลลัพธ์นี้แสดงให้เห็นอย่างชัดเจนว่าปริมาณพื้นที่ที่จำเป็นในการประเมินเทอมแลมบ์ดาไม่ได้เป็นสัดส่วนกับขนาดของเทอมในระหว่างการลด ปัจจุบันยังไม่ทราบว่ามาตรวัดความซับซ้อนของพื้นที่ที่ดีควรเป็นอย่างไร^{[ 37 ]}

แบบจำลองที่ไม่สมเหตุสมผลไม่ได้หมายความว่าไม่มีประสิทธิภาพเสมอไปการลดขนาดที่เหมาะสมจะลดการคำนวณทั้งหมดที่มีป้ายกำกับเดียวกันในขั้นตอนเดียว หลีกเลี่ยงการทำงานซ้ำซ้อน แต่จำนวนขั้นตอนการลดขนาด β แบบขนานเพื่อลดเทอมที่กำหนดไปยังรูปแบบปกติจะเป็นเชิงเส้นโดยประมาณตามขนาดของเทอม ซึ่งเล็กเกินไปที่จะเป็นมาตรวัดต้นทุนที่สมเหตุสมผล เนื่องจากเครื่องทัวริงใดๆ ก็สามารถเข้ารหัสในแคลคูลัสแลมบ์ดาได้ในขนาดที่เป็นสัดส่วนเชิงเส้นกับขนาดของเครื่องทัวริง ต้นทุนที่แท้จริงของการลดเทอมแลมบ์ดาไม่ได้เกิดจากการลดขนาด β โดยตรง แต่เกิดจากการจัดการการทำซ้ำของ redex ในระหว่างการลดขนาด β ^{[ 38 ]}ยังไม่เป็นที่ทราบแน่ชัดว่าการใช้งานการลดขนาดที่เหมาะสมนั้นสมเหตุสมผลหรือไม่เมื่อวัดเทียบกับแบบจำลองต้นทุนที่สมเหตุสมผล เช่น จำนวนขั้นตอนซ้ายสุด-นอกสุดไปยังรูปแบบปกติ แต่ได้แสดงให้เห็นแล้วสำหรับส่วนย่อยของแคลคูลัสแลมบ์ดาว่าอัลกอริทึมการลดขนาดที่เหมาะสมนั้นมีประสิทธิภาพและมีค่าใช้จ่ายสูงสุดเพียงกำลังสองเมื่อเทียบกับซ้ายสุด-นอกสุด^{[ 37 ]}นอกจากนี้ การนำต้นแบบ BOHM มาใช้ในการลดค่าที่เหมาะสมที่สุดยังทำได้ดีกว่าทั้งCaml Light และ Haskell ในส่วนของเงื่อนไขแลมบ์ดาบริสุทธิ์^{[ 38 ]}

ตามที่ Peter Landinชี้ให้เห็นในบทความปี 1965 เรื่อง " ความสอดคล้องกันระหว่างALGOL 60และสัญกรณ์แลมบ์ดาของ Church " ^{[ 39 ]} ภาษา การเขียนโปรแกรมเชิงขั้นตอนแบบลำดับสามารถเข้าใจได้ในแง่ของแคลคูลัสแลมบ์ดา ซึ่งเป็นกลไกพื้นฐานสำหรับนามธรรมเชิงขั้นตอนและการประยุกต์ใช้ขั้นตอน (โปรแกรมย่อย)

ตัวอย่างเช่น ในภาษา Pythonฟังก์ชัน "square" สามารถแสดงได้ในรูปนิพจน์แลมบ์ดา ดังนี้:

( แลมบ์ดาx : x ** 2 )

ตัวอย่างข้างต้นเป็นนิพจน์ที่ประเมินค่าได้เป็นฟังก์ชันชั้นหนึ่ง สัญลักษณ์นี้lambdaสร้างฟังก์ชันนิรนาม โดยรับรายการชื่อพารามิเตอร์— xในกรณีนี้คืออาร์กิวเมนต์เพียงตัวเดียว—และนิพจน์ที่จะถูกประเมินค่าเป็นส่วนเนื้อหาของฟังก์ชัน ฟังก์ชันx**2นิรนามบางครั้งเรียกว่านิพจน์แลมบ์ดา

ภาษา Pascalและภาษาเชิงคำสั่งอื่นๆ อีกมากมายได้สนับสนุนการส่งผ่านโปรแกรมย่อยเป็นอาร์กิวเมนต์ไปยังโปรแกรมย่อยอื่นๆ ผ่านกลไกของตัวชี้ฟังก์ชัน มานานแล้ว อย่างไรก็ตาม ตัวชี้ฟังก์ชันเป็นเงื่อนไขที่ไม่เพียงพอสำหรับฟังก์ชันที่จะเป็น ชนิดข้อมูล ระดับเฟิร์สคลาสเพราะฟังก์ชันจะเป็นชนิดข้อมูลระดับเฟิร์สคลาสก็ต่อเมื่อสามารถสร้างอินสแตนซ์ใหม่ของฟังก์ชันได้ในขณะรันไทม์การสร้างฟังก์ชันในขณะรันไทม์ดังกล่าวได้รับการสนับสนุนในSmalltalk , JavaScript , Wolfram Languageและล่าสุดในScala , Eiffel (ในฐานะเอเจนต์), C# (ในฐานะดีลีเกต) และC++11เป็นต้น

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

ข้อเท็จจริงที่ว่าเทอมในแคลคูลัสแลมบ์ดาทำหน้าที่เป็นฟังก์ชันบนเทอมแคลคูลัสแลมบ์ดาอื่นๆ และแม้กระทั่งบนตัวมันเอง ทำให้เกิดคำถามเกี่ยวกับความหมายของแคลคูลัสแลมบ์ดา เราสามารถกำหนดความหมายที่สมเหตุสมผลให้กับเทอมแคลคูลัสแลมบ์ดาได้หรือไม่? ความหมายตามธรรมชาติคือการหาเซตDที่สม isomorphic กับปริภูมิฟังก์ชันD → Dของฟังก์ชันบนตัวมันเอง อย่างไรก็ตาม ไม่มีเซตD ที่ไม่ใช่เซตว่าง ที่สามารถมีอยู่ได้ เนื่องจาก ข้อจำกัด ด้านจำนวนสมาชิกเพราะเซตของฟังก์ชันทั้งหมดจากDไปยังDมีจำนวนสมาชิกมากกว่าDเว้นแต่ว่าDจะเป็นเซตที่มี สมาชิกเพียงตัวเดียว

ในช่วงทศวรรษ 1970 Dana Scottได้แสดงให้เห็นว่าหากพิจารณา เฉพาะ ฟังก์ชันต่อเนื่อง เท่านั้น จะสามารถค้นหาเซตหรือ โดเมนDที่มีคุณสมบัติที่ต้องการได้ ซึ่งจะเป็นแบบจำลองสำหรับแคลคูลัสแลมบ์ดา^{[ 40 ]}

งานวิจัยนี้ยังเป็นพื้นฐานสำหรับความหมายเชิงสัญลักษณ์ของภาษาโปรแกรม อีกด้วย

ส่วนขยายเหล่านี้อยู่ในแลมบ์ดาคิวบ์ :

• แคลคูลัสแลมบ์ดาแบบมีตัวแปรกำหนดประเภท – แคลคูลัสแลมบ์ดาที่มีตัวแปรกำหนดประเภท (และฟังก์ชัน)
• ระบบ F – แคลคูลัสแลมบ์ดาแบบมีชนิดข้อมูลและตัวแปรชนิดข้อมูล
• แคลคูลัสของการสร้าง – แคลคูลัสแลมบ์ดาแบบมีชนิดข้อมูล โดยที่ชนิดข้อมูลเป็นค่าระดับแรก

ระบบที่เป็นทางการเหล่านี้เป็นส่วนขยายของแคลคูลัสแลมบ์ดาที่ไม่รวมอยู่ในลูกบาศก์แลมบ์ดา:

• แคลคูลัสแลมบ์ดาแบบไบนารี – แคลคูลัสแลมบ์ดาเวอร์ชันหนึ่งที่มีการรับ/ส่งข้อมูล (I/O) แบบไบนารี การเข้ารหัสเทอมแบบไบนารี และเครื่องจักรสากลที่กำหนดไว้
• แคลคูลัสแลมบ์ดา-มิว – ส่วนขยายของแคลคูลัสแลมบ์ดาสำหรับใช้ในการแก้ตรรกศาสตร์คลาสสิก

ระบบที่เป็นทางการเหล่านี้เป็นรูปแบบต่างๆ ของแคลคูลัสแลมบ์ดา:

• แคลคูลัสแคปปา – อนาล็อกอันดับหนึ่งของแคลคูลัสแลมบ์ดา

ระบบที่เป็นทางการเหล่านี้เกี่ยวข้องกับแคลคูลัสแลมบ์ดา:

• ตรรกศาสตร์เชิงผสม – สัญลักษณ์สำหรับตรรกศาสตร์ทางคณิตศาสตร์ที่ไม่มีตัวแปร
• แคลคูลัสคอมบินเนเตอร์ SKI – ระบบการคำนวณที่ใช้ คอมบินเนเตอร์ S , KและIซึ่งเทียบเท่ากับแคลคูลัสแลมบ์ดา แต่สามารถลดรูปได้โดยไม่ต้องแทนที่ตัวแปร

• Abelson, Harold และ Gerald Jay Sussman. โครงสร้างและการตีความโปรแกรมคอมพิวเตอร์ . สำนักพิมพ์ MIT . ISBN 0-262-51087-1.
• บาเรนเร็กต์, เฮนดริก ปีเตอร์ แคลคูลัสแลมบ์ดาเบื้องต้น
• Barendregt, Hendrik Pieter, ผลกระทบของแคลคูลัสแลมบ์ดาในตรรกศาสตร์และวิทยาศาสตร์คอมพิวเตอร์วารสารตรรกศาสตร์เชิงสัญลักษณ์ เล่มที่ 3 ฉบับที่ 2 มิถุนายน 1997
• Barendregt, Hendrik Pieter, The Type Free Lambda Calculusหน้า 1091–1132 ของHandbook of Mathematical Logic , North-Holland (1977) ISBN 0-7204-2285-X
• Cardone, Felice และ Hindley, J. Roger, 2006. ประวัติของแคลคูลัสแลมบ์ดาและตรรกศาสตร์เชิงผสมเก็บถาวรเมื่อ 2021-05-06 ที่Wayback Machineใน Gabbay และ Woods (บรรณาธิการ), Handbook of the History of Logic , เล่ม 5. Elsevier.
• Church, Alonzo, ปัญหาที่แก้ไม่ได้ของทฤษฎีจำนวนเบื้องต้น , American Journal of Mathematics , 58 (1936), หน้า 345–363. บทความนี้มีหลักฐานพิสูจน์ว่าความเท่าเทียมกันของนิพจน์แลมบ์ดาโดยทั่วไปไม่สามารถตัดสินได้
• Church, Alonzo (1941). The Calculi of Lambda-Conversion . Princeton: Princeton University Press . สืบค้นเมื่อ2020-04-14 .( ISBN) 978-0-691-08394-0)
• Frink Jr., Orrin (1944). "บทวิจารณ์: The Calculi of Lambda-Conversionโดย Alonzo Church" (PDF) . Bulletin of the American Mathematical Society . 50 (3): 169– 172. doi : 10.1090/s0002-9904-1944-08090-7 .
• Kleene, Stephen, ทฤษฎีจำนวนเต็มบวกในตรรกศาสตร์เชิงรูปธรรม , American Journal of Mathematics , 57 (1935), หน้า 153–173 และ 219–244 ประกอบด้วยนิยามแคลคูลัสแลมบ์ดาของฟังก์ชันที่คุ้นเคยหลายฟังก์ชัน
• Landin, Peter , การติดต่อสื่อสารระหว่าง ALGOL 60 และสัญกรณ์แลมบ์ดาของ Church , Communications of the ACM , เล่ม 8, ฉบับที่ 2 (1965), หน้า 89–101 สามารถดูได้จากเว็บไซต์ ACMบทความคลาสสิกที่เน้นความสำคัญของแคลคูลัสแลมบ์ดาในฐานะพื้นฐานสำหรับภาษาโปรแกรม
• ลาร์สัน, จิม, บทนำสู่แคลคูลัสแลมบ์ดาและภาษา Scheme : บทนำอย่างง่ายสำหรับโปรแกรมเมอร์
• Michaelson, Greg (10 เมษายน 2556). บทนำสู่การเขียนโปรแกรมเชิงฟังก์ชันผ่านแคลคูลัสแลมบ์ดา . สำนักพิมพ์ Courier Corporation. ISBN 978-0-486-28029-5.^{[ 1 ]}
• Schalk, A. และ Simmons, H. (2005) บทนำเกี่ยวกับแคลคูลัสแลมบ์ดาและเลขคณิต พร้อมแบบฝึกหัดที่เหมาะสมบันทึกประกอบการเรียนในหลักสูตรปริญญาโทสาขาตรรกศาสตร์คณิตศาสตร์ มหาวิทยาลัยแมนเชสเตอร์
• de Queiroz, Ruy JGB (2008). "เกี่ยวกับกฎการลดรูป ความหมายตามการใช้งาน และความหมายเชิงทฤษฎีการพิสูจน์" Studia Logica . 90 (2): 211– 247. doi : 10.1007/s11225-008-9150-5 . S2CID  11321602 .บทความนี้ให้พื้นฐานทางรูปแบบแก่แนวคิด "ความหมายคือการใช้งาน" ซึ่งแม้จะอิงตามการพิสูจน์ แต่ก็แตกต่างจากความหมายเชิงทฤษฎีการพิสูจน์ตามแบบฉบับของ Dummett–Prawitz เนื่องจากถือว่าการลดทอนเป็นกฎที่ให้ความหมาย
• แฮงกิน, คริส, บทนำเกี่ยวกับแคลคูลัสแลมบ์ดาสำหรับนักวิทยาศาสตร์คอมพิวเตอร์, ISBN 0954300653

หนังสือ/ตำราสำหรับนักศึกษาปริญญาโท

• Sørensen, Morten Heine และ Urzyczyn, Paweł (2006), Lectures on the Curry–Howard isomorphism , Elsevier, ISBN 0-444-52077-5เป็นเอกสารทางวิชาการล่าสุดที่ครอบคลุมหัวข้อหลักของแคลคูลัสแลมบ์ดา ตั้งแต่แบบไร้ประเภท ไปจนถึงแคลคูลัสแลมบ์ดาแบบมี ประเภทส่วนใหญ่ รวมถึงการพัฒนาล่าสุด เช่นระบบประเภทบริสุทธิ์และแลมบ์ดาคิวบ์ อย่างไรก็ตาม เอกสาร นี้ไม่ได้กล่าวถึงส่วนขยายของการกำหนดประเภทย่อย
• เพียร์ซ, เบนจามิน (2002), ประเภทและภาษาการเขียนโปรแกรม , สำนักพิมพ์ MIT, ISBN 0-262-16209-1เนื้อหาครอบคลุมแคลคูลัสแลมบ์ดาจากมุมมองของระบบประเภทเชิงปฏิบัติ หัวข้อบางอย่างเช่นประเภทที่ขึ้นอยู่กับตัวแปรอื่นจะถูกกล่าวถึงเพียงเล็กน้อย แต่การกำหนดประเภทย่อยเป็นหัวข้อสำคัญ

เอกสาร

• บทนำโดยย่อเกี่ยวกับแคลคูลัสแลมบ์ดา ( PDF ) โดย อาคิม จุง
• ลำดับเหตุการณ์ของแคลคูลัสแลมบ์ดา (ไฟล์ PDF ) โดย ดานา สก็อตต์
• คู่มือแนะนำแคลคูลัสแลมบ์ดา (ไฟล์ PDF ) โดย ราอูล โรฮาส
• เอกสารประกอบการบรรยายเรื่องแคลคูลัสแลมบ์ดา (ไฟล์ PDF ) โดย ปีเตอร์ เซลลิงเกอร์
• แคลคูลัสแลมบ์ดากราฟิกโดย Marius Buliga
• บทความ เรื่อง "Lambda Calculus as a Workflow Model"โดย Peter Kelly, Paul Coddington และ Andrew Wendelborn กล่าวถึงการลดรูปกราฟเป็นวิธีการทั่วไปในการประเมินนิพจน์แลมบ์ดา และอภิปรายถึงการประยุกต์ใช้แคลคูลัสแลมบ์ดาสำหรับการประมวลผลแบบกระจาย (เนื่องจาก คุณสมบัติ Church–Rosserซึ่งช่วยให้สามารถ ลดรูปกราฟ แบบขนานสำหรับนิพจน์แลมบ์ดาได้)

วิกิมีเดียคอมมอนส์มีสื่อที่เกี่ยวข้องกับแคลคูลัสแลมบ์ดา

• Graham Hutton, Lambda Calculus , วิดีโอสั้น (12 นาที) จาก Computerphile เกี่ยวกับ Lambda Calculus
• เฮลมุท บรันด์ล, บทนำทีละขั้นตอนสู่แคลคูลัสแลมบ์ดา
• "แลมบ์ดาแคลคูลัส" , สารานุกรมคณิตศาสตร์ , EMS Press , 2001 [1994]
• เดวิด ซี. คีนาน, การวิเคราะห์นกม็อกกิ้งเบิร์ด: สัญกรณ์กราฟิกสำหรับแคลคูลัสแลมบ์ดาพร้อมการลดรูปแอนิเมชัน
• แอล. อัลลิสันตัวอย่างแคลคูลัสปฏิบัติการบางตัวอย่าง
• จอร์จ พี. โลเชฟสกี, แคลคูลัสแลมบ์ดาและ A++
• เบร็ต วิคเตอร์, ไข่จระเข้: เกมปริศนาที่อิงจากแคลคูลัสแลมบ์ดา
• แคลคูลัสแลมบ์ดาถูกเก็บถาวรเมื่อวันที่ 14 ตุลาคม 2012 ที่Wayback Machineบนเว็บไซต์ของ Safalra และถูกเก็บถาวรอีกครั้งเมื่อวันที่ 2 พฤษภาคม 2021 ที่ Wayback Machine
• LCI Lambda Interpreter คือตัวแปลภาษาแคลคูลัสบริสุทธิ์ที่เรียบง่ายแต่ทรงพลัง
• ลิงก์ไปยัง Lambda Calculus บน Lambda-the-Ultimate
• Mike Thyer, Lambda Animator , แอปเพล็ต Java แบบกราฟิกที่แสดงให้เห็นถึงกลยุทธ์การลดขนาดทางเลือกต่างๆ
• การนำแคลคูลัสแลมบ์ดาไปใช้โดยใช้เทมเพลต C++
• Shane Steinert-Threlkeld, "Lambda Calculi" , สารานุกรมปรัชญาอินเทอร์เน็ต
• อันตอน ซาลิคเมตอฟ, แคลคูลัสแลมบ์ดาขนาดใหญ่