ในตรรกศาสตร์ทางคณิตศาสตร์แคลคูลัสแลมบ์ดา (หรือเขียนว่าλ -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 (แลมบ์ดาg .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 (แลมบ์ชั่วโมง .แลต 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)คือเมื่อฟังก์ชันเรียกตัวเอง ค่าใดที่จะใช้แทนฟังก์ชันดังกล่าวได้? มันจะต้องอ้างอิงถึงตัวเองภายในตัวมันเอง เหมือนกับที่นิยามอ้างอิงถึงตัวเองภายในตัวมันเอง ถ้าค่านี้มีตัวมันเองอยู่ภายใน มันจะต้องมีขนาดอนันต์ ซึ่งเป็นไปไม่ได้ สัญกรณ์อื่นๆ ที่รองรับการเรียกซ้ำโดยธรรมชาติ จึงแก้ปัญหานี้โดยการอ้างอิงถึงฟังก์ชันด้วยชื่อภายในนิยาม แคลคูลัสแลมบ์ดาไม่สามารถแสดงสิ่งนี้ได้ เนื่องจากในนั้นไม่มีชื่อสำหรับเทอม มีเพียงชื่อของอาร์กิวเมนต์ เช่น พารามิเตอร์ในนามธรรม ดังนั้น นิพจน์แลมบ์ดาจึงสามารถรับตัวเองเป็นอาร์กิวเมนต์และอ้างอิงถึง (สำเนาของ) ตัวเองผ่านชื่อของพารามิเตอร์ที่เกี่ยวข้อง ซึ่งจะทำงานได้ดีในกรณีที่มันถูกเรียกโดยมีตัวเองเป็นอาร์กิวเมนต์ ตัวอย่างเช่น (λ x . x x ) E = ( EE )จะแสดงการเรียกซ้ำเมื่อEเป็นนามธรรมที่ใช้พารามิเตอร์กับตัวเองภายในตัวมันเพื่อแสดงการเรียกซ้ำ เนื่องจากพารามิเตอร์นี้รับ ค่าเป็น 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" , สารานุกรมปรัชญาอินเทอร์เน็ต
• อันตอน ซาลิคเมตอฟ, แคลคูลัสแลมบ์ดาขนาดใหญ่